add(Arithmetic): Add partial truth predicate#849
Draft
SnO2WMaN wants to merge 21 commits into
Draft
Conversation
…thmetical hierarchy Introduces StrictHierarchy as the first step toward issue #707, defining a non-cumulative prenex Sigma_n/Pi_n class on top of the existing Hierarchy predicate. Co-Authored-By: Claude <noreply@anthropic.com>
…issue #707 step 2, phase 0) Adds StrictHierarchy inversion lemmas (sigma_succ_elim/pi_succ_elim) and a new PrenexNat.lean with the EquivStrict definition, CoreClosure bundling, and all assembly lemmas implemented. The ten hardest lemmas (semantic closure steps, nat_collection, and the main hierarchy_equivStrict theorem) are left as sorry with statements fixed, per the plan recorded in .directions/strict-arithmetic-hierarchy.md, to allow parallel implementation per lemma. Co-Authored-By: Claude <noreply@anthropic.com>
Co-Authored-By: Claude <noreply@anthropic.com>
…#707 step 2) Integrates the 9 lemmas implemented in parallel across separate worktrees (nat_collection, nat_exists_and_exists, nat_exists_exists, coreClosure_one, or_sigma_step, and_sigma_step, bexs_sigma_step, ball_sigma_step, hierarchy_equivStrict) into the skeleton from the previous commit. No sorry remains in PrenexNat.lean. Co-Authored-By: Claude <noreply@anthropic.com>
… strict hierarchy theorem (issue #707 step 3-4, phase 0) Adds PartialTruth.lean (the sigmaTruth partial truth predicate, fully defined) and StrictHierarchy.lean (the diagNeg diagonal formula, fully defined, plus the main theorem strict_arithmetical_hierarchy assembled from sigmaTruth_hierarchy and sigmaTruth_not_pi). The harder correctness/diagonalization lemmas are left as sorry with statements fixed, per the plan recorded in .directions/strict-arithmetic-hierarchy.md, to allow parallel implementation per lemma. Co-Authored-By: Claude <noreply@anthropic.com>
…step 3) Co-Authored-By: Claude <noreply@anthropic.com>
…em (issue #707 step 4) Co-Authored-By: Claude <noreply@anthropic.com>
SnO2WMaN
marked this pull request as draft
July 13, 2026 04:11
Co-Authored-By: Claude <noreply@anthropic.com>
Co-Authored-By: Claude <noreply@anthropic.com>
Co-Authored-By: Claude <noreply@anthropic.com>
…archy Rewrite sigmaTruth_iff to take n/σ/h explicitly and use induction. Co-Authored-By: Claude <noreply@anthropic.com> # Conflicts: # Foundation/FirstOrder/Incompleteness/PartialTruth.lean
…archy Clean up StrictHierarchy: English docstring, shared variables, drop unneeded set_option linter.flexible false. Co-Authored-By: Claude <noreply@anthropic.com>
Co-Authored-By: Claude <noreply@anthropic.com>
Clean up EquivStrict proofs and add simp/grind attributes. Co-Authored-By: Claude <noreply@anthropic.com>
SnO2WMaN
changed the title
Σ_n truth predicate
Co-Authored-By: Claude <noreply@anthropic.com>
…rarchy Strip issue/step/plan-label references from comments and docstrings. Co-Authored-By: Claude <noreply@anthropic.com>
Co-Authored-By: Claude <noreply@anthropic.com>
…erarchy Drop stale skeleton-phase module docstrings that no longer match the completed implementation. Co-Authored-By: Claude <noreply@anthropic.com>
Member
|
基本的には |
Co-Authored-By: Claude <noreply@anthropic.com>
…ection Co-Authored-By: Claude <noreply@anthropic.com>
Cite HP98 (Hájek–Pudlák) for the arithmetical hierarchy results. Co-Authored-By: Claude <noreply@anthropic.com>
SnO2WMaN
changed the title
Σ_n truth predicate
SnO2WMaN
added a commit
that referenced
this pull request
Jul 13, 2026
Co-Authored-By: Claude <noreply@anthropic.com>
SnO2WMaN
added
the
Arithmetic
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
2 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.
Close #705
Summary
sigmaTruth（𝗜𝚺₁の証明可能性述語を基底とした，各レベルのΣ_{n+1}文の真偽をℕ上で正しく判定する部分真理述語）とその周辺の補題群を対象に，issue #707（strict arithmetical hierarchyの形式化）はPR #850へ切り出した．本PRは issue #705（partial truth definitions）向けの部分真理述語関連の作業を継続する．🤖 Generated with Claude Code