Gödel's First Incompleteness Theorem

A deduction system $\mathcal{S}$ is complete iff it can prove or refute every sentence $\sigma$. Otherwise, $\mathcal{S}$ is incomplete.

def System.Complete {F S} [System F S] [LogicalConnective F] (𝓢 : S) : Prop :=
    ∀ f, 𝓢 ⊢! f ∨ 𝓢 ⊢! ~f

• System.Complete

Theorem

Let $T$ be a ${\Delta }_1$-definable arithmetic theory, stronger than ${\mathsf{R}}_0$ and ${\Sigma }_1$-sound.

Representeation Theorem

Theorem: Let $S$ be a r.e. set. Then, there exists a formula ${\phi }_S(x)$ such that $n\in S⟺T⊢{\phi }_S(\overline{n})$ for all $n\in \mathbb{N}$.

lemma re_complete
    [𝐑₀ ≼ T] [Sigma1Sound T]
    {p : ℕ → Prop} (hp : RePred p) {x : ℕ} :
    p x ↔ T ⊢! ↑((codeOfRePred p)/[‘↑x’] : Sentence ℒₒᵣ) 

• re_complete

Main Theorem

Theorem: ${\Sigma }_1$-sound and ${\Delta }_1$-definable first-order theory, which is stronger than ${\mathsf{R}}_0$, is incomplete.

• Proof.

  Define a set of formulae with one variable. $$D:=\{\phi \mid T⊢\neg \phi (┌\phi ┐)\}$$ $D$ is r.e. since $T$ is ${\Delta }_1$-definable. (one could use Craig's trick to weaken this condition to ${\Sigma }_1$, but I will not do that here.)

  By the representation theorem, there exists a ${\Sigma }_1$ formula $\rho (x)$ that represents $D$. i.e.,

  $$T⊢\rho (┌\phi ┐)⟺T⊢\neg \phi (┌\phi ┐)$$

  Let $\gamma :=\rho (┌\rho ┐)$. The next follows immediately.

  $$T⊢\gamma ⟺T⊢\neg \gamma$$

  Thus, as $T$ is consistent, $\gamma$ is undecidable from $T$. ∎

theorem goedel_first_incompleteness
  (T : Theory ℒₒᵣ) [𝐑₀ ≼ T] [Sigma1Sound T] [T.Delta1Definable] :
  ¬System.Complete T

• goedel_first_incompleteness