feat(Incompleteness): discharge the π£π / ππΊβ Ξβ-definability axioms (v4.29.0)#6
Closed
gotrevor wants to merge 2 commits into
Closed
feat(Incompleteness): discharge the π£π / ππΊβ Ξβ-definability axioms (v4.29.0)#6gotrevor wants to merge 2 commits into
gotrevor wants to merge 2 commits into
Conversation
`Examples.lean` shipped two disclosed-TODO axioms:
axiom ISigma1_delta1Definable : ππΊβ.Ξβ
axiom PA_delta1Definable : π£π.Ξβ
This proves both as instances. New `InductionSchemeDelta1.lean` establishes the
mathematical content `(InductionScheme ββα΅£ C).Ξβ` (the schema's Ξβ-definability via
an internal Ξ£β recognizer); `Theory.Ξβ.add`/`.ofEq` assemble the two headline
instances from it plus the finite `π£πβ».Ξβ`.
Verified axiom-clean (no sorryAx, no custom axioms):
#print axioms PA_delta1Definable / ISigma1_delta1Definable
β [propext, Classical.choice, Quot.sound]
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Owner
Author
|
Moved to #9 |
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
1 participant
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.
Small, v4.29.0 PR β base = the commit matching upstream
FormalizedFormalLogic/Foundationmaster. Fork-internal review; nothing sent upstream.
What
Discharges the two disclosed-TODO axioms in
Foundation/FirstOrder/Incompleteness/Examples.lean,proving both as instances:
How
New
InductionSchemeDelta1.leanestablishes(InductionScheme ββα΅£ C).Ξββ the schema'sΞβ-definability via an internal Ξ£β recognizer (with a proven
IsSigma1 βΟβ β Hierarchy πΊ 1 Οbridge).
Theory.Ξβ.add/.ofEqplus the finiteπ£πβ».Ξβassemble both headline instances.Provenance / verification
Developed on v4.31, cherry-picked clean onto v4.29.0 (no conflicts; no v4.31-only tactics;
its imports
First/Secondare byte-identical v4.29βv4.31). Axiom-clean on v4.31:The v4.29 build is not yet locally verified β CI on this PR is the check.