Il calcolo ℱ

• Il calcolo logico ℱ consiste nelle argomentazioni provabili in Fitch usando tutte e sole le regole di introduzione ed eliminazione dei connettivi, dei quantificatori e dell'identità

$$ P_1,..., P_n\vdash_{FO} Q $$

• Questa notazione indica che esiste una prova in ℱ con premesse P1, ..., Pn e conclusione Q

Teorema di validità (soundness)

$$ Se\ P_1,..., P_n \vdash_{FO}Q,\ allora\ P_1,..., P_n\models_{FO}Q $$

Teorema di completezza (completness)

$$ Se\ P_1,..., P_n\models_{FO} Q,\ allora\ P_1,..., P_n\vdash_{FO}Q $$

Teorie infinite

<aside> 💡 Il teorema di validità e completezza vale anche per teorie infinite.

</aside>

$$ \Gamma\vdash_{FO}Q\ se\ e\ solo\ se\ \Gamma\models_{FO}Q $$

Teorema di validità e completezza applicato a PA

Sia 𝛤(PA) l'insieme {PA1, ..., PA6} ∪ {PA7(P): per ogni fbf P(x)}

$$ P_1,..., P_n \vdash_{PA} Q\ se\ e\ solo\ se\ \Gamma(PA), P_1,..., P_n\vdash_{FO}Q $$

Allora

$$ \vdash_{PA}Q\ se\ e\ solo\ se\ \Gamma(PA)\models_{FO}Q $$

• Se e solo se Q è vero in S per ogni modello S di 𝛤(PA)