[Logica intuizionista] Negazione

[thedarkhero]

La negazione in logica classica è una proposizione mentre in logica intuizionista non lo è.
Si può tuttavia utilizzare l'approssimazione $notA=A->\bot$ per interpretare intuizionisticamente la negazione.
Vediamo ora la proposizione classica $not(AandnotA)$ che in logica intuizionista va interpretata come $(Aand(A->\bot))->\bot$.
Dal punto di vista classico la proposizione è chiaramente vera ma non mi è chiaro perchè non lo è dal punto di vista intuizionista...

[Susannap1]

Prendi con le pinze ciò che dico , perché sono frutto di considerazioni personali altamente opinabili e visto che non studio matematica (ma scienze della formazione primaria) con probabilità di errore altissime .

Chiamiamo $y$ la tua proposizione .

Se $y$ è dimostrabile, allora è certamente impossibile provare che non esiste una dimostrazione di $y$ (introduzione della doppia negazione); ma l'eliminazione della doppia negazione è intuizionisticamente insostenibile se non c'è una dimostrazione che non esiste una dimostrazione di $y$,quindi non è possibile concludere che esista una dimostrazione di $y$.

Ciao e scusa se eventualmente ho detto una cavolata ..

[fields1]

"thedarkhero":
Vediamo ora la proposizione classica $not(AandnotA)$ che in logica intuizionista va interpretata come $(Aand(A->\bot))->\bot$.
Dal punto di vista classico la proposizione è chiaramente vera ma non mi è chiaro perchè non lo è dal punto di vista intuizionista...

E' vera anche dal punto di vista intuizionista. Se abbiamo $A\wedge \neg A$, abbiamo $A$ e $A\->\bot$ e dunque per modus ponens $\bot$. Abbiamo quindi dimostrato che $(A\wedge \neg A)\->\bot$.

Il fatto è che tu hai considerato una formulazione debole del terzo escluso. La vera formulazione è $A\vee \neg A$ ed è questa che non è valida intuizionisticamente. Mentre in logica classica le due formulazioni del terzo escluso sono equivalenti, in logica intuizionista non lo sono!

[thedarkhero]

Giusto. Consideriamo allora la proposizione che dici tu $A or not A$ che in logica intuizionista viene interpretata come $A or (A -> \bot)$.
Come facciamo a dire che questa proposizione non è vera in logica classica? Se trovassimo un ticket per la proposizione allora sarebbe vera, mentre per dire che non è vera cosa dobbiamo trovare?

[fields1]

"thedarkhero":Giusto. Consideriamo allora la proposizione che dici tu $A or not A$ che in logica intuizionista viene interpretata come $A or (A -> \bot)$.
Come facciamo a dire che questa proposizione non è vera in logica classica? Se trovassimo un ticket per la proposizione allora sarebbe vera, mentre per dire che non è vera cosa dobbiamo trovare?

Per dire che $A\vee \neg A$ non è valida intuizionisticamente basta trovare una $A$ per cui non esiste un ticket, cioè non esiste né un ticket per $A$ né per $\neg A$. Ora non so che definizione di ticket hai, ma di solito basta prendere una proposizione indecidibile, alla Gödel, che non è né dimostrabile né refutabile.

[thedarkhero]

Chiedo scusa, intendevo come possiamo dire che non è vera in logica intuizionista?

[fields1]

"thedarkhero":Chiedo scusa, intendevo come possiamo dire che non è vera in logica intuizionista?

Sì, ti ho risposto. Ho distrattamente scritto "classicamente" nel mio post sopra, intendevo "intuizionisticamente", avendo capito che volevi anche tu sapere quello.