Church's undecidability theorem

church_theorem_general shows that for every arithmetic theory T ⊇ 𝗥₀ sound on 𝚺₁ sentences, the set of T-provable sentences is not computable, by a direct diagonalization on the self-applied substitution σ ↦ σ/[⌜σ⌝] (no fixed-point/Gödel-numbering machinery beyond weak representability of r.e. predicates, rePred_weak_representation, is needed, unlike Gödel's first incompleteness theorem). undecidability_first_order_logic specializes this to T = ∅: since 𝗣𝗔⁻ is finitely axiomatizable, 𝗣𝗔⁻-provability computably many-one reduces to ∅-provability, so undecidability transfers from church_theorem_general without needing the 𝗥₀ ⪯ T and soundness hypotheses required there.

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)) : Computable F

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)) : Computable₂ F

theorem LO.FirstOrder.Arithmetic.church_theorem_general {T : ArithmeticTheory} [𝗥₀ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : ¬ComputablePred (Theory.theory T)

Church's theorem, for an arbitrary arithmetic theory T ⊇ 𝗥₀ sound on 𝚺₁ sentences: the set of T-provable sentences is not computable.

theorem LO.FirstOrder.Arithmetic.undecidability_first_order_logic : ¬ComputablePred (Theory.theory ∅)

Church's theorem: the set of (purely logically, i.e. ∅-)provable sentences is not computable.