Logica matematica/Sistemi formali

Introduciamo, a questo punto, la nozione di logica o sistema formale. Ne diamo dapprima la definizione, per passare poi ad alcune considerazioni sulla semantica e sulla nozione di deduzione; mettiamo infine a confronto l'aspetto della deduzione e della semantica nei sistemi formali.

Definizione

Diamo la definizione di sistema formale o sistema logico o, più semplicemente, logica.

Definizione

Una logica $\Lambda$ è definita da

• Un insieme non vuoto (finito o al più numerabile) ${\mathcal {A}}$ di simboli, detto alfabeto di $\Lambda$. Una sequenza finita di elementi di ${\mathcal {A}}$ è detta espressione di $\Lambda$.
• Un sottoinsieme ${\mathcal {F}}$ delle espressioni di $\Lambda$ chiamato insieme delle formule ben formate (o più semplicemente formule) di $\Lambda$.
• Un sottoinsieme $Ax$ di ${\mathcal {F}}$, detto insieme degli assiomi logici o assiomi di $\Lambda$.
• Un insieme finito ${\mathcal {R}}$ di relazioni $R_{1},...,R_{n}$ tra formule di $\Lambda$, dette regole di inferenza. Per ciascuna $R_{i}$ di ${\mathcal {R}}$ esiste un unico intero positivo $j$ tale che, per ogni insieme costituito da $j$ formule e per ogni formula $A$, si può effettivamente decidere se le $j$ formule sono in relazione $R_{i}$ con $A$. In caso positivo, $A$ è detta conseguenza diretta delle $j$ formule date mediante $R_{i}$.

Linguaggio e semantica

L'insieme ${\mathcal {F}}$ delle formule ben formate costituisce il linguaggio ${\mathcal {L}}$ della logica. Generalmente ${\mathcal {F}}$ viene definito in modo induttivo.

La costruzione induttiva dell'insieme delle formule ben formate ci garantisce una proprietà chiamata composizionalità del linguaggio, che è molto importante per associare un significato alle formule.

Normalmente, ogni linguaggio (pensiamo all'italiano piuttosto che all'inglese o a un linguaggio di programmazione) associa al suo insieme di simboli iniziali un significato. Ad esempio, in Pascal, l'insieme dei simboli iniziali è l'insieme delle parole riservate, e a ciascun simbolo è associato un comando. Così, in italiano, come in tutte le lingue parlate, possiamo considerare le parole (il vocabolario) come l'insieme dei simboli iniziali e, ovviamente, ogni parola assume un significato rispetto al mondo reale. Tuttavia, quando mettiamo insieme le parole, e con esse costruiamo una frase per mezzo di opportuni costruttori linguistici, l'interpretazione della frase dipende non solo dal significato delle parole, ma dalla costruzione stessa della frase.

Pertanto, quando parliamo di "interpretazione" di un linguaggio, ci riferiamo sia al significato associato ai suoi simboli iniziali, sia all'estensione di tale significato alle frasi del linguaggio per mezzo dei costruttori del linguaggio. In tal modo, anche l'interpretazione ha un carattere composizionale.

Nel caso di un sistema formale, individuare il significato dei simboli iniziali ed estendere tale significato, mediante i costruttori del linguaggio, alle formule ben formate vuol dire fornire il sistema formale di una semantica. Associare ad una frase una semantica significa determinare il contesto d'interpretazione della frase; a tale scopo viene fornito un insieme ${\mathcal {B}}$, detto insieme dei valori di verità, che contiene almeno due elementi, e un insieme ${\mathcal {T}}$, sottoinsieme proprio di ${\mathcal {B}}$ (${\mathcal {T}}\subset {\mathcal {B}}$), detto insieme designato a rappresentare il vero. La semantica per le frasi verrà fornita definendo un'opportuna funzione (detta funzione di interpretazione) che le mappa in ${\mathcal {B}}$.

Solitamente, ${\mathcal {B}}$ contiene esattamente due elementi (${\mathcal {B}}=\{\mathrm {T} ,\mathrm {F} \}$): in tal caso, la logica è detta "a due valori di verità", $\mathrm {T}$ sta per il vero, $\mathrm {F}$ sta per il falso; ma può anche contenerne tre, quattro, o un qualunque numero finito o infinito (anche non numerabile, come nel caso delle logiche "fuzzy"); ${\mathcal {T}}$ è l'insieme dei valori che designano il vero. Nel caso della logica a due valori di verità, cioè nel caso ${\mathcal {B}}=\{\mathrm {T} ,\mathrm {F} \}$, si avrà ${\mathcal {T}}=\{\mathrm {T} \}$.

Alternativamente alle funzioni di interpretazione, si può studiare il significato di una formula in una "struttura" matematica o "realtà": invece di una notazione funzionale, si adotta una notazione relazionale, basata sulla relazione di soddisfacibilità $\models$, dove $\models \subseteq {\mathcal {M}}\times {\mathcal {F}}$; ${\mathcal {M}}$ è una struttura e ${\mathcal {M}}\models A$ si legge "${\mathcal {M}}$ modella $A$". In questo contesto scriveremo $\vDash A$, e si leggerà "$A$ è valida", sse ${\mathcal {M}}\models A$ vale per ogni ${\mathcal {M}}$.

Rimandiamo una definizione più dettagliata a quando presenteremo le varie logiche, ovvero daremo un carattere più preciso ai costruttori del linguaggio e alle strutture.

Apparato deduttivo

Vediamo ora com'è possibile manipolare una logica $\Lambda$ utilizzando categorie formali o nozioni metalogiche, come regole di inferenza e assiomi, e mediante questi definire un sottoinsieme interessante di formule ben formate, cioè i teoremi di $\Lambda$. Introdurremo prima la nozione di dimostrazione, poi quella di teorema.

Le regole di inferenza di ${\mathcal {R}}$ spesso vengono scritte nella seguente forma:

${\frac {A_{1}...A_{n}}{A}}$

dove le formule scritte al di sopra della riga orizzontale vengono chiamate premesse della regola e la formula scritta al di sotto della riga è detta la sua conclusione.

L'insieme $Ax$ degli assiomi di una logica $\Lambda$ può essere vuoto, finito o infinito. Particolarmente interessante è il caso in cui $Ax$ è finito o descrivibile in maniera finita, cioè è decidibile.

Talvolta gli assiomi vengono scritti come regole di inferenza senza premesse, cioè se $A\in Ax$ scriveremo:

${\overline {A}}$

Definizioni

Dimostrazione

Definizione

Una sequenza finita di formule $A_{1},...,A_{n}$ di $\Lambda$ è detta dimostrazione o prova in $\Lambda$ se, per ogni $i$ compreso tra $1$ ed $n$, o $A_{i}\in Ax$, cioè è un assioma di $\Lambda$, oppure è una conseguenza diretta, mediante una delle regole di ${\mathcal {R}}$, di alcune delle formule che la precedono nella sequenza.

Teorema

Definizione

Una formula $A$ di $\Lambda$ è detta teorema di $\Lambda$ se esiste una dimostrazione di $\Lambda$ che ha $A$ come ultima formula. Tale dimostrazione è detta una dimostrazione di $A$ in $\Lambda$.

Indicheremo con $\vdash A$ il fatto che $A$ è un teorema di $\Lambda$. In caso di ambiguità, scriveremo $\vdash _{\Lambda }A$ oppure $\vdash _{\mathcal {R}}A$, a sottolineare che $A$ ha una dimostrazione in $\Lambda$, oppure che $A$ ha una dimostrazione mediante regole di ${\mathcal {R}}$. $\vdash _{\Lambda }A$ si legge anche: $A$ è derivabile in $\Lambda$; $\vdash _{\mathcal {R}}A$ si legge anche: $A$ è derivabile mediante ${\mathcal {R}}$.

Conseguenza

Definizione

Sia $\Gamma$ un insieme di formule, cioè $\Gamma \subseteq {\mathcal {F}}$. Diciamo che una formula $A$ è conseguenza di $\Gamma$ (scriviamo $\Gamma \vdash A$, che si legge "$A$ si deriva da $\Gamma$") se esiste una sequenza di formule $A_{1},...,A_{n}$ tale che $A$ è $A_{n}$ e per ciascun $i$ compreso tra $1$ ed $n$ si ha che o $A_{i}\in Ax$, o $A_{i}\in \Gamma$, o $A_{i}$ è conseguenza diretta di alcune delle formule che la precedono nella sequenza.

Tale sequenza è detta una derivazione o prova di $A$ da $\Gamma$ in $\Lambda$. Gli elementi di $\Gamma$ sono detti premesse, o ipotesi, o anche assunzioni di $A$. Se $\Gamma$ è un insieme finito $B_{1},...,B_{n}$, scriviamo indifferentemente $\{B_{1},...,B_{n}\}\vdash A$ oppure $B_{1},...,B_{n}\vdash A$.

Si noti come un teorema altro non è se non una formula derivabile "per via di logica", cioè una derivazione da un insieme di assunzioni $\Gamma$ vuoto: scrivere $\vdash A$ equivale a scrivere $\emptyset \vdash A$.

Chiusura deduttiva

Definizione

Sia $\Gamma$ un insieme di formule. La chiusura deduttiva di $\Gamma$, denotata con $Cn(\Gamma )$, è l'insieme di tutte le formule che sono conseguenza di $\Gamma$ (cioè $Cn(\Gamma )=\{A|\Gamma \vdash A\}$).

Consistenza

Definizione

Sia $\Gamma$ un insieme di formule. $\Gamma$ è consistente sse $Cn(\Gamma )$ è un sottoinsieme proprio di ${\mathcal {F}}$ (cioè $Cn(\Gamma )=\{A|\Gamma \vdash A\}\subset {\mathcal {F}}$).

Proprietà

La nozione di conseguenza, in una logica $\Lambda$, può godere di una o più delle seguenti proprietà.

• Se $A\in \Gamma$ allora $\Gamma \vdash A$, o anche, se $A\in \Gamma$ allora $A\in Cn(\Gamma )$, dunque $\Gamma \subseteq Cn(\Gamma )$ (questa proprietà è detta inclusione);

• Se $\Gamma \subseteq \Delta$ e $\Gamma \vdash A$ allora $\Delta \vdash A$, o anche $Cn(\Gamma )\subseteq Cn(\Delta )$ (questa proprietà è detta monotonia);
• $\Gamma \vdash A$ se e solo se esiste un sottoinsieme finito $\Delta$ di $\Gamma$ tale che $\Delta \vdash A$ (questa proprietà è detta compattezza);
• Se $\Delta \vdash A$ e per ogni $B$ di $\Delta$ si ha che $\Gamma \vdash B$, allora si ha che $\Gamma \vdash A$ (questa proprietà è detta taglio sulle premesse).

In una logica in cui sia presente un operatore di implicazione può inoltre valere un teorema di deduzione, cioè

$\Gamma \vdash A\to B$ sse $\Gamma ,A\vdash B$

Notare che in logica un teorema è una formula derivabile nel linguaggio. Una proprietà del linguaggio e delle sue formule non è quindi un teorema, ma un metateorema. Le proprietà che abbiamo sopra enunciato, nel caso valgano per una logica $\Lambda$, sono metateoremi per $\Lambda$.

Nel seguito, la parola "dimostrazione" verrà usata con un duplice significato: una "dimostrazione" in una logica $\Lambda$ è una sequenza di formule di $\Lambda$ che porta ad un teorema di $\Lambda$ (coerentemente con le definizioni di dimostrazione e teorema sovraesposte); una "dimostrazione" di un metateorema che concerne una logica $\Lambda$ è una sequenza di argomentazioni usata per provare una proprietà di cui la logica $\Lambda$ gode.

Considerazioni sui sistemi formali

In genere, le formule di un insieme $\Gamma$ sono intese rappresentare una data realtà. In questo caso, tutte le strutture in cui le formule di $\Gamma$ sono verificate sono dette modelli di $\Gamma$ e l'insieme $\Gamma$ è detto insieme degli assiomi propri associati a tali modelli. Quindi, rappresentare una data realtà in un sistema formale $\Lambda$ significa individuare un insieme di formule di $\Lambda$ (detti assiomi propri, nel senso che sono "propri" di quella realtà) che hanno quella realtà a modello, non sempre, anzi di rado, modello esclusivo.

Abbiamo visto che una logica si può definire tramite un linguaggio, un insieme di assiomi e un insieme di regole di inferenza. Stabilire, per mezzo degli assiomi e delle regole di inferenza, quali siano le formule "interessanti" della logica, ovvero i teoremi, significa fare "deduzione". I passi necessari a stabilire se una formula è un teorema della logica possono essere espressi tramite un algoritmo, e quindi meccanizzati. Possiamo dire che, in questo modo, stiamo utilizzando il sistema formale come un sistema di deduzione e, quindi, non siamo effettivamente interessati al significato delle formule del linguaggio ma, piuttosto, al modo in cui mettiamo insieme tali formule per costruire una prova diretta oppure, come vedremo spesso in seguito, una refutazione, cioè una prova che la negazione di una certa formula è in contraddizione con gli assiomi e le ipotesi supposte.

Un sistema di deduzione è anche un sistema di calcolo, in quanto esso ci permette di "calcolare" le conclusioni che seguono da premesse date. È in questo senso che la logica proposizionale e quella predicativa sono talvolta dette, rispettivamente, "calcolo delle proposizioni" e "calcolo dei predicati".

Il fatto che i passi di una dimostrazione possano essere posti in forma di algoritmo e meccanizzati non significa che possiamo sempre avere una risposta se una formula è un teorema oppure no, né significa che per costruire una prova non occorra alcuna creatività. Che una procedura di prova termini con una risposta positiva o negativa (a seconda che la formula in questione sia un teorema o meno) dipende dalla logica. Se tale procedura esiste, cioè se l'insieme dei teoremi di una logica è decidibile, diremo che la logica è decidibile.

Abbiamo visto che un linguaggio ha un significato. Possiamo essere interessati a un sistema formale dal punto di vista "del significato", invece che da un punto di vista deduttivo. In altri termini, il linguaggio può servirci per caratterizzare delle strutture. In tal caso siamo interessati alla teoria dei modelli. L'aspetto interessante della teoria dei modelli è che ci porta a dare una caratterizzazione precisa di cos'è la nozione di verità in una struttura.

È chiaro che, così come si possono definire algoritmi associati alle procedure di prova, si possono definire algoritmi associati all'interpretazione di una formula; algoritmi che possono stabilire se una formula è vera in tutte le strutture della logica o meno. Analogamente alle procedure di prova, la possibilità di stabilire effettivamente la validità di una formula dipende dal linguaggio.

È naturale chiedersi che tipo di connessione c'è tra i due modi di utilizzare un sistema formale: quello legato alle dimostrazioni e quello semantico legato ai modelli. La connessione è auspicabile, nel senso che sarebbe per lo meno strano riuscire a provare teoremi e non riuscire a collegarli alle formule valide. Tutto ciò però non è ovvio, nel senso che procedure di deduzione e procedure associate alla validità non sono necessariamente complementari l'una all'altra.

Ad esempio, potremmo avere un insieme infinito di strutture da analizzare per verificare se una certa formula è vera in esse, ma solo un insieme finito di assiomi che descrive tali strutture, e da tale insieme potremmo avere una procedura di prova che ci fornisce una risposta.

Nel primo caso, l'arbitrarietà con cui si può scegliere un modello per un insieme di formule lascia poco spazio alla decidibilità della nozione di validità.

In altre condizioni, potremmo essere interessati a trovare solo un modello per una formula, cioè a verificarne la soddisfacibilità, mentre la procedura di prova non è in grado di darci una risposta se quella formula è un teorema o meno.

In effetti, è proprio l'interazione tra teoria dei modelli e teoria della deduzione che rende un sistema formale interessante: ciò che si può manipolare sintatticamente ha un effettivo riscontro, in termini di nozione di verità, nella realtà in cui il linguaggio è interpretato.

Tale interazione è stabilita dalle seguenti definizioni.

Correttezza e completezza di un apparato deduttivo

Correttezza

Definizione

Un apparato deduttivo ${\mathcal {R}}$ è corretto se, per ogni formula $A\in {\mathcal {F}}$, $\vdash _{\mathcal {R}}A$ implica $\vDash A$.

Completezza

Definizione

Un apparato deduttivo ${\mathcal {R}}$ è completo rispetto a una classe di formule $\Gamma \subseteq {\mathcal {F}}$ se, per ogni formula $A\in \Gamma$, $\vDash A$ implica $\vdash _{\mathcal {R}}A$.

Risultano di particolare interesse le logiche $\Lambda$ e le definizioni di semantiche per cui si possa dimostrare un teorema di correttezza e completezza, ossia una coincidenza tra la nozione semantica di conseguenza (cioè quella basata sui modelli) e quella sintattica (basata sulle dimostrazioni). Tale metateorema talvolta si esemplifica scrivendo: $\vdash \equiv \vDash$.

Il teorema di correttezza e completezza stabilisce una stretta relazione tra il livello sintattico (della deduzione) e quello semantico (dei modelli) per un sistema formale, e stabilisce una stretta analogia tra le nozioni introdotte ai due livelli.

Uso della parola "modello" in logica

Chiudiamo il discorso sui sistemi formali con una riflessione sull'uso della parola "modello" in logica. Nel linguaggio comune, così pure come in quello scientifico, la parola modello ha due distinti e opposti significati; entrambi hanno a che vedere con una rappresentazione e con ciò che è rappresentato. Il problema è che la parola modello è talvolta usata per indicare il primo termine della relazione (la rappresentazione), talvolta il secondo (l'oggetto rappresentato). Così, per esempio, si dice che il manufatto a scala ridotta che rappresenta una barca o un aereo è un modello della barca o dell'aereo. Anche in economia si parla di modello per intendere una rappresentazione matematica del mercato. In Logica matematica, al contrario, la rappresentazione è chiamata teoria e ciò che è rappresentato è chiamato modello. Questo uso è contrario a quello scientifico, ma coincide con quello degli artisti, per esempio i pittori, che parlano di modello per intendere ciò che viene rappresentato, cioè l'oggetto del dipinto (che ne è quindi la rappresentazione).