Usando quindi gli strumenti della Logica intuizionista, non sì potrà ad esempio dedurre la profezia Italia '14 (P="o l'Italia vincerà il mondiale del 2014 oppure l'Italia non vincerà il mondiale del 2014").
Inoltre, usando l'intuito, molti di voi probabilmente direbbero che affermare che l'Italia vincerà il mondiale del 2014 è equivalente a dire che non è vero che l'Italia non vincerà il mondiale del 2014.
O detto in termini simbolici:
I ↔ ¬¬I
Invece nella Logica intuizionista, dal fatto che l'Italia vincerà il mondiale del 2014 si potrà sì dedurre che non è vero che l'Italia non vincerà il mondiale del 2014 ( I → ¬¬I ), ma non vale il viceversa. Cioè dal fatto che non è vero che l'Italia non vincerà il mondiale del 2014 non si potrà dedurre che l'Italia vincerà il mondiale del 2014 (¬¬I → I).
A questo punto risulta sicuramente interessante vedere molto brevemente qualche cenno di semantica per la Logica intuizionista. È infatti grazie ad essa che possono essere verificate le suddette affermazioni.
Il primo a fornire una semantica per la Logica intuizionista fu Heyting, un allievo di Brouwer.
In modo simile alla semantica per la Logica proposizionale classica, in cui l'algebra booleana viene usata per stabilire se una formula sia vera o falsa, Heyting pensò di introdurre un nuovo tipo di algebra, chiamata in seguito algebra di Heyting, per stabilire se una formula sia vera o falsa nell'ambito della Logica intuizionista.
La Logica proposizionale classica, come la maggior parte dei sistemi di Logica matematica, è costituita da una parte sintattica ed una parte semantica.La parte sintattica è quella che si occupa di definire la corretta struttura delle formule; e nella quale si include di solito anche l'apparato deduttivo che definisce gli assiomi e le regole che consentono di dedurre i teoremi a partire dagli assiomi.
Mentre la parte semantica, che risulta di solito più semplice ed intuitiva, è quella che si occupa di definire il significato dei simboli.
Per definire una semantica della Logica proposizionale classica si può partire ad esempio da una funzione di valutazione che va dall'insieme L delle formule all'insieme {V,F} (vero, falso). O detto in termini più semplici, si definisce un meccanismo per determinare in quali casi una formula sia vera o falsa. La funzione la si definisce nel seguente modo:
- v : L → {V,F}
- v(¬A) = V sse v(A) = F (¬A è vera sse A è falsa)
- v(¬A) = F sse v(A) = V (¬A è falsa sse A è vera)
- v(A∧B) = V sse v(A) = V e v(B) = V (A∧B è vera sse A è vera e B è vera)
- v(A∨B) = V sse v(A) = V oppure v(B) = V (A∨B è vera sse A è vera oppure B è vera)
- v(A→B) = V sse v(A) = F oppure v(B) = V (A→B è vera sse A è falsa oppure B è vera)
Similmente, anche nel caso della Logica proposizionale intuzionista si può definire una funzione di valutazione, ma di tipo un po' diverso. Invece di essere correlata ad un'algebra booleana la funzione di valutazione della Logica proposizionale intuzionista è correlata ad un'algebra di Heyting.
Ad esempio si può definire la funzione di valutazione che va dall'insieme L delle formule all'insieme dei sottinsiemi aperti della retta reale:
- v : L → {int(S) : S ⊆ R} dove int(S) è la parte interna di S
- v(A) = int(v(A))
- v(¬A) = int(v(A)C) dove XC è il complemento di X
- v(A∧B) = v(A) ∩ v(B)
- v(A∨B) = v(A) ∪ v(B)
- v(A→B) = int(v(A)C ∪ v(B))
Grazie a questi teoremi si può facilmente verificare che la formula ¬(A ∧ ¬A) è valida. Il fatto che questa formula risulti valida è un requisito minimale affinché un sistema di Logica matematica possa destare qualche interesse. Se essa risultasse non valida infatti esisterebbero delle A per cui il sistema potrebbe dimostrare sia A che ¬A. Il sistema risulterebbe quindi contraddittorio.
La validità di ¬(A ∧ ¬A) si può dimostrare in quanto ponendo v(A) = X, indipendentemente dall'insieme X che viene scelto come valore della formula A, il valore di ¬(A ∧ ¬A) sarà sempre uguale all'intera retta reale R. Infatti
- v(¬(A ∧ ¬A)) =
- int((v(A ∧ ¬A))C) =
- int((v(A) ∩ v(¬A))C) =
- int((X ∩ int((v(A))C))C) =
- int((X ∩ int(XC))C) =
- (Siccome int(XC) è un sottinsieme di XC allora
- X ∩ int(XC) = ∅)
- int((∅)C)=int(R)=R
Basta scegliere v(A) = {x ∈ R : x > 0 }. Si avrà infatti:
- v((A ∨ ¬A)) =
- v(A) ∪ v(¬A) =
- v(A) ∪ int(v(A)C) =
- {x ∈ R : x > 0 } ∪ int({x ∈ R : x ≤ 0 }) =
- {x ∈ R : x > 0 } ∪ {x ∈ R : x < 0 }) =
- {x ∈ R : x ≠ 0 } ≠ R che è ciò che si voleva dimostrare
Ho anche provato a dimostrare che nella Logica intuizionista vale (I → ¬¬I), ma non vale il viceversa (¬¬I → I). Per chi fosse interessato può dare uno sguardo a questo mio tentativo di dimostrazione.