Teoria assiomatica per il calcolo proposizionale e costruzione di una dimostrazione (esercizio proposto)
Salve a tutti. Sono iscritto al forum da 3 anni ma non partecipo attivamente spesso; tuttavia "mi affaccio" assiduamente per risolvere dubbi che sorgono dallo studio di varie materie. Ma veniamo al nocciolo della questione. Ultimamente ho iniziato a studiare (per diletto) Logica matematica e utilizzo il libro di Elliot Mendelson, "Introduzione alla Logica Matematica", Bollati Boringhieri. La questione è la seguente. Considerate una teoria formale assiomatica $L$ per il calcolo proposizionale. Come ben sapete gli schemi assiomi di $L$ sono:
A1 $(A \Rightarrow (B \Rightarrow A) )$
A2 $((A \Rightarrow (B \Rightarrow C)) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C)))$
A3 $((\negB \Rightarrow \negA) \Rightarrow ((\negB \Rightarrow A) \Rightarrow B))$
dove $A,B,C$ sono fbf (formule ben formate). Inoltre l'unica regola di inferenza di $L$ è il "modus ponens" (MP): $B$ è una conseguenza diretta di $A$ e di $A\RightarrowB$.
A pagina 46, l'autore chiede di dimostrare: $A\RightarrowB, B\RightarrowC \vdash A \Rightarrow C$. In altri termini, bisogna dimostrare che $A\RightarrowC$ è una conseguenza diretta di $A\RightarrowB, B\RightarrowC$.
Pertanto, riporto testualmente dal libro " una fbf $A$ si dice essere una conseguenza in $L$ di un insieme $\Gamma$ di fbf se e solo se esiste una sequenza $A_1,...,A_n$ di fbf tale che $A=A_n$ e, per ogni $i$, o $A_i$ è un assioma, o $A_i$ è in $\Gamma$, o $A_i$ è una conseguenza diretta , per mezzo di regole di inferenza , di precedenti fbf della sequenza. Tale sequenza si chiama "dimostrazione di $A$ da $\Gamma$".
In sostanza, tornando all'esercizio proposto, è necessario costruire una sequenza in cui l'ultima fbf della sequenza è $A\RightarrowC$, mentre le precedenti fbf della sequenza, o rientrano negli schemi di assiomi A1, A2, A3, o sono le ipotesi (in questo caso $A\RightarrowB$ e $B\RightarrowC$), oppure sono conseguenze dirette, per mezzo della regola MP, di precedenti fbf. Dunque l'esercizio consiste nella costruzione di una tale sequenza, MA, cosa importante, SENZA FARE USO DEL Teorema di deduzione. In effetti, nel libro, il Teorema di deduzione viene introdotto dopo questo esercizio.
In conclusione, sono tre giorno che sto cercando di fare questa dimostrazione (ripeto, senza l'uso del teorema di deduzione) ma non ne vengo a capo. Sarei grato se qualcuno potesse aiutarmi.
Spero di essere stato il più chiaro possibile.
A1 $(A \Rightarrow (B \Rightarrow A) )$
A2 $((A \Rightarrow (B \Rightarrow C)) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C)))$
A3 $((\negB \Rightarrow \negA) \Rightarrow ((\negB \Rightarrow A) \Rightarrow B))$
dove $A,B,C$ sono fbf (formule ben formate). Inoltre l'unica regola di inferenza di $L$ è il "modus ponens" (MP): $B$ è una conseguenza diretta di $A$ e di $A\RightarrowB$.
A pagina 46, l'autore chiede di dimostrare: $A\RightarrowB, B\RightarrowC \vdash A \Rightarrow C$. In altri termini, bisogna dimostrare che $A\RightarrowC$ è una conseguenza diretta di $A\RightarrowB, B\RightarrowC$.
Pertanto, riporto testualmente dal libro " una fbf $A$ si dice essere una conseguenza in $L$ di un insieme $\Gamma$ di fbf se e solo se esiste una sequenza $A_1,...,A_n$ di fbf tale che $A=A_n$ e, per ogni $i$, o $A_i$ è un assioma, o $A_i$ è in $\Gamma$, o $A_i$ è una conseguenza diretta , per mezzo di regole di inferenza , di precedenti fbf della sequenza. Tale sequenza si chiama "dimostrazione di $A$ da $\Gamma$".
In sostanza, tornando all'esercizio proposto, è necessario costruire una sequenza in cui l'ultima fbf della sequenza è $A\RightarrowC$, mentre le precedenti fbf della sequenza, o rientrano negli schemi di assiomi A1, A2, A3, o sono le ipotesi (in questo caso $A\RightarrowB$ e $B\RightarrowC$), oppure sono conseguenze dirette, per mezzo della regola MP, di precedenti fbf. Dunque l'esercizio consiste nella costruzione di una tale sequenza, MA, cosa importante, SENZA FARE USO DEL Teorema di deduzione. In effetti, nel libro, il Teorema di deduzione viene introdotto dopo questo esercizio.
In conclusione, sono tre giorno che sto cercando di fare questa dimostrazione (ripeto, senza l'uso del teorema di deduzione) ma non ne vengo a capo. Sarei grato se qualcuno potesse aiutarmi.
Spero di essere stato il più chiaro possibile.
Risposte
A1 $ (A \Rightarrow (B \Rightarrow A) ) $
A2 $ ((A \Rightarrow (B \Rightarrow C)) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C))) $
A3 $ ((\negB \Rightarrow \negA) \Rightarrow ((\negB \Rightarrow A) \Rightarrow B)) $
non so se si può ottenere più semplicemente, comunque questa dimostrazione qui di seguito dovrebbe funzionare.
sostituendo in A1 al posto di $A$//$(B \Rightarrow C)$ e al posto di $B$//$A$
si ottiene $ ((B \Rightarrow C) \Rightarrow (A \Rightarrow (B \Rightarrow C)) ) $
Per (MP) dato che $(B \Rightarrow C)$ è nell'insieme otteniamo $(A \Rightarrow (B \Rightarrow C)))$
da quest'ultima e da A2 otteniamo per (MP) $((A \Rightarrow B) \Rightarrow (A \Rightarrow C))$
siccome $(A\RightarrowB)$ è nell'insieme di nuovo per (MP) otteniamo $(A \Rightarrow C)$.
A2 $ ((A \Rightarrow (B \Rightarrow C)) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C))) $
A3 $ ((\negB \Rightarrow \negA) \Rightarrow ((\negB \Rightarrow A) \Rightarrow B)) $
non so se si può ottenere più semplicemente, comunque questa dimostrazione qui di seguito dovrebbe funzionare.
sostituendo in A1 al posto di $A$//$(B \Rightarrow C)$ e al posto di $B$//$A$
si ottiene $ ((B \Rightarrow C) \Rightarrow (A \Rightarrow (B \Rightarrow C)) ) $
Per (MP) dato che $(B \Rightarrow C)$ è nell'insieme otteniamo $(A \Rightarrow (B \Rightarrow C)))$
da quest'ultima e da A2 otteniamo per (MP) $((A \Rightarrow B) \Rightarrow (A \Rightarrow C))$
siccome $(A\RightarrowB)$ è nell'insieme di nuovo per (MP) otteniamo $(A \Rightarrow C)$.
Si bub è perfetta. ti ringrazio molto. avevo provato sostituzioni complicatissime....mi chiedo come ho fatto a non arrivarci. in realtà come prima prova ero proprio partito dalla A2, così com'è, vale a dire senza effettuare sostituzioni, per poi costruire la "validità" di $A\Rightarrow(B\RightarrowC)$; poichè fatto ciò, il gioco è fatto. Poi, bo....non so perchè ho mollato quella strada e iniziare a complicarmi la vita
. Comunque, grazie di nuovo, ottimo!


Salve, continuo con questo argomento. In particolare, propongo due dimostrazioni.
a) $A\Rightarrow(B\RightarrowC)\vdash B\Rightarrow(A\RightarrowC)$
b) $(\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)$
Allora, del teorema a) ho già una dimostrazione e, per chi è interessato, posso riportarla nella prossima risposta. Ciò che mi sta mettendo in difficoltà è invece la dimostrazione del teorema b). Ho fatto molte prove, ma alla fine mi perdo sempre. In effetti, sono convinto che si tratti di una dimostrazione abbastanza lunga. Ho scelto di riportare qui due punti di partenza alternativi utilizzati per dimostrare il teorema. All'inizio ero partito da:
c) $((\negB\Rightarrow\negA)\Rightarrow(((\negB\RightarrowA)\RightarrowB)\Rightarrow(A\RightarrowB)))\Rightarrow(((\negB\Rightarrow\negA)\Rightarrow((\negB\RightarrowA)\RightarrowB))\Rightarrow((\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)))$ schema di assiomi A2
Infatti, considerando lo schema A2 (che è possibile consultare nel primo messaggio), ho posto $(\negB\Rightarrow\negA)$ in luogo di $A$, $((\negB\RightarrowA)\RightarrowB)$ al posto di $B$, e, infine, $((\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB))$ in luogo di $C$.
Partendo da c) la difficoltà consiste nel dimostrare la validità del primo blocco di parentesi, poichè il secondo blocco è effettivamente lo schema A3. Per me è stato abbastanza arduo e in effetti "ho fallito"
. Allora ho reimpostato il problema ,cercando di semplificarlo, in questi termini:
d) $((\negB\Rightarrow\negA)\Rightarrow((\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)))\Rightarrow(((\negB\Rightarrow\negA)\Rightarrow(\negB\Rightarrow\negA))\Rightarrow((\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)))$
Partendo da d), di nuovo, la difficoltà sta tutta nel dimostrare la validità del primo blocco di parentesi (cioè, $((\negB\Rightarrow\negA)\Rightarrow((\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)))$) dato che il secondo blocco (ossia, $((\negB\Rightarrow\negA)\Rightarrow(\negB\Rightarrow\negA))$) è effettivamente un teorema, la cui dimostrazione è abbastanza banale.
Non so se ci sono strade più semplici, e quindi chiedo un vostro aiuto.
in bocca al lupo
a) $A\Rightarrow(B\RightarrowC)\vdash B\Rightarrow(A\RightarrowC)$
b) $(\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)$
Allora, del teorema a) ho già una dimostrazione e, per chi è interessato, posso riportarla nella prossima risposta. Ciò che mi sta mettendo in difficoltà è invece la dimostrazione del teorema b). Ho fatto molte prove, ma alla fine mi perdo sempre. In effetti, sono convinto che si tratti di una dimostrazione abbastanza lunga. Ho scelto di riportare qui due punti di partenza alternativi utilizzati per dimostrare il teorema. All'inizio ero partito da:
c) $((\negB\Rightarrow\negA)\Rightarrow(((\negB\RightarrowA)\RightarrowB)\Rightarrow(A\RightarrowB)))\Rightarrow(((\negB\Rightarrow\negA)\Rightarrow((\negB\RightarrowA)\RightarrowB))\Rightarrow((\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)))$ schema di assiomi A2
Infatti, considerando lo schema A2 (che è possibile consultare nel primo messaggio), ho posto $(\negB\Rightarrow\negA)$ in luogo di $A$, $((\negB\RightarrowA)\RightarrowB)$ al posto di $B$, e, infine, $((\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB))$ in luogo di $C$.
Partendo da c) la difficoltà consiste nel dimostrare la validità del primo blocco di parentesi, poichè il secondo blocco è effettivamente lo schema A3. Per me è stato abbastanza arduo e in effetti "ho fallito"


d) $((\negB\Rightarrow\negA)\Rightarrow((\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)))\Rightarrow(((\negB\Rightarrow\negA)\Rightarrow(\negB\Rightarrow\negA))\Rightarrow((\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)))$
Partendo da d), di nuovo, la difficoltà sta tutta nel dimostrare la validità del primo blocco di parentesi (cioè, $((\negB\Rightarrow\negA)\Rightarrow((\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)))$) dato che il secondo blocco (ossia, $((\negB\Rightarrow\negA)\Rightarrow(\negB\Rightarrow\negA))$) è effettivamente un teorema, la cui dimostrazione è abbastanza banale.
Non so se ci sono strade più semplici, e quindi chiedo un vostro aiuto.
in bocca al lupo


ciao a tutti, ho appena finito di studiare il teorema di deduzione.
TEOREMA DI DEDUZIONE: Se $\Gamma$ è un insieme di fbf, e $A$ e $B$ sono fbf, e $\Gamma, A \vdashB$, allora $\Gamma\vdashA\RightarrowB$. In particolare, se $A\vdashB$, allora $\vdashA\RightarrowB$ (Herbrand, 1930).
Utilizzando tale teorema, sono riuscito a risolvere il problema b) del messaggio precedente, ossia dimostrare $\vdash(\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)$.
La dimostrazione è la seguente:
-innanzitutto dimostro $(\negB\Rightarrow\negA)\vdash(A\RightarrowB)$
1)$(\negB\Rightarrow\negA)\Rightarrow((\negB\RightarrowA)\RightarrowB)$ schema assiomi A3
2)$(\negB\Rightarrow\negA)$ ipotesi
3)$(\negB\RightarrowA)\RightarrowB$ da 1),2) per MP
4)$((\negB\RightarrowA)\RightarrowB)\Rightarrow(A\Rightarrow((\negB\RightarrowA)\RightarrowB))$ schema assiomi A1
5)$A\Rightarrow((\negB\RightarrowA)\RightarrowB)$ da 3), 4) per MP
6)$(A\Rightarrow((\negB\RightarrowA)\RightarrowB))\Rightarrow((A\Rightarrow(\negB\RightarrowA))\Rightarrow(A\RightarrowB))$ schema assiomi A2
7)$(A\Rightarrow(\negB\RightarrowA))\Rightarrow(A\RightarrowB)$ da 5), 6) per MP
8)$A\Rightarrow(\negB\RightarrowA)$ schema assiomi A1
9)$A\RightarrowB$ da 7), 8) tramite MP
- per cui $(\negB\Rightarrow\negA)\vdash(A\RightarrowB)$. Cosi, per il teorema di deduzione $\vdash(\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)$
Insomma, niente di particolarmente complicato. In effetti l'uso del teorema di deduzione semplifica enormemente le dimostrazioni dei teoremi. La domanda è questa, c'è qualcuno che riesce a dimostrare $\vdash(\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)$ senza utilizzare il teorema di deduzione??
TEOREMA DI DEDUZIONE: Se $\Gamma$ è un insieme di fbf, e $A$ e $B$ sono fbf, e $\Gamma, A \vdashB$, allora $\Gamma\vdashA\RightarrowB$. In particolare, se $A\vdashB$, allora $\vdashA\RightarrowB$ (Herbrand, 1930).
Utilizzando tale teorema, sono riuscito a risolvere il problema b) del messaggio precedente, ossia dimostrare $\vdash(\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)$.
La dimostrazione è la seguente:
-innanzitutto dimostro $(\negB\Rightarrow\negA)\vdash(A\RightarrowB)$
1)$(\negB\Rightarrow\negA)\Rightarrow((\negB\RightarrowA)\RightarrowB)$ schema assiomi A3
2)$(\negB\Rightarrow\negA)$ ipotesi
3)$(\negB\RightarrowA)\RightarrowB$ da 1),2) per MP
4)$((\negB\RightarrowA)\RightarrowB)\Rightarrow(A\Rightarrow((\negB\RightarrowA)\RightarrowB))$ schema assiomi A1
5)$A\Rightarrow((\negB\RightarrowA)\RightarrowB)$ da 3), 4) per MP
6)$(A\Rightarrow((\negB\RightarrowA)\RightarrowB))\Rightarrow((A\Rightarrow(\negB\RightarrowA))\Rightarrow(A\RightarrowB))$ schema assiomi A2
7)$(A\Rightarrow(\negB\RightarrowA))\Rightarrow(A\RightarrowB)$ da 5), 6) per MP
8)$A\Rightarrow(\negB\RightarrowA)$ schema assiomi A1
9)$A\RightarrowB$ da 7), 8) tramite MP
- per cui $(\negB\Rightarrow\negA)\vdash(A\RightarrowB)$. Cosi, per il teorema di deduzione $\vdash(\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)$
Insomma, niente di particolarmente complicato. In effetti l'uso del teorema di deduzione semplifica enormemente le dimostrazioni dei teoremi. La domanda è questa, c'è qualcuno che riesce a dimostrare $\vdash(\negB\Rightarrow\negA)\Rightarrow(A\RightarrowB)$ senza utilizzare il teorema di deduzione??