Sinossi

Nel calcolo dei predicati del primo ordine l'argomento centrale è il problema della soddisfacibilità di una formula o di un insieme di formule. Il principale scopo è dare criteri di soddisfacibilità ed algoritmi per la costruzione di un modello. In questa direzione, il linguaggio scelto sarà il protagonista, nel senso che la soddisfacibilità è strettamente legata al linguaggio considerato e, più il linguaggio sarà povero, più saranno le possibilità di avere formule valide o soddisfacibili. In questo lavoro si studiano due procedure logiche per la soddisfacibilità: la ricerca degli avatars di una formulae la ricerca dei testimoni di Henkin di una teoria. La prima procedura è un algoritmo utile a costruire un modello per la formula considerata, la seconda ha per finalità la dimostrazione del teorema di Gäodel sull'esistenza di un modello per ogni teoria non contraddittoria del 1° ordine. Nell'appendice si danno le definizioni fondamentali sul tipo di similarità di un linguaggio corredate da esempi, si introducono e si studiano i fondamentali linguaggiprovenienti dall'algebra e dalla geometria. Riterremo note le nozioni fondamentali del calcolo dei predicati del primo ordine.