Teoria del primo ordine: differenze tra le versioni

* un '''[[alfabeto]]''', ovvero un insieme finito di simboli,

* un '''[[linguaggio del primo ordine]]''' costituito da un insieme di [[Formula ben formata|formule ben formate]] che rappresentano enunciati di senso compiuto,

* un insieme di '''[[assiomi logici]]''', cioè un insieme di [[Formula ben formata|formule]] che esprimono le relazioni logiche relative ai [[connettivo logico|connettivi logici]] e ai [[quantificatore|quantificatori]],

* un insieme di '''[[assiomi propri]]''' che stabiliscono alcune relazioni fondamentali tra gli oggetti della teoria non deducibili dagli assiomi logici (come l'assioma "per due punti passa una e una sola retta"),

* un insieme di '''[[regola di inferenza|regole di inferenza]]''' che stabiliscono quando una formula è una conseguenza logica di altre formule.

Una ''dimostrazione'' di una formula <math>\varphi</math> in una teoria del primo ordine '''T''' è una sequenza ordinata di formule

* ogni formula <math>\varphi_i</math> o è un ''assioma'' di '''T''' o è deducibile da una o più formule ad essa precedenti mediante una [[regola di inferenza]].

Una formula che ha una ''dimostrazione formale'' in '''T''' si dice '''dimostrabile''' o '''derivabile'''. Se la formula <math>\varphi</math> è dimostrabile in '''T''' si usa la notazione

Una ''teoria del primo ordine'' '''T''' si dice:

* '''sintatticamente completa''' se per ogni formula <math>\varphi</math> si ha

* '''sintatticamente consistente''' se non esiste nessuna formula <math>\varphi</math> per cui si ha