Esercizio di deduzione naturale e domanda teoria

[Darèios89]

Allora, ho una derivazione da fare, mi chiedevo se è stata svolta correttamente o meno, allego l'immagine.

http://i58.tinypic.com/35m2mj6.jpg

Correzioni da fare?

Poi avrei questa domanda di teoria, non ho ben capito eliminazione ed introduzione della negazione...dalla teoria ho:

[tex]*\phi[/tex] assunzione
[tex]*.[/tex]
[tex]*.[/tex]
[tex]*.[/tex]
[tex]*\psi[/tex]
[tex]*NOT \psi[/tex]
[tex]NOT \phi[/tex]

Ora la domanda è, la parte [tex]NOT \psi[/tex], devo ottenerla necessariamente in qualche modo, tipo eliminare OR, eliminazione implicazione, oppure posso introdurla banalmente e questo mi permette di uscire banalmente dalla sottoderivazione introducendo il NOT per la variabile che avevo assunto?

Grazie

[el_brando]

Non va bene... Ogni ipotesi che fai (le assunzioni) deve essere "scaricata" tramite le regole che lo permettono (\( \longrightarrow I \), \( \neg I \), \( \vee E \), \( RAA \), et cetera) in logica classica... Non sono molto pratico con lo stile Fitch (preferisco gli alberi) ma la derivazione si potrebbe fare così:
1 \( \forall x (F(x) \wedge G(x)) \) | \( H \)
2 \( F(x) \wedge G(x) \) | \( \forall E_1 \)
3 \( F(x) \) | \( \wedge E_2 \)
4 \( \forall x F(x) \) | \( \forall I_3 \)
5 \( G(x) \) | \( \wedge E_2 \)
6 \( \forall x G(x) \) | \( \forall I_5 \)
7 \( \forall x F(x) \wedge \forall x G(x) \) | \( \wedge I_{4,6} \)
8 \( \forall x (F(x) \wedge G(x)) \longrightarrow \forall x F(x) \wedge \forall x G(x) \) | \( \longrightarrow I_{1,7} \)
9 \( \forall x F(x) \wedge \forall G(x) \) | \( H \)
10 \( \forall x F(x) \) | \( \wedge E_9 \)
11 \( F(x) \) | \( \forall E_{10} \)
12 \( \forall x G(x) \) | \( \wedge E_9 \)
13 \( G(x) \) | \( \forall E_{12} \)
14 \( F(x) \wedge G(x) \) | \( \wedge I_{11,13} \)
15 \( \forall x (F(x) \wedge G(x)) \) | \( \forall I_{14} \)
16 \( \forall x F(x) \wedge \forall x G(x) \longrightarrow \forall x (F(x) \wedge G(x)) \) | \( \longrightarrow I_{9,15} \)
17 \( (\forall x (F(x) \wedge G(x)) \longrightarrow \forall x F(x) \wedge \forall x G(x)) \wedge (\forall x F(x) \wedge \forall x G(x) \longrightarrow \forall x (F(x) \wedge G(x))) \) | \( \wedge I_{8,16}\)

[el_brando]

La regola \( \neg I \) dice:
\( \frac {\begin{matrix} [\varphi] \\ \vdots \\ \bot \end{matrix}} {\neg \varphi} \)
cioè che se dall'ipotesi \( \varphi \) derivi il falso, allora puoi derivare \( \neg \varphi \) scaricando l'ipotesi \( \varphi \)
Il falso lo ottieni come vuoi (ad esempio derivando \( \psi \) e \( \neg \psi \)), l'importante è che se introduci nuove ipotesi queste vengano scartate prima o poi...

[Darèios89]

Quanto alla regola per il not....si solo che ho un dubbio....cioè se io assumessi [tex]\phi[/tex] e poi nella derivazione ottenessi [tex]\psi[/tex] posso poi introdurre a piacimento il NOT [tex]\psi[/tex] e poi scaricare l'assunzione?

[el_brando]

Certo, puoi ipotizzare quello che vuoi basta che alla fine tutte le assunzioni vengano scaricate...
Guarda questo esempio (uso gli alberi di derivazione, secondo me si capisce meglio)...

Vogliamo derivare: \( \vdash (A \longrightarrow \neg B)\longrightarrow (B \longrightarrow \neg A) \)

Albero di derivazione:
[size=180]
\( \bot\frac{\rightarrow E \frac{|A|^1 \ \ \ \ \ |A \longrightarrow \neg B|^3}{ \neg B}_{\ \ \ \ \ \ \ |B|^2}}{\neg I^1\frac{\bot}{\rightarrow I^2\frac{\neg A}{\rightarrow I^3\frac{B\longrightarrow\neg A}{(A \longrightarrow \neg B)\longrightarrow (B \longrightarrow \neg A)}}}} \)
[/size]

Come vedi dopo aver ottenuto \( \neg B \) assumo \( B \) derivando l'assurdo, poi applico la regola \( \neg I \) (l'apice indica l'assunzione che viene scaricata) e successivamente scarico \( B \) con la regola \( \rightarrow I \)