Church's undecidability theorem #
The set of sentences provable in an arithmetic theory T ⊇ 𝗥₀ is not computable, whether T is
sound on 𝚺₁ sentences (uncomputable_theory_of_sigma1Sound) or merely consistent and extends
𝗜𝚺₁ (uncomputable_theory_of_consistent). Provability in pure first-order logic is likewise
undecidable (undecidability_first_order_logic).
theorem
LO.FirstOrder.Arithmetic.computable_iff_sigma1_simulate
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{f : ℕ → ℕ}
(hf : 𝚺₁-Function₁ f)
{F : α → β}
(h : ∀ (a : α), f (Encodable.encode a) = Encodable.encode (F a))
:
theorem
LO.FirstOrder.Arithmetic.computable₂_iff_sigma1_simulate
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable γ]
{f : ℕ → ℕ → ℕ}
(hf : 𝚺₁-Function₂ f)
{F : α → β → γ}
(h : ∀ (a : α) (b : β), f (Encodable.encode a) (Encodable.encode b) = Encodable.encode (F a b))
:
theorem
LO.FirstOrder.Arithmetic.uncomputable_theory_of_sigma1Sound
{T : ArithmeticTheory}
[𝗥₀ ⪯ T]
[T.SoundOnHierarchy 𝚺 1]
:
Provability in pure first-order logic, i.e. provability from the empty theory, is undecidable.