Esercizio Deduzione Naturale

One2
Devo svolgere:
$P$$vv$$Q$,$not$$P$ implica $Q$
Secondo me è giusto dire che:
$P$$vv$$Q$,$not$$P$,$not$$Q$ implica $\bot$
Però non sò più andare avanti....
Mi potete dare una mano?

Risposte
vict85
Puoi usare il principio del terzo escluso. O meglio che \(Q\vee \neg Q\) è una tautologia.

One2
Scusa,ma non capisco quale sia il vantaggio una volta applicato tale principio.
(Devi avere pazienza,sono alle prime armi con questo tipo di esercizzi)

vict85
Avevo letto male.

La dimostrazione con la deduzione naturale non è proprio tra le più immediate. Comunque...

La prima ipotesi dice che \(\displaystyle P\vee Q \) deve aversi una delle due. Quindi dividiamo in casi.

Se \(\displaystyle P \) allora \(\displaystyle P,\ \neg P \Rightarrow \perp \Rightarrow Q\) per la seconda ipotesi. Cioè \(\displaystyle P\rightarrow Q \).

Se \(\displaystyle Q \) allora \(\displaystyle Q \). Quindi \(\displaystyle Q\rightarrow Q \).

E quindi puoi concludere. Ho fatto queste cose un po' di tempo fa e non sono proprio sicurissimo delle notazioni. Controllale tu. Anche perché magari vuoi scrivere il tutto "in colonna".

One2
Credo di avere capito in parte...
Cioè,devo concludere facendo la disgiunzione di $P$$vv$$Q$.Però per fare questo devo sapere che $Q$ è vero e $P$ è vero.
Per $Q$ è facile,perchè sò dall'inizio che $Q$ è vero,ma come faccio a dire che $P$ e vero se all'inizio ho $not$$P$ :?: (forse per assurdo?).Le mie difficolta stanno prorio nel comprendere questo ultimo passaggio.

Simonixx
Allora potresti provare in questa maniera, sempre cercando di fare in modo che le assunzioni rimanenti quando giungi alla conclusione siano SOLO quelle due che hai lì, ad assumere anche $notQ$ e a dimostrare la seguente sequenza (che vale anche il viceversa):

$notP ^^ notQ harr not(P vv Q)$

Se dimostri questa, ti ritrovi che hai l'assunzione $P vv Q$ e la sua negazione, che deriva essenzialmente dalle assunzioni $notP$ e $notQ$, quindi tramite una reductio ad absurdum, che è una regola di inferenza che prende come assunzioni quelle che ti hanno portato a negare l'assunzione di prima + quella che hai assunto prima di tutto questo, ovvero le assunzioni di $notP ^^ notQ$ e l'assunzione iniziale $notQ$, ottieni $notnotQ = Q$.

Ora se non ho sbagliato i calcoli, dovresti ritrovare la conclusione soprascritta con solo le prime due assunzioni iniziali.

p.s.: non è facile spiegarmi, lo so. Finisco di studiare algebra e cerco di fare un incolonnamento e vedere se ho ragione o no... (la sequenza comunque è sicuramente vera, ma neanche semplice da dimostrare)

vict85
"Simonixx":
Allora potresti provare in questa maniera, sempre cercando di fare in modo che le assunzioni rimanenti quando giungi alla conclusione siano SOLO quelle due che hai lì, ad assumere anche $notQ$ e a dimostrare la seguente sequenza (che vale anche il viceversa):

$notP ^^ notQ harr not(P vv Q)$

Se dimostri questa, ti ritrovi che hai l'assunzione $P vv Q$ e la sua negazione, che deriva essenzialmente dalle assunzioni $notP$ e $notQ$, quindi tramite una reductio ad absurdum, che è una regola di inferenza che prende come assunzioni quelle che ti hanno portato a negare l'assunzione di prima + quella che hai assunto prima di tutto questo, ovvero le assunzioni di $notP ^^ notQ$ e l'assunzione iniziale $notQ$, ottieni $notnotQ = Q$.

Ora se non ho sbagliato i calcoli, dovresti ritrovare la conclusione soprascritta con solo le prime due assunzioni iniziali.

p.s.: non è facile spiegarmi, lo so. Finisco di studiare algebra e cerco di fare un incolonnamento e vedere se ho ragione o no... (la sequenza comunque è sicuramente vera, ma neanche semplice da dimostrare)


Ho sono un dubbio. Ma che logica sta usando? Perché in quella intuizionista la doppia negazione non sarebbe proprio ammessa... :roll: O forse mi ricordo male...

Simonixx
E' logica elementare classica di 1° ordine... (quasielementare se ci metti anche l'identità)...

E la doppia negazione c'è >.<

Bibliografia: E.J. Lemmon "Fondamenti di Logica"

vict85
"Simonixx":
E' logica elementare classica di 1° ordine... (quasielementare se ci metti anche l'identità)...

E la doppia negazione c'è >.<

Bibliografia: E.J. Lemmon "Fondamenti di Logica"


Ma la deduzione naturale si usa anche in logica intuizionista... Io l'ho studiata al suo interno. Semplicemente hai meno possibità. A meno che tu sappia dove studia non darei per scontato che possa usare regole non universalmente accettate.

In ogni caso ho mostrato che non serve affatto usarlo. Ho visto cercando anche un'altra dimostrazione che non la usa. Basta usare come mostrato la regola di eliminazione del $\vee$. Se scrivete tutto in colonna vedete che vi esce.

Simonixx
Il tuo modo di fare è giusto, si, ma non trovo un incollonnamento immediato. Il mio invece poteva essere incolonnato. Comunque non è logica "intuizionista" quella che intendo io, e la doppia negazione è lecita...

$1; P vv Q ; 1A$
$2; notP; 2 A$
$3; P; 3 A$
$2,3; P ^^ notP; 2,3I^^$
A questo punto l'implicazione dalla disgiunzione alla verità di Q come si svolge?
Per l'altro caso, cioè assumendo Q..

$5; Q ; 5 A$

E poi faccio l'eliminazione della disgiunzione, ok. Ma manca il passaggio con le regole di inferenza di prima...

vict85
Introducendo \(\perp\)... Ovviamente devi avere \(\perp\) nel linguaggio... altrimenti devi seguire un'altra strada.

Dopo una breve ricerca l'ho trovato... Qui è scritto senza tutte le regole segnate. Ovviamente non sono difficili da scrivere...
http://www-sop.inria.fr/marelle/Laurent ... 1.html#E10

Ovviamente se tu non hai \(\perp\) devi seguire un'altra strada.

Simonixx
Domanda: siccome che non conosco quel simbolo, cosa starebbe a significare e in che logica è introdotto?

One2
Grazie per le spiegazioni,finalmente ho capito come svolgerlo :D

$\bot$ questo simbolo è usato per indicare il falso

P.S:Nel link che hai postato quale sarebbe l'esercizio simile al mio?

Rispondi
Per rispondere a questa discussione devi prima effettuare il login.