Lagmental Vicfred

Gödel's First Incompleteness Theorem Produces an Undecidable Sentence by Vicfred

tags: mathematics, computability, incompleteness, Turing machines

A sound effective theory strong enough for arithmetic cannot decide every arithmetic sentence. I want the notation, the mechanism, and the failure mode visible at the same time.

Set-up

A decision problem is computable when a Turing machine \(M_e(x)\) halts on every input with the correct answer. A set \(A\subseteq\mathbf N\) is computably enumerable when a machine can list its members.

$$ T\ \text{sound, computably axiomatized, and arithmetically adequate} $$

I read the first line as input and the second as output. The symbols \(\forall\) and \(\exists\) are not interchangeable, and neither may be upgraded silently to \(\Longleftrightarrow\).

$$ \exists G_T,\qquad T\nvdash G_T,\quad T\nvdash\neg G_T $$

The calculation

The computation below is not a second theorem. It is a checksum for the definitions and a place to inspect the difficult LaTeX at full size.

$$ T\vdash G_T\leftrightarrow\neg\operatorname{Prov}_T(\ulcorner G_T\urcorner) $$

What survives abstraction

The compact alignment is a local map of the argument: assumptions on the first row, consequence on the second. Any generalisation must preserve that dependency.

$$ \begin{aligned} \mathsf{D}\;&:\quad T\ \text{sound, computably axiomatized, and arithmetically adequate},\\[5pt] \mathsf{C}\;&:\quad \exists G_T,\qquad T\nvdash G_T,\quad T\nvdash\neg G_T. \end{aligned} $$

The boundary

Enumerability is weaker than decidability. A search may confirm membership eventually without ever certifying nonmembership.

$$ \boxed{\begin{gathered} \text{compact conclusion}\\[-2pt] \exists G_T,\qquad T\nvdash G_T,\quad T\nvdash\neg G_T \end{gathered}} $$

The result is compact enough to reuse without pretending that the caveat has disappeared. The worked line remains the quickest consistency check.

This article was posted on Thu 24 September 2009. Facts and circumstances may have changed since publication.
Please contact me before jumping to conclusions if something seems wrong or unclear.