Undecidability first order logic
LO.FirstOrder.Arithmetic.undecidability_first_order_logic
Project documentation
Church's theorem: the set of (purely logically, i.e. ∅-)provable sentences is not computable.
Exact Lean statement
theorem undecidability_first_order_logic : ¬ComputablePred ((∅ : ArithmeticTheory).theory)
Formal artifact
Lean source
theorem undecidability_first_order_logic : ¬ComputablePred ((∅ : ArithmeticTheory).theory) := by have hDeduction (σ : ArithmeticSentence) : 𝗣𝗔⁻ ⊢ σ ↔ (∅ : ArithmeticTheory) ⊢ PeanoMinus.finite.toFinset.conj 🡒 σ := by rw [Entailment.Equiv.iff.mp PeanoMinus.equiv_singleton_finiteConj σ, ←insert_empty_eq] exact Entailment.deduction_iff by_contra hC have hImpIntro : Computable fun σ : ArithmeticSentence ↦ PeanoMinus.finite.toFinset.conj 🡒 σ := let c := Encodable.encode (∼PeanoMinus.finite.toFinset.conj : ArithmeticSentence) computable_iff_sigma1_simulate (f := fun e ↦ ⟪5, c, e⟫ + 1) (by definability) fun σ ↦ by simp [nat_pair_eq, c, Semiformula.imp_eq, Semiformula.encode_or, ← Semiformula.encode_eq_toNat, ← Semiformula.encode_eq_toNat] apply church_theorem_general (T := 𝗣𝗔⁻) (ComputablePred.computable_of_manyOneReducible ?_ hC) refine ⟨fun σ ↦ PeanoMinus.finite.toFinset.conj 🡒 σ, ?_, ?_⟩ . exact hImpIntro . exact hDeduction- Project
- Foundation
- License
- Apache-2.0
- Commit
- 8dcdb3196454
- Source
- Foundation/FirstOrder/Incompleteness/Church.lean:84-100
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Computable Pred iff decoded pred
ComputablePred.iff_decoded_pred
Plain-language statement
Computability of a predicate on a Primcodable type is equivalent to the computability of the corresponding predicate on ℕ obtained by decoding.
Source project: Foundation
Person-level attribution pending.
Bv quote fixitr
LO.FirstOrder.Arithmetic.Bootstrapping.bv_quote_fixitr
Plain-language statement
bv-pin bridge (over ℕ): bv ⌜fixitr 0 (fvSup χ) ▹ χ⌝ = fvSup χ. - ≤ is immediate from quote_univCl_eq + bv_qqAlls (closing fvSup quantifiers reaches a sentence, whose bv is 0). - ≥ is by level-factoring: were the body an IsSemiformula j for some j < fvSup, IsSemiformula.sound + castLE-invariance would re-express χ as `γ ⇜ ![...
Source project: Foundation
Person-level attribution pending.
Conj
LO.FirstOrder.Arithmetic.Bootstrapping.Derivable.conj
Plain-language statement
Crucial inducion for formalized -completeness.
Source project: Foundation
Person-level attribution pending.