Legge della doppia negazione intuizionista
Nella logica intuizionista, da una prova di $A$ si può sempre costruire una prova di $\neg \neg A$: $$ A \vdash \neg \neg A $$ Tuttavia, non è sempre possibile dedurre $A$ da $\neg \neg A$ senza una prova costruttiva: $$ \neg \neg A \not\vdash A $$
In altre parole, nella logica intuizionista, se dimostro che qualcosa è vero, posso anche dimostrare che è impossibile dimostrarne la falsità (cioè ¬¬A).
Tuttavia, sapere solo che qualcosa non è falso non basta per affermare che sia vero: serve sempre una prova costruttiva.
Quindi, nella logica intuizionista la doppia negazione di $ A $ non permette in generale di dedurre $ A $ .
Perché è Importante? Questa differenza evidenzia il cuore della logica intuizionista: essa è costruttiva. Non basta sapere che qualcosa non è falso per poterlo considerare vero; occorre sempre una dimostrazione diretta.
Un esempio pratico
Considero la proposizione
A: "Esiste una sequenza infinita di cifre uguali nel numero decimale π"
In questo caso non ho una prova costruttiva per affermare che è vera, né una confutazione.
Nella logica intuizionista non posso affermare $ A $, né posso dedurre $ A $ da $ \neg \neg A $ senza una dimostrazione costruttiva esplicita.
Infatti, $ \neg \neg A $ significherebbe solo che è impossibile dimostrare costruttivamente che $ A $ porti a contraddizione, ma questo non equivale ad avere una prova di $ A $.
Differenza con la logica classica
Nella logica classica, vale sempre la legge della doppia negazione, ossia ogni proposizione è logicamente equivalente alla sua doppia negazione:
$$ \neg \neg A \;\iff\; A $$
In altre parole, se $ \neg \neg A$ è vero, allora $A$ è vero, e viceversa.
Esempio. Nella logica classica, se "non è falso che esiste una sequenza infinita di cifre uguali nel numero decimale di π", allora si può concludere che "esiste una sequenza infinita di cifre uguali nel numero decimale di π".
Nella logica intuizionista, invece, questa equivalenza non vale in generale. Vale solo la deduzione in avanti:
$$ A \vdash \neg \neg A $$
cioè se possiedo una prova costruttiva di $A$, allora posso anche costruire una prova di $\neg \neg A$.
Il contrario, invece, non è sempre vero senza una dimostrazione costruttiva esplicita di $A$:
$$ \neg \neg A \not\vdash A $$
Esempio. Nella logica intuizionista, anche se posso dimostrare che è impossibile provare che $ A $ porti a contraddizione, ossia $A \to \bot$, non posso affermare direttamente che $ A $ è vera senza una prova costruttiva. In questo caso non posso concludere che "esiste una sequenza infinita di cifre uguali nel numero decimale di π".
Questo vuole dire che nella logica intuizionista non posso usare il ragionamento per assurdo per dimostrare un’affermazione positiva qualunque.
Cioè, non posso in generale dimostrare $ A $ partendo da $ \neg \neg A $
Le dimostrazioni per assurdo
Nella logica classica, se voglio dimostrare $ A $ posso ragionare così:
- Suppongo per assurdo $ \neg A $
- Dimostro che $ \neg A $ arriva a contraddizione.
- Deduco che $ \neg \neg A $ è vero
- Se $ \neg \neg A $ è vero allora $ A $ è vero
Nella logica intuizionista, invece. il passaggio finale $ ¬¬A⊢A $ non è valido in generale.
Senza costruzione esplicita di $ A $ mi devo fermare a $ ¬¬A $ e basta.
Esempio
Assumo la proposizione A che "esiste un numero naturale pari maggiore di 2 che è la somma di due numeri primi", si tratta di un caso particolare della congettura di Goldbach.
Suppongo che non esista nessun numero pari maggiore di 2 somma di due primi ( $ ¬A $) e dimostro tramite qualche teorema matematico che porta a una contraddizione (⊥).
Concludo che la proposizione A "non è falsa" ( $ ¬¬A $).
Da questo punto in poi la conclusione cambia a seconda se adotto la logica classica o intuizionista.
- Nella logica classica $ ¬¬A $ implica $ A $.
- Nella logica intuizionista, invece, non posso passare da $ ¬¬A $ a $ A $ in generale, senza una prova costruttiva. Per affermare l’esistenza di quel numero pari, devo esibire esplicitamente quale numero è e quali due numeri primi lo compongono. Sapere solo che la sua esistenza non porta a contraddizione non basta.
Ad esempio, prendo il numero 8 che è composto dalla somma di due numeri primi (3+5). Questo prova che esiste almeno un numero maggiore di 2 composto dalla somma di due numeri primi.
In particolar modo, nella logica intuizionista non posso dimostrare per assurdo una affermazione senza una prova costruttiva.
E' invece possibile dimostrare per assurdo una negazione.
Nota. Nella logica intuizionista, posso sempre dimostrare per assurdo una negazione. Ad esempio, se voglio dimostrare $ \neg A $ posso assumere $ A $ come ipotesi e dimostrare che porta a una contraddizione ( $ A \rightarrow \bot $ ). In questo caso anche nella logica intuizionista posso concludere che $ \neg A $ è dimostrabile. $$ A→⊥ \ ⊢ \ ¬A $$ Questa forma di ragionamento per assurdo è valida, ma non si può usare in generale per dimostrare affermazioni positive senza una costruzione esplicita. Ad esempio, assumo la proposizione A che "5 sia pari e dispari". Questo è impossibile, perché un numero naturale non può essere contemporaneamente pari e dispari. Quindi, da questa ipotesi deriva una contraddizione (⊥). Quindi, posso concludere che $ ¬A $ è dimostrabile.
E così via.
