Mar 052013
 

Definisco innanzitutto un semplice linguaggio formale a partire da due soli simboli $A$, $B$ che considero l’uno la negazione dell’altro: $B = neg A$ e $A = neg B$. Qui sto usando i simboli $neg$ e $=$ per semplice comodità illustrativa, ma tali simboli non fanno parte del linguaggio, all’interno del quale non sono definiti e non hanno senso.

Stabilisco che una formula $cal{A}$ del suddetto linguaggio è ben formata se risulta composta da una sequenza finita di tali simboli, per esempio risultano essere formule ben formate le sequenze $B$, $ABBA$, $ABAABA$. Stabilisco inoltre che la negazione di una formula consiste nella sequenza ordinata delle negazioni dei simboli che ne compongono la sequenza, per esempio $neg ABBA = BAAB$. Qui sto di nuovo utilizzando i simboli $neg$ e $=$ per comodità di illustrazione, tuttavia essi continuano a non fare parte del linguaggio e la formula che li contiene non solo non è ben formata, ma è completamente priva di senso all’interno del linguaggio stesso.

Introduco nel metalinguaggio relativo al linguaggio in oggetto la seguente regola sintattica di deduzione formale: se $cal{A}$ e $cal{B}$ sono formule ben formate non necessariamente tra loro distinte stabilisco che, data l’ipotesi che tali formule siano vere, è dimostrabilmente vera anche la formula ben formata $cal{A}cal{B}$ ottenuta giustapponendo le due sequenze corrispondenti. In simboli ${cal{A}, cal{B}} vdash cal{A}cal{B}$. Per esempio sono dimostrazioni valide ${ A, AB } vdash AAB$ e anche ${A, AB} vdash ABA$. È una dimostrazione valida anche $ { A } vdash AA$, dove le due formule contenute nell’ipotesi coincidono.

Poiché il mio linguaggio di partenza è tanto povero da non contenere né un simbolo di congiunzione, né un simbolo di implicazione è impossibile mappare sintatticamente tale regola di deduzione all’interno del linguaggio stesso tramite un qualsivoglia (meta)teorema di deduzione, ottenendo per esempio una formula del tipo $( A land AB ) to AAB$.

Sempre all’interno del metalinguaggio introduco il seguente criterio semantico: sono vere tutte le formule ben formate del linguaggio in oggetto la cui sequenza inizia con il simbolo $A$ e sono al converso false tutte le formule ben formate la cui sequenza inizia con il simbolo $B$. Si verifica subito come la negazione di una formula vera sia falsa e viceversa, il linguaggio viene dunque semanticamente fondato su di una logica di tipo classico a due valori, la quale attribuisce un ben definito valore di verità a qualunque formula ben formata.

A questo punto posso utilizzare questo semplice linguaggio per costruire un’altrettanto semplice teoria mediante l’introduzione di due assiomi ${A, AB}$. Reinterpretati in questa teoria i tre esempi di deduzione formale presentati sopra si trasformano nella dimostrazione di tre teoremi, le cui tesi ${AAB, ABA, AA}$ risultano dunque essere formule dimostrabili.

Faccio notare come la teoria è sintatticamente consistente, cioè non è in grado di dimostrare sia una formula che la rispettiva negazione, ed è inoltre semanticamente consistente, cioè in grado di dimostrare soltanto formule vere, dato che per giustapposizione di sole sequenze che iniziano con il simbolo $A$ è impossibile ottenere una sequenza che inizi con il simbolo $B$, ma noto anche che tale teoria non è in grado di dimostrare tutte le formule vere ed è perciò incompleta, dato che per giustapposizione di sequenze ottenute a partire da $A$ e $AB$ è impossibile ottenere una formula che contenga più di un simbolo $B$ consecutivo e alcune tra queste formule che risultano sintatticamente indimostrabili sono semanticamente vere: tutte quelle che cominciano con $A$. Per esempio la formula $ABB$ è vera, ma non è ottenibile per giustapposizione a partire dagli assiomi e quindi non è dimostrabile all’interno della teoria. Si tratta pertanto di una formula vera che risulta però non dimostrabile nella teoria stessa, come non ne è dimostrabile la negazione $BAA$ semanticamente falsa, la formula $ABB$ è dunque indecidibile nella teoria stessa.

Avendo trovato una formula indecidibile posso ora estendere la teoria di partenza in modo standard aggiungendo la formula vera $ABB$ agli altri assiomi, la teoria che ne risulta è in grado di dimostrare tutte le formule dimostrate dalla teoria originaria e in più dimostra altre formule semanticamente vere contenenti due simboli $B$ consecutivi, per esempio ${ABB, A} vdash ABBA$. Tuttavia anche questa teoria è incompleta, non potendo dimostrare formule vere contenenti tre o più simboli $B$ consecutivi, per esempio $ABBB$.

Posso però anche estendere la teoria di partenza in modo non-standard aggiungendo agli assiomi la formula semanticamente falsa $BAA$ che nega la formula indecidibile. La teoria risultante dimostra anch’essa tutte le formule dimostrate dalla teoria originaria, oltre ad alcune formule addizionali che sono semanticamente vere (per esempio ${AB, BAA} vdash ABBAA$), ma in più dimostra anche alcune altre formule che sono semanticamente false poiché le relative sequenze iniziano con il simbolo $B$ (per esempio ${AB, BAA} vdash BAAAB$). Dunque quest’altra teoria dimostra formule false e non è semanticamente consistente, ma è anch’essa sintatticamente consistente come lo erano la teoria di partenza e l’estensione standard, infatti non è difficile mostrare che non è possibile al suo interno ottenere una contraddizione, cioè non è possibile dimostrarvi al contempo una formula e la relativa negazione. Di conseguenza è per esempio impossibile dimostrare all’interno della teoria non-standard la formula $ABB$, che pure è semanticamente vera, dato che la sua negazione $BAA$ è stata assunta come assioma ed è dunque sintatticamente dimostrabile.

Se invece aggiungessi come assioma alla teoria d’origine la negazione di una qualche formula dimostrabile, per esempio $BBA$, otterrei una teoria inconsistente nella quale è ovviamente possibile dimostrare contemporaneamente una formula e la sua negazione, per esempio $AAB$ che abbiamo dimostrato sopra a partire dagli assiomi e il nuovo assioma $BBA$. Il sistema di deduzione di questa teoria inconsistente è troppo poco potente per renderla automaticamente esplosiva a seguito della presenza di contraddizioni, in essa non tutte le formule ben formate vi risultano dimostrabili, per esempio la formula $B$ non lo è.

Una teoria effettivamente esplosiva, cioè una teoria in cui qualunque formula ben formata è dimostrabile, si ottiene per altro facilmente assumendo come assiomi le formule contraddittorie ${ A, B }$.

Ora interpretiamo il simbolo $A$ con la cifra $1$, il simbolo $B$ con la cifra $0$, una sequenza $cal{A}$ come un numero intero scritto da destra a sinistra in notazione binaria (nella traduzione perdiamo le sequenze che terminano con uno o più simboli $B$), la nozione semantica di vero con la nozione aritmetica di numero dispari e la nozione semantica di falso con la nozione aritmetica di numero pari. Occorrerà modificare gli assiomi opportunamente in modo da evitare di perdere del tutto la cifra $0$. Resta come esercizio per il lettore descrivere come si traduca in questa interpretazione la regola di deduzione, sempre che la cosa sia possibile dopo aver perso gli zeri iniziali.

Sorry, the comment form is closed at this time.