My teacher presented Gödel's first incompleteness theorem as follows:
(1) First Incompleteness theorem (Gödel [Rosser]):
Every [$\omega$-]consistent and reasonably expressive system of arithmetic contains sentences that are neither provable nor refutable(2) First Incompleteness Theorem (with shades of Tarski): Every sound and reasonably expressive system of arithmetic contains true, but unprovable sentences.
This is still a bit vague, so here the formalisation of a "system of arithmetic":
Def. A system $\Sigma$ is a set containing the following components:
$\mathcal{E} \ldots $ expressions of $\Sigma$
$\mathcal{S} \ldots $ sentences of $\Sigma$; $\mathcal{S} \subseteq \mathcal{E} $
$\mathcal{T} \ldots $ true sentences of $\Sigma$; $\mathcal{T} \subseteq \mathcal{S}$
$\mathcal{P} \ldots $ provable sentences of $\Sigma$; $\mathcal{P} \subseteq \mathcal{S}$
$\mathcal{R} \ldots $ refutable sentences of $\Sigma$; $\mathcal{R} \subseteq \mathcal{S}$
$\mathcal{H} \ldots $ predicates of $\Sigma$; $\mathcal{H} \subseteq \mathcal{E}$
function $\Phi: \mathcal E \times \mathcal H \mapsto \mathcal E$: If $E \in \mathcal H$ then $\Phi(E, n) = E(n) \in \mathcal S$
Def. Soundness: A system is sound iff all provable sentences are true ($\mathcal P \subseteq \mathcal T$) and no refutable sentence is true ($\mathcal R \cap \mathcal T = \emptyset$).
Def. Completeness: A system is complete iff all true sentences are provable ($\mathcal T \subseteq \mathcal P$).
What I am struggling with is how this formalisation translates to FOL and the notion of first-order theories. In particular, how does "true sentence" translate to FOL? Does it mean tautological truth (in all structures)? Truth in a first-order theory (e.g. Peano Arithmetic)? Truth in just some structure (e.g. the standard model for arithmetic)?
I am also interested in how this relates to Gödel's completeness theorem of FOL. For example, if "true sentence" in the above system would mean "tautological truth of FOL", then (2) would contradict Gödel's completeness theorem of FOL. Right?
Best Answer
In the semantics of FOL we have the formal definition of the property of a formula $A$ to be true in a structure $\mathfrak A$.
A formula of FOL is (universally) valid if it is true in every structures (e.g. $\forall x (x=x)$).
A formula of first-order arithmetic like e.g. $\forall n \exists m (n < m)$ is true in the structure $\mathbb N$, but it is not valid.
Thus, when we states the "semantical version" of Gödel’s Incompleteness Theorems we mean that there is a formula $G$ in the language of first-order arithmetic that is true in $\mathbb N$ but not provable (nor refutable) in $\mathsf {PA}$.
Why this fact does not contradict the Completeness Theorem for FOL ?
The theorem states that every valid FOL formula is provable, and that every FOL formula $\varphi$ that is a logical consequence of a set $\Gamma$ of formulas (in symbols : $\Gamma \vDash \varphi$) must be derivable in the calculus from the set $\Gamma$ of assumptions (in symbols : $\Gamma \vdash \varphi$).
The fact that $G$ is not provable in $\mathsf {PA}$, i.e. that $\mathsf {PA} \nvdash G$ means that the formula $G$, that is true in $\mathbb N$ is not a logical consequence of the set $\mathsf {PA}$ of axioms (i.e. that $\mathsf {PA} \nvDash G$).
Thus, there is a non standard model of arithmetic in which $G$ is not true.