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
FFL.FirstOrder.Arithmetic.computable_iff_sigma1_simulate
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{f : ℕ → ℕ}
(hf : { Γ := 𝚺, rank := 1 }.DefinableFunction₁ f)
{F : α → β}
(h : ∀ (a : α), f (Encodable.encode a) = Encodable.encode (F a))
:
theorem
FFL.FirstOrder.Arithmetic.computable₂_iff_sigma1_simulate
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable γ]
{f : ℕ → ℕ → ℕ}
(hf : { Γ := 𝚺, rank := 1 }.DefinableFunction₂ f)
{F : α → β → γ}
(h : ∀ (a : α) (b : β), f (Encodable.encode a) (Encodable.encode b) = Encodable.encode (F a b))
:
theorem
FFL.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.