Aiuto con la deduzione
Non riesco a risolvere questo esercizio, mi blocco e mi incarto con gli asterischi e le sottoderivazioni, qualcuno saprebbe aiutarmi?
[tex]NOT \forall x A \vdash \exists x NOT A[/tex]
[tex]NOT \forall x A \vdash \exists x NOT A[/tex]
Risposte
Ciao Darèios89 
Allora, innanzitutto bisogna che parti con la tua assunzione, ossia $\not \forall x A$. Ora, per ricavare $\exists x$ possiamo seguire due strade: o lo assumiamo noi (ma in tal caso dovremmo discaricarlo successivamente ed il che potrebbe essere un problema per noi) oppure ce lo ricaviamo a partire da un $\bot$ (dall'assurdo se ricordi si può ricavare ciò che si vuole). Essendo noi nella logica classica possiamo usare a tale scopo la regola RRA (che invece in quella intuizionistica non si può usare come penso tu sappia). Io ti suggerisco la seconda strada. Ovviamente per ricavare l'assurdo ci serve anche un'altra ipotesi da cui partire (lascio a te capire quale, è semplice semplice) che poi andrà discaricata.
Quando vuoi sono qua.
Allora, innanzitutto bisogna che parti con la tua assunzione, ossia $\not \forall x A$. Ora, per ricavare $\exists x$ possiamo seguire due strade: o lo assumiamo noi (ma in tal caso dovremmo discaricarlo successivamente ed il che potrebbe essere un problema per noi) oppure ce lo ricaviamo a partire da un $\bot$ (dall'assurdo se ricordi si può ricavare ciò che si vuole). Essendo noi nella logica classica possiamo usare a tale scopo la regola RRA (che invece in quella intuizionistica non si può usare come penso tu sappia). Io ti suggerisco la seconda strada. Ovviamente per ricavare l'assurdo ci serve anche un'altra ipotesi da cui partire (lascio a te capire quale, è semplice semplice) che poi andrà discaricata.
Quando vuoi sono qua.
Ciao! Scusa il ritardo ma ho una miriade di esami e progetti da fare quindi mi sono allontanato un pò da logica. 
Allora, ho provato a svolgere ma non so se sono riuscito a intuire l'assunzione giusta da fare, a scaricarla bene e tutto il resto.
[tex]\neg \forall xA \vdash \exists x \neg A[/tex]
1 [tex]\neg \forall x A[/tex] premessa
2 [tex]* A[/tex] assunzione
3 [tex]* \neg \forall x A[/tex] import(1)
4 [tex]* \forall x A[/tex] [tex]\forall[/tex]-intro(2)
5 [tex]\neg A[/tex] [tex]\neg[/tex]-intro(2)
6 [tex]\exists x \neg A[/tex] [tex]\exists[/tex]-intro(5)
Allora, ho provato a svolgere ma non so se sono riuscito a intuire l'assunzione giusta da fare, a scaricarla bene e tutto il resto.
[tex]\neg \forall xA \vdash \exists x \neg A[/tex]
1 [tex]\neg \forall x A[/tex] premessa
2 [tex]* A[/tex] assunzione
3 [tex]* \neg \forall x A[/tex] import(1)
4 [tex]* \forall x A[/tex] [tex]\forall[/tex]-intro(2)
5 [tex]\neg A[/tex] [tex]\neg[/tex]-intro(2)
6 [tex]\exists x \neg A[/tex] [tex]\exists[/tex]-intro(5)
Allora, assumere $A$ è giusto (sapendo che poi andrà scaricato) ma scritto così non riesco a capire bene tutti i passaggi che fai. Con un po' di pazienza mediante l'uso delle frazioni riusciresti a disegnarmi l'albero di derivazione che ottieni 
In particolare, riferendomi alla $3$, non capisco che regola sia "import". Nella mia versione il $\not \forall x A$ lo utilizzo solo nella premessa.
In particolare, riferendomi alla $3$, non capisco che regola sia "import". Nella mia versione il $\not \forall x A$ lo utilizzo solo nella premessa.
Ciao!
Purtroppo noi non abbiamo usato mai gli alberi di derivazione...usiamo questo metodo qui..
Ad ogni modo, gli asterischi indicano che siamo in una sottoderivazione, quindi la regola import mi permette di inserire qualcosa da fuori, all'interno della sottoderivazione. Per dimostrare quello a cui devo arrivare, devo però in ogni caso trovare un modo per uscire dalla sottoderivazione e ottenere ciò che voglio dimostrare senza asterischi. So che è un pò vago..
Purtroppo noi non abbiamo usato mai gli alberi di derivazione...usiamo questo metodo qui..
Ad ogni modo, gli asterischi indicano che siamo in una sottoderivazione, quindi la regola import mi permette di inserire qualcosa da fuori, all'interno della sottoderivazione. Per dimostrare quello a cui devo arrivare, devo però in ogni caso trovare un modo per uscire dalla sottoderivazione e ottenere ciò che voglio dimostrare senza asterischi. So che è un pò vago..
Ciao
Ho capito un po' di più la tua notazione ora ma, traslando ciò che scrivi nella tua dimostrazione in un albero di derivazione non mi torna il perché dopo aver importato la premessa di fatto non la usi mai congiuntamente a quanto ottieni dopo aver elaborato con vari passaggi l'assunzione $A$. Consiglio: la $\not_i$ (not introduction) non ti serve (e secondo me non è neanche applicata correttamente nella tua dimostrazione). Prova ad applicare la $\forall_i$ alla tua assunzione $A$ e successivamente usare ciò che ottieni assieme alla tua premessa. In tal caso la regola che ti suggerisco è la $\bot_e$.
Prova e caso mai fammi sapere...
Ho capito un po' di più la tua notazione ora ma, traslando ciò che scrivi nella tua dimostrazione in un albero di derivazione non mi torna il perché dopo aver importato la premessa di fatto non la usi mai congiuntamente a quanto ottieni dopo aver elaborato con vari passaggi l'assunzione $A$. Consiglio: la $\not_i$ (not introduction) non ti serve (e secondo me non è neanche applicata correttamente nella tua dimostrazione). Prova ad applicare la $\forall_i$ alla tua assunzione $A$ e successivamente usare ciò che ottieni assieme alla tua premessa. In tal caso la regola che ti suggerisco è la $\bot_e$.
Prova e caso mai fammi sapere...
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo