finitezza, teoremi di

In logica matematica, data una teoria formale, occorre distinguere un teorema sintattico di f. da uno semantico. Il primo si riferisce ai concetti di derivabilità e di non contraddittorietà, il secondo a quelli di conseguenza logica e di soddisfacibilità. Del teorema sintattico di f. si hanno due formulazioni equivalenti: a) un’espressione A è derivabile da un insieme P di premesse se e solo se A è derivabile da un sottoinsieme finito di P; b) un insieme P di espressioni è non contraddittorio se e solo se è tale ogni sottoinsieme finito di P. In modo analogo si hanno due formulazioni equivalenti del teorema semantico di f.: c) un’espressione A è conseguenza logica di un insieme P di espressioni se e solo se A è conseguenza logica di un sottoinsieme finito di P; d) un insieme P di espressioni è soddisfacibile (esiste cioè almeno un modo di interpretare le espressioni di P che le rende tutte simultaneamente vere) se e solo se ogni sottoinsieme finito di P è soddisfacibile. Questo significa che, dato un qualunque insieme P di espressioni, anche infinito, se per ogni suo sottoinsieme finito esiste un modello, anche l’intero insieme P deve avere un modello. Questa seconda formulazione del teorema, assai importante in teoria dei modelli, è nota anche come teorema di compattezza.