Assioma logico

Gli assiomi logici sono un insieme (infinito) di assiomi di una teoria del primo ordine che formalizzano tutte le deduzioni logiche che solitamente si fanno nelle dimostrazioni matematiche. Ci sono diversi modi di ottenere questo tipo di formalizzazione. Uno di questi è dato dal seguente insieme di assiomi:

Per ogni formula ben formata ${\mathcal {A}},{\mathcal {B}},{\mathcal {C}}$ sono assiomi logici le chiusure universali delle fbf:

(L1) ${\mathcal {A}}\to ({\mathcal {B}}\to {\mathcal {A}})$

(L2) $({\mathcal {A}}\to ({\mathcal {B}}\to {\mathcal {C}}))\to (({\mathcal {A}}\to {\mathcal {B}})\to ({\mathcal {A}}\to {\mathcal {C}}))$

(L3) $(\neg {\mathcal {A}}\to \neg {\mathcal {B}})\to ({\mathcal {B}}\to {\mathcal {A}})$

(L4) $(\forall x{\mathcal {A}})\to {\mathcal {A}}$ per ogni fbf ${\mathcal {A}}$ in cui $x$ non è una variabile libera

(L5) $(\forall x{\mathcal {A}}(x))\to {\mathcal {A}}(t)$ per ogni fbf ${\mathcal {A}}$ e per ogni termine $t$ che non contiene una variabile libera di ${\mathcal {A}}$

(L6) $(\forall x({\mathcal {A}}\to {\mathcal {B}}))\to ((\forall x{\mathcal {A}})\to {\mathcal {B}})$ per ogni fbf ${\mathcal {A}}$ in cui $x$ non è variabile libera.

Notare che si tratta di schemi di assiomi, ciascuno dei quali ha infinite diverse istanze.

L'insieme di assiomi definito sopra vale per un linguaggio del primo ordine dotato dei simboli per connettivi logici e quantificatori "$\to$", "$\neg$" e "$\forall$". Esso ed è sufficiente a formalizzare in una teoria del primo ordine tutti i tipi di deduzioni logiche se la teoria è dotata della sola regola di inferenza chiamata modus ponens che consente, date fbf ${\mathcal {A}}\to {\mathcal {B}}$ e ${\mathcal {A}}$ di derivare la fbf ${\mathcal {B}}$. Il teorema di completezza per il calcolo dei predicati assicura infatti che in una teoria del primo ordine dotata di questi assiomi si possono dedurre tutte le fbf logicamente valide.

Se il linguaggio del primo ordine include simboli per gli altri connettivi e quantificatori occorre aggiungere assiomi che colleghino i nuovi connettivi e quantificatori con quelli usati fino ad ora:

(L7) $\exists x{\mathcal {A}}\leftrightarrow \neg (\forall x\neg {\mathcal {A}})$

(L8) $({\mathcal {A}}\land {\mathcal {B}})\leftrightarrow (\neg ({\mathcal {A}}\to (\neg {\mathcal {B}})))$

(L9) $({\mathcal {A}}\lor {\mathcal {B}})\leftrightarrow ((\neg {\mathcal {A}})\to {\mathcal {B}})$