Pages: [1]   Go Down
Print
Author Topic: Deduzione naturale e logica proposizionale  (Read 372 times)
0 Members e 1 Utente non registrato stanno visualizzando questa discussione.
teo998
Matricola
*
Offline Offline

Posts: 42



WWW
« on: 12-12-2017, 20:05:57 »

Stavo pensando: considerato che abbiamo detto a lezione che deduzione naturale e logica proposizionale sono equivalenti, sono sufficienti i passi sotto elencati (ovviamente svolti in dettaglio) per affermare che "A è un teorema in deduzione naturale se e solo se A è un teorema in logica proposizionale"?
Code:
Se A è un teorema in deduzione naturale, A è un teorema in logica proposizionale.
Si dimostra che tutte le regole di produzione in DN sono regole derivabili e ammissibili in P0;
per le regole in cui è presente lo scaricamento delle ipotesi si fa riferimento al Teorema di Herbrand
per trasformarle in regole che rientrano nella definizione di regola di un sistema formale alla Hilbert.

Se A è un teorema in logica proposizionale, A è un teorema in logica proposizionale
Si dimostra che i tre schemi di assiomi in P0 sono schemi di teoremi in DN. 
L'unica regola di P0 è anche una regola in DN.
Logged

Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.928



WWW
« Reply #1 on: 13-12-2017, 10:10:47 »

La logica proposizionale si puo' definire tramite almeno due differenti sistemi formali:
il sistema formale "alla Hilbert" per la logica proposizionale (quello del Martini)
il sistema formale della deduzione naturale per la logica proposizionale.

La questione descritta quindi in questo thread e' malposta.

Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.928



WWW
« Reply #2 on: 13-12-2017, 11:23:46 »

Immagino comunque che il problema che si pone giustamente teo998
e' quello dell'equivalenza tra i due sistemi formali per la logica proposizionale.
Lui si chiede se l'inseme dei teoremi del sistema alla Hilbert e'
identico all'insieme dei teoremi del sistema in deduzione naturale.
E' meglio pero' porre il problema in modo piu' generale, nel modo seguente:

per ogni insieme Gamma di ipotesi, ed ogni fbf alpha

     Gamma |-DN  alpha    se e solo se  Gamma |-Po  alpha    (*)

Ovviamente bisogna tener presente che le fbf del sistema alla Hilbert del Martini sono
costruite solo utilizzando implicazione e negazione.
Quindi per prima cosa occorre restringere l'insieme delle fbf del sistema in deduzione naturale
alle sole formule con implicazione e negazione.
Fatto questo si dimostra lì'equivalenza (*), che si puo' fare seguendo lo schema proposto da teo998.
Esercizio: dimostrare con precisione l'affermazione (*).

Fatto questo, occorre far vedere che, rappresentando la congiunzione e la disgiunzione come fatto nel Martini
in termini di implicazione e negazione, tutte le regole per la disgiunzione e la negazione sono derivabili in Po.
Nel Martini non viene proposta una rappresentazione per   _|_.
L'assurdo si puo' rappresentare come una qualsiasi formula contraddittoria, per esempio (p and (not p)).
Esercizio: fare quanto indicato.

Grazie a teo998 per essersi posto il problema di  dimostrare con precisione
che i due sistemi di deduzione naturali che abbiamo studiato sono equivalenti.




   
Logged
teo998
Matricola
*
Offline Offline

Posts: 42



WWW
« Reply #3 on: 14-12-2017, 23:00:08 »

Code:
Si dimostra che tutte le regole di produzione in DN sono regole derivabili e ammissibili in P0;

il falso lo sostituisco con: not(A -> (A -> A)), che, essendo la negazione di un assioma, è una contraddizione
Sia C: A→(A→A)
il falso è quindi not C

-> I
(P -> Q) |- (P -> Q)    per il teorema di Herbrand:
(P |- Q) |- (P -> Q)     che è l'enunciato di -> I

-> E
P, P -> Q |- Q      la regola è la stessa

et falso quodlibet:   not C |- B
1.C→(¬B→C)Ak
2.CAk
3.¬B→CMD(2,1)
4.¬C→(¬B→¬C)Ak
5.¬CIp. (il falso)
6.¬B→¬CMD(5,6)
7.(¬B→¬C)→((¬B→C)→B)
8.(¬B→C)→BMD(6,7)
9.BMD(3,8)

not I
(P |- not C) |- not P       per il Teorema di Herbrand:
(P -> not C) |- not P       (DA SVOLGERE)

not E
P, not P |- C
1.P→(¬C→P)Ak
2.PIp.
3.¬C→PMD(2,1)
4.¬P→(¬C→¬P)Ak
5.¬PIp.
6.¬C→¬PMD(5,4)
7.(¬C→¬P)→((¬C→P)→C) A¬
8.(¬C→P)→CMD(6,7)
9.CMD(3,8)

RAA
(not P |- not C) |- P         per  il Teorema di Herbrand
not P -> not C |- P

per la regola not I precedentemente dimostrata:
not P -> not C |- not(not P)
not(not P) |- P (Proposizione 3.6)
not P -> not C |- P

Code:
Si dimostra che i tre schemi di assiomi in P0 sono schemi di teoremi in DN. 
L'unica regola di P0 è anche una regola in DN.
I tre assiomi sono stati già dimostrati sul forum (As e Anot dal sottoscritto  pc)
 
Ak:
 [A] 2
   ----------- [1]
      B -> A
 --------------- [2]
   A -> (B -> A)

As e Anot: Link Immagine
Infine il modus ponens e la regola -> E sono la stessa cosa
« Last Edit: 14-12-2017, 23:02:31 by teo998 » Logged

Pages: [1]   Go Up
Print
Jump to: