feat(Incompleteness): discharge the 𝗣𝗔 / 𝗜𝚺₁ Δ₁-definability axioms#833
Merged
Merged
Conversation
Upstream (FormalizedFormalLogic#830) ships `𝗣𝗔.Δ₁` and `𝗜𝚺₁.Δ₁` as unproven `axiom`s in `FirstOrder/Incompleteness/Examples.lean`. This discharges both. New `InductionSchemeDelta1.lean` establishes `(InductionScheme ℒₒᵣ C).Δ₁` (the schema's Δ₁-definability via an internal Σ₁ recognizer); `Theory.Δ₁.add` /`.ofEq` assemble the two headline instances from it plus finite `𝗣𝗔⁻.Δ₁`. Ported onto current upstream master (post-FormalizedFormalLogic#794 FirstOrder redesign). Three adjustments were needed vs the pre-FormalizedFormalLogic#794 proof: * model satisfaction `[V ⊧ₘ* 𝗜𝚺₁]` → `[V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁]` (language made explicit) * re-introduced the `SyntacticSemiformula`/`SyntacticFormula` abbreviations (FormalizedFormalLogic#794 removed the formula-level ones; the term-level `SyntacticSemiterm` /`SyntacticTerm` survive in `Syntax/Predicate/Term.lean`) * `Function.comp_apply` in one `simp only` (`Rew.func` now normalises to `∘`) Verified axiom-clean on current upstream: #print axioms PA_delta1Definable / ISigma1_delta1Definable → [propext, Classical.choice, Quot.sound] Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Codex's warning-cleanup commit also touched 5 files unrelated to the Δ₁ discharge. Those are pre-existing upstream mathlib/Std deprecation renames — reverted here to keep this PR focused on the two axioms; the deprecation fixes move to their own PR.
Member
Per review feedback, remove all five `set_option maxHeartbeats` in InductionSchemeDelta1.lean; the file now builds under the default 200k. The three that mattered are the recognizer-inversion lemmas `IsSigma1.and_iff/or_iff/ex_iff`. They use the same `rcases h.case <;> simp [qq…] at h` idiom as the upstream `IsUFormula.and/or/ex`, but the simp set additionally carried `Arithmetic.qqNLT`. In these lemmas the bounded-∀ branch only needs its outer `qqAll` tag to be seen as distinct from `qqAnd`/`qqOr`/`qqExs`; including `qqNLT` forced the whole nested `qqBall = ^∀(qqOr (qqNLT #0 u) q)` encoding to unfold across all eight `rcases` branches. Dropping `qqNLT` brings them well under the default, matching the un-annotated upstream lemmas. The other two (`termBV_termBShift_le`, `hierarchy_of_isSigma1`) needed no proof change; their ceilings were simply over-provisioned. Full `lake build` green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Member
|
I can't find any mathematical flaws in it. What concerns me is the use of |
SnO2WMaN
changed the title
𝗣𝗔 / 𝗜𝚺₁ Δ₁-definability axioms
Member
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Discharges the two
axioms upstreammastercurrently ships inFirstOrder/Incompleteness/Examples.lean(they rode in via the v4.31 port #830):Both are now proven (the
axiomkeyword +attribute [instance]block are removed;the proofs live in the new
InductionSchemeDelta1.leanand are picked up as instances).A note on review scope
This proof was Claude Code generated, and I (@gotrevor) cannot defend or
validate the ~1400 lines of
InductionSchemeDelta1.lean, formally or mathematically.What I can stand behind is mechanical and checkable:
Examples.lean), under identicalsignatures — nothing new is asserted; the
axiomkeyword is simply replaced by a proof.So the kernel vouches for internal consistency, but whether the internal Σ₁ recognizer faithfully
captures the induction schema is a mathematical judgment I'd rather leave to your review than assert
myself.
Route
𝗣𝗔 = 𝗣𝗔⁻ ∪ InductionScheme ℒₒᵣ Set.univ,𝗜𝚺₁ = 𝗣𝗔⁻ ∪ InductionScheme ℒₒᵣ (Hierarchy 𝚺 1).𝗣𝗔⁻is finite (Theory.Δ₁.ofFinite);Theory.Δ₁.add/.ofEqreduce both headlines to thesingle obligation
(InductionScheme ℒₒᵣ C).Δ₁, established via an internal Σ₁ recognizer.Port notes
Rebased the pre-#794 proof onto current
master. Three adjustments vs #794's FirstOrder redesign:[V ⊧ₘ* 𝗜𝚺₁]→[V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁](language made explicit)SyntacticSemiformula/SyntacticFormulaabbreviations (change(FirstOrder): redesignFirstOrder#794 removed theformula-level ones; the term-level
SyntacticSemiterm/SyntacticTermsurvive) — happy to inlineSemiformula L ℕ ninstead if you prefer the new conventionFunction.comp_applyin onesimp only(Rew.funcnow normalises the arg map to∘)Verification
Audit surface
The load-bearing statements are the two axiom signatures being discharged, in
Examples.lean.Supersedes the fork-internal #6 (pre-#794 base).
🤖 Generated with Claude Code