Sistema formale

In logica matematica, la nozione di sistema formale è utilizzata per fornire una definizione rigorosa del concetto di dimostrazione. In altri termini, la nozione di sistema formale corrisponde ad una formalizzazione rigorosa e completa della nozione di sistema assiomatico.

Descrizione[modifica | modifica wikitesto]

Un sistema formale è costituito da:

un alfabeto, ovvero un insieme (finito o numerabile) di simboli;
una grammatica che specifica quali sequenze finite di questi simboli sono formule ben formate. La grammatica deve essere ricorsiva, nel senso che deve esistere un algoritmo per decidere se una sequenza di simboli è o meno una formula ben formata.
un sottoinsieme dell'insieme delle formule ben formate: gli assiomi del sistema formale. Anche in questo caso l'insieme degli assiomi deve essere ricorsivo.
alcune regole, dette regole di inferenza, che associano formule ben formate ad n-uple di formule ben formate. Più dettagliatamente, una regola di inferenza è un sottoinsieme di tutte le n+1-uple di formule ben formate: le prime n formule di ognuna di queste n+1-uple si dicono premesse, mentre l'ultima formula si dice essere una loro conseguenza.

Gli esempi più comuni di sistemi formali sono le teorie del primo ordine.

Dato un sistema formale, l'insieme dei suoi teoremi è definito ricorsivamente come il più piccolo insieme di formule ben formate che sono

assiomi, oppure
possono essere ottenute mediante le regole di inferenza del sistema utilizzando altri teoremi ottenuti in precedenza.

Fin qui si sono utilizzate esclusivamente nozioni sintattiche, ovvero non si è fatto riferimento alcuno alla nozione di verità. Intuitivamente, le formule ben formate rappresentano affermazioni che hanno un senso, e gli assiomi sono affermazioni da considerare vere. Se si suppone che le regole di inferenza portino affermazioni vere in altre affermazioni vere, allora tutti i teoremi sono veri.

È comunque da notare che la definizione di sistema formale (e, quindi, la definizione di dimostrazione) possono essere date indipendentemente dalla nozione di verità.

Anche la nozione di verità può comunque essere formalizzata costruendo una semantica per il sistema formale, ovvero assegnando ad ogni sottoinsieme dell'insieme dei simboli una classe di strutture (o modelli), insieme ad una nozione di soddisfacibilità, che dice quando una formula è vera o falsa in un dato modello.

Assegnare una semantica non è comunque semplice, e non sempre è possibile, se si vuole che vi sia una corrispondenza esatta fra gli enunciati dimostrabili e gli enunciati veri, cioè quelli veri in ogni modello (teorema di completezza), e se si vuole che la definizione di sistema formale continui ad essere ricorsiva.