[Deduzione naturale] Problemi nel derivare un sequente

[perplesso1]

Salve, non riesco a capire come derivare il sequente $ \vdash (( neg (\phi \rightarrow \psi)) \rightarrow \phi)$. Il testo dice che devo usare RAA ma non capisco come. Ho anche pensato che potrebbe essere più facile derivare il contrapositivo $ \vdash ((neg \phi) \rightarrow (\phi \rightarrow \psi))$. Ma lo stesso non mi viene. Mi date qualche suggerimento ? Grazie!

[fields1]

Assumi $\not \phi$ e utilizza $\not (\phi ->\psi)$ per derivare il falso.

[perplesso1]

Grazie mille. Allora dici così?

$neg \phi \qquad \qquad neg(\phi \rightarrow \psi)$
--------------------------------------------- (ma questa che regola è?)
falso
------------------------------ RAA
$\phi$
----------------------------------------------- $(\rightarrow I)$
$ (neg(\phi \rightarrow \psi) ) \rightarrow \phi $

Però non mi è chiaro che regola si utilizza per derivare il falso da queste due affermazioni? Per caso è $(neg E)$ ? Questa regola di eliminazione il testo me la presenta utilizzando $\phi$ e $neg \phi$ (cioè una proposizione e la sua negazione mentre $neg \phi$ e $neg (\phi \rightarrow \psi)$ sono diverse, si può fare lo stesso? )

[fields1]

La prima regola che hai scritto non esiste... Suggerimento: prima di tutto, cerca di ricavare $\phi->\psi$ dalla premessa $\not \phi$. Quindi assumi $\phi$ e...

[perplesso1]

Esiste esiste, è semplicemente un'altra versione di $(\rightarrow E)$ considerando $\neg \phi$ equivalente a ($\phi \rightarrow$ falso). Posso dirti il testo: "Mathematical Logic" di Chiswell e Hodges. Adesso rifletto sul tuo suggerimento grazie!

Edit: aspè ma "non esiste" era riferito a $(\neg E)$ o no?

[perplesso1]

$\phi \qquad \qquad (\neg \phi)$
----------------------------- $(\neg E)$
falso
------------ RAA
$\psi$
------------------------ $(\rightarrow I)$
$(\phi \rightarrow \psi) \qquad \qquad \qquad \qquad \qquad (\neg (\phi \rightarrow \psi))$
---------------------------------------------------------------------- $(\neg E)$
falso
------------ RAA
$\phi$
-----------------------------$(\rightarrow I)$
$(\neg (\phi \rightarrow \psi)) \rightarrow \phi$


Come va?

[fields1]

Adesso ci siamo Ps: la regola che non esiste è quella che avevi scritto in cima all'albero di deduzione di prima.

[perplesso1]

C'è un cosa che non capisco, mi sembra di aver usato RAA per fare due cose sostanzialmente diverse. La prima volta ho derivato dal falso un'affermazione che non era fra le mie ipotesi, la seconda volta ho negato un'affermazione e ne ho derivato il falso quindi ho dedotto che quell'affermazione non potevo negarla (cioè doveva essere vera). Ora quest'ultimo procedimento intuitivamente è quello che si fa di solito quando si dimostra qualcosa per assurdo. Invece il primo caso (che se non sbaglio si sintetizza dicendo "dal falso segue tutto") ai miei occhi sembra avere ben poco di intuitivo. Ora mi chiedo questa differenza la vedo solo io oppure c'è davvero? E se c'è perchè due procedimenti diversi non sono espressi con due regole diverse? Grazie e scusa se ti secco con delle domande puerili!

[fields1]

Non preoccuparti, le tue osservazioni sono corrette e sensate. In effetti, nel primo caso si effettua un uso della RAA "banale" e "spropositato". Infatti in molti sistemi di deduzione naturale si preferisce introdurre una regola apposita, la regola dell'ex-falso-quodlibet: dal falso segue tutto. In questo modo, la RAA si mantiene solo per le "vere" dimostrazioni per assurdo. La regola dell'ex-falso, inoltre, è necessaria per i sistemi in cui RAA non c'è, ovvero i sistemi costruttivi.