Mar 022014
 

Il linguaggio introdotto nella prima parte per illustrare l’indecidibilità e i modelli non standard, e fuffa di vario genere nella seconda è estremamente primitivo e non permette di rappresentare pressoché nulla al proprio interno, se non sequenze finite composte dalle lettere ${ A, B }$, ottenute tramite giustapposizione a partire dagli assiomi iniziali.

Date le regole semantiche utilizzate per interpretare i valori di verità delle sue formule non risulta molto complicato introdurre al suo interno il nuovo simbolo di negazione $neg$ tramite la seguente definizione, accennata nella prima parte:

$
begin{aligned}
neg A & := B\
neg B & := A\
neg({cal AB}) & := neg{cal A neg B}
end{aligned}
$

In sostanza il simbolo $neg$ applicato a una formula trasforma tutte le lettere $A$ in $B$ e viceversa.

Date le premesse questa è una definizione naturale e per nulla problematica, ma le cose cambiano quando si vogliano introdurre nel linguaggio simboli logici più complessi che permettano di esprimere, per esempio, i connettivi $land$ (AND) e $lor$ (OR) e l’implicazione $rightarrow$, il modo più naturale di farlo, infatti, tende a far collassare l’intero linguaggio sull’algebra booleana elementare dove ognuna delle formule originarie del linguaggio, le sequenze di lettere $A$ e $B$, possono essenzialmente essere tutte identificate con la sola lettera iniziale senza perdità di generalità.

Non ho ancora escogitato un buon modo per estendere il linguaggio in modo non banale, sempre che la cosa sia possibile, quindi riservo un’eventuale estensione di questo genere per la quarta parte. Qui illustrerò l’estensione banale più naturale cominciando con il definire l’operatore di Sheffer $uparrow$ (NAND) nel modo seguente:

$
begin{aligned}
A{cal A} uparrow A{cal B} & := B({cal A uparrow B})\
A{cal A} uparrow B{cal B} & := A({cal A uparrow B})\
B{cal A} uparrow A{cal B} & := A({cal A uparrow B})\
B{cal A} uparrow B{cal B} & := A({cal A uparrow B})
end{aligned}
$

dove $cal{A}$ e $cal{B}$ sono formule generiche oppure la stringa vuota — che di per sé sola non fa parte del linguaggio — e si intende vigente l’estensione $“” uparrow cal{A} = cal{A} uparrow “” = negcal{A}$, cioè l’operatore di Sheffer applicato a una stringa vuota e a una formula generica ha per risultato la negazione della suddetta formula generica.

Applicando la definizione si ottengono per esempio le formule particolari seguenti;

$
begin{aligned}
A uparrow A & = B\
A uparrow B & = A\
B uparrow A & = A\
B uparrow B & = A\
A uparrow BAA & = A(“” uparrow AA) = ABB\
AB uparrow AABA & = B(B uparrow ABA) = BA(“” uparrow BA) = BAAB
end{aligned}
$

Armati con tale operatore siamo ora in grado di definire gli operatori logici più comuni nel modo usuale:

$
begin{aligned}
neg{cal A} & := {cal A uparrow A}\
{cal A land cal B} & := {cal (A uparrow B) uparrow (A uparrow B)}\
{cal A lor cal B} & := {cal (A uparrow A) uparrow (B uparrow B)}\
{cal A rightarrow cal B} & := {cal A uparrow ( B uparrow B)}
end{aligned}
$

Non è difficile verificare che questa seconda definizione di negazione è perfettamente consistente e fornisce lo stesso risultato di quella espressa più sopra, nonché che i connettivi logici così definiti sono consistenti con l’attribuzione del valore di verità a ciascuna formula così come decretato nella prima parte (tutte le formule che iniziano con $A$ sono vere, tutte le formule che iniziano con $B$ sono false). Valgono infatti le seguenti relazioni:

$
begin{aligned}
neg A{cal A} & = (A{cal A} uparrow A{cal A}) = B({cal A} uparrow {cal A}) = Bneg{cal A}\
neg B{cal A} & = (B{cal A} uparrow B{cal A}) = A({cal A} uparrow {cal A}) = Aneg{cal A}\
end{aligned}
$

$
begin{aligned}
A{cal A} land A{cal B} & = (A{cal A} uparrow A{cal B}) uparrow (A{cal A} uparrow A{cal B}) = B({cal A} uparrow {cal B}) uparrow B({cal A} uparrow {cal B}) = A({cal A} land {cal B})\
A{cal A} land B{cal B} & = (A{cal A} uparrow B{cal B}) uparrow (A{cal A} uparrow B{cal B}) = A({cal A} uparrow {cal B}) uparrow A({cal A} uparrow {cal B}) = B({cal A} land {cal B})\
B{cal A} land B{cal B} & = (B{cal A} uparrow B{cal B}) uparrow (B{cal A} uparrow B{cal B}) = A({cal A} uparrow {cal B}) uparrow A({cal A} uparrow {cal B}) = B({cal A} land {cal B})\
end{aligned}
$

$
begin{aligned}
A{cal A} lor A{cal B} & = (A{cal A} uparrow A{cal A}) uparrow (A{cal B} uparrow A{cal B}) = B({cal A} uparrow {cal A}) uparrow B({cal B} uparrow {cal B}) = A({cal A} lor {cal B})\
A{cal A} lor B{cal B} & = (A{cal A} uparrow A{cal A}) uparrow (B{cal B} uparrow B{cal B}) = B({cal A} uparrow {cal A}) uparrow A({cal B} uparrow {cal B}) = A({cal A} lor {cal B})\
B{cal A} lor B{cal B} & = (B{cal A} uparrow B{cal A}) uparrow (B{cal B} uparrow B{cal B}) = A({cal A} uparrow {cal A}) uparrow A({cal B} uparrow {cal B}) = B({cal A} lor {cal B})
end{aligned}
$

$
begin{aligned}
A{cal A} rightarrow A{cal B} & = A{cal A} uparrow (A{cal B} uparrow A{cal B}) = A{cal A} uparrow B({cal B} uparrow {cal B}) = A({cal A} rightarrow {cal B})\
A{cal A} rightarrow B{cal B} & = A{cal A} uparrow (B{cal B} uparrow B{cal B}) = A{cal A} uparrow A({cal B} uparrow {cal B}) = B({cal A} rightarrow {cal B})\
B{cal A} rightarrow A{cal B} & = B{cal A} uparrow (A{cal B} uparrow A{cal B}) = B{cal A} uparrow B({cal B} uparrow {cal B}) = A({cal A} rightarrow {cal B})\
B{cal A} rightarrow B{cal B} & = B{cal A} uparrow (B{cal B} uparrow B{cal B}) = B{cal A} uparrow A({cal B} uparrow {cal B}) = A({cal A} rightarrow {cal B})\
end{aligned}
$

Tramite questa estensione del linguaggio con connettivi e operatori logici siamo ora in grado di esprimere i teoremi della teoria all’interno della teoria stessa tramite opportune regole e di verificare se le formule risultanti siano logicamente vere all’interno della teoria stessa.

In particolare vorremmo esprimere un qualsiasi teorema, per esempi ${AB, A} vdash ABA$, tramite teoremi equivalenti in cui ipotesi, tesi e dimostrazione siano tutte espresse in una semplice formula tramite il solo linguaggio della teoria, senza ricorrere esplicitamente alla metateoria se non nel momento in cui si dichiari che tale semplice formula è un teorema; per esempio $vdash AB rightarrow (A rightarrow ABA)$ o, più simmetricamente, $vdash (AB land A)rightarrow ABA$.

Sì dà il caso che quanto espresso dal paragrafo precedente sia noto come “(meta)teorema di deduzione” e che la (meta)dimostrazione di tale teorema sia un po’ tediosa per motivi tecnici, ma assolutamente standard per un linguaggio del tipo di quello in esame, che si riduce essenzialmente a un particolare modello del calcolo proposizionale classico. Purtroppo capita anche che un tale modello attribuisca a tutte le proprie formule il valore di verità che ci si aspetta a priori, che estenda le regole di deduzione del metalinguaggio — da me artificialmente limitate nella prima parte — a tutte quelle valide nella teoria classica della dimostrazione, e che pertanto tale linguaggio cessi immediatamente di essere interessante.

Tanto per curiosità calcoliamo il valore della formula $AB rightarrow (A rightarrow ABA) = AB rightarrow ABA = AAA$ e quello della formula $(AB land A)rightarrow ABA = AB rightarrow ABA = AAA$, notando come entrambi i risultati forniscano la medesima formula vera, così come per altro $A rightarrow (AB rightarrow ABA) = A rightarrow AAA = AAA$.

Sorry, the comment form is closed at this time.