Lug 072012
 

Quanto segue è una serie di considerazioni di metalogica che avevo scritto circa cinque anni fa per motivi che non ricordo più bene e che avevo messo da parte per altri motivi che non ricordo molto bene, ma che avevano vagamente a che fare con le perle e con i suini. Oggi ne ho riesumato la prima parte per testare l’installazione di MathJax, che mi permetterà di sbizzarrirmi con $LaTeX$ e non più solo, come nel titolo, con i font Unicode.

Posta una teoria $mathit{T}$ basata su una logica del primo ordine consistente o paraconsistente, il teorema di deduzione (dimostrabile in modo macchinoso, ma elementare) è una formula meta-meta-teorica che afferma come nella relativa meta-teoria sia possibile inferire a partire da un insieme finito di ipotesi $(mathcal{H} cup { H_n } )$ una tesi $A$ se e solo se a partire dalle sole ipotesi $mathcal{H}$ è anche possibile inferire che $H_n$ implica $A$, cioé che sotto le ipotesi $mathcal{H}$ la formula $H_n rightarrow A$ è dimostrabile. In formule:
$$mathcal{H} := { H_0, H_1, …  H_{n-1} }$$
$$( mathcal{H} cup {H_n} vdash_{mathit{MT}} A ) Leftrightarrow_{mathit{MMT}} ( mathcal{H} vdash_{mathit{MT}} H_n rightarrow A )$$

Poiché le ipotesi sono supposte di numero finito è inoltre possibile applicare successivamente il teorema di deduzione per un numero finito di volte pari a quello delle ipotesi, ottenendo infine:
$$mathcal{H} := { H_0, H_1, …  H_{n} }$$
$$( mathcal{H} vdash_{mathit{MT}} A ) Leftrightarrow_{mathit{MMT}} ( vdash_{mathit{MT}} H_0 rightarrow ( H_1 rightarrow … ( H_{n-1} rightarrow ( H_n rightarrow A ) ) … ) ) $$

Poiché una teoria (para)consistente dimostra solo formule valide (cioè identicamente vere in ogni modello della teoria stessa) è inoltre possibile ricavare:
$$(mathcal{H} vdash_{mathit{MT}} A ) Leftrightarrow_{mathit{MMT}} ( models H_0 rightarrow ( H_1 rightarrow … ( H_{n-1} rightarrow ( H_n rightarrow A ) ) … ) ) $$
vale a dire che il teorema $mathcal{H}  vdash_{mathit{MT}} A$ è equivalente, a livello meta-meta-teorico, all’affermazione che $H_0 rightarrow ( H_1 rightarrow … ( H_{n-1} rightarrow ( H_n rightarrow A ) ) … )$ sia una formula valida della teoria.

A questo punto si può anche osservare che sotto ipotesi abbastanza generali sulla forma dei connettivi logici è possibile dimostrare i teoremi seguenti:
$$( A rightarrow ( B rightarrow C ) ) vdash ( B rightarrow (A rightarrow C) )$$
$$( A rightarrow (B rightarrow C) ) vdash ( A land B rightarrow C )$$
$$( A land B rightarrow C ) vdash ( A rightarrow (B rightarrow C) )$$
che permettono di riformulare l’ultimo meta-teorema nella forma più semplice:
$$(mathcal{H} vdash_{mathit{MT}} A ) Leftrightarrow_{mathit{MMT}} ( models ( H_0 land H_1 land … H_{n-1} land H_n ) rightarrow A ) Leftrightarrow_{mathit{MMT}} ( models bigwedgemathcal{H} rightarrow A )$$
In particolare quanto sopra vale per la logica classica, per la logica di Heyting, per la logica trivalente di Łukasiewicz e per la logica tetravalente di Belnap (le prime due consistenti, le ultime due paraconsistenti). Di qui in avanti supporremo per semplicità di aver fondato la nostra teoria su una logica i cui connettivi soddisfino i teoremi precedenti.

Riassumendo, si verifica dunque a livello meta-meta-teorico come un teorema della teoria $T$ sia equivalente all’affermazione che una corrispondente formula sia valida nella teoria $T$ stessa:
$$(mathcal{H} vdash_{mathit{MT}} A ) Leftrightarrow_{mathit{MMT}} ( models bigwedgemathcal{H} rightarrow A )$$
cioè che tutti i teoremi siano rappresentabili come formule valide all’interno della teoria $T$, cosa che evita ai matematici di dover mantenere sempre ben distinte le affermazioni teoriche da quelle meta-teoriche, rendendo ancora più lunghe e complesse le proprie dimostrazioni.

Ricordiamo a questo punto che gli assiomi di una teoria $T$ sono un insieme di formule assunte come valide senza dimostrazione. Una struttura che funga da modello della teoria $T$ renderà identicamente vere tali formule.

Orbene, una teoria $T’$ che abbia come assiomi tutti gli assiomi di $T$ con l’aggiunta della proposizione $bigwedgemathcal{H} rightarrow A$, dove $mathcal{H} vdash_{mathit{MT}} A$ è un teorema di $T$, possiede come modelli tutte e sole le strutture che sono modello della teoria $T$ di partenza, dato che:

  1. qualunque modello della teoria di origine rende per definizione vera una qualunque proposizione valida, inclusi ovviamente gli assiomi, e quindi è modello anche della nuova teoria
  2. qualunque modello della nuova teoria rende vere tutte le sue proposizioni valide, che comprendono tutti gli assiomi della teoria di origine e le loro conseguenze logiche, ed è quindi modello anche di quest’ultima

In conclusione, dato un qualunque teorema di una teoria $T$ della forma $mathcal{H} vdash_{mathit{MT}} A$, siamo elementarmente in grado di costruire una teoria $T’$ che ha come assiomi tutti gli assiomi di $T$ e in più la formula (valida in $T$) $bigwedgemathcal{H} rightarrow A$. Tale teoria $T’$ avrà come modelli tutte e sole le strutture che sono modello di $T$, risultando a essa equivalente e potendo essere identificata con $T$ per tutti i fini pratici.

Sorry, the comment form is closed at this time.