2
$\begingroup$

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?

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Okay, so when we say "every sound and reasonably expressive system of arithmetic contains true, but unprovable sentences", we really mean that it contains sentences that are true in the standard model of arithmetic (the structure $\N$) that are unprovable? $\endgroup$ – Rafael Bankosegger Mar 2 at 11:18
  • 1
    $\begingroup$ @RafaelBankosegger - exactly. $\endgroup$ – Mauro ALLEGRANZA Mar 2 at 11:19
  • $\begingroup$ Perfect answer! This is what I was searching for. Many thanks :) $\endgroup$ – Rafael Bankosegger Mar 2 at 11:22
  • $\begingroup$ @RafaelBankosegger However, it's also worth noting that there is a "model-independent" result here too: no recursively axiomatizable extension of PA is both consistent and complete. This improvement on Godel's original result is due to Rosser. $\endgroup$ – Noah Schweber Mar 2 at 16:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.