refactor(FirstOrder): abstract hierarchy over operators#838
Open
00sqh wants to merge 1 commit into
Open
Conversation
iehality
reviewed
Jul 9, 2026
Comment on lines
+392
to
+408
| ⟨by | ||
| generalize hq : (∀⁰[R.operator ![#0, t]] φ) = ψ | ||
| intro H | ||
| induction H <;> try simp [LO.FirstOrder.ball, LO.FirstOrder.bexs] at hq | ||
| case ball φ t pt hp ih => | ||
| rcases hq with ⟨_, rfl⟩ | ||
| assumption | ||
| case all hp ih => | ||
| rcases hq with rfl | ||
| exact (imp_iff.mp hp).2 | ||
| case pi s _ _ hp ih => | ||
| rcases hq with rfl | ||
| exact (imp_iff.mp hp).2.accum _ | ||
| case dummy_sigma hp _ => | ||
| rcases hq with rfl | ||
| exact (imp_iff.mp hp).2.accum _, | ||
| by intro hp; exact hp.ball ht⟩ |
Member
There was a problem hiding this comment.
It is much clearer to use by constructor ... instead of ⟨by ..., by ...⟩ for long proof.
|
|
||
| namespace LO.FirstOrder | ||
|
|
||
| namespace OperatorHierarchy |
Member
There was a problem hiding this comment.
I think OperatorHierarchy is bit misleading. How about using Bounding instead of Operator in general?
Comment on lines
+287
to
+293
| class OperatorRewPreimage (R : Semiformula.Operator L 2) (ξ₁ ξ₂ : Type*) : Prop where | ||
| operator_preimage {n₁ n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) | ||
| {φ : Semiformula L ξ₁ (n₁ + 1)} | ||
| {t : Semiterm L ξ₂ (n₂ + 1)} : | ||
| ω.q ▹ φ = R.operator ![#0, t] → | ||
| ∃ u : Semiterm L ξ₁ (n₁ + 1), | ||
| ω.q u = t ∧ φ = R.operator ![#0, u] |
Member
There was a problem hiding this comment.
How about using general characterization Operator.SymbolLike like
class Operator.SymbolLike (o : Operator L k) (ξ₁ ξ₂) : Prop where
symbolLike : ∀ ω : Rel L ξ₁ n₁ ξ₂, n₂, ω ▹ φ = o.operator v → ∃ w, φ = o.operator w ∧ ∀ i, ω (w i) = v i
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.
Partially addresses #663.
This PR abstracts the hierarchy machinery from the arithmetic hierarchy into an operator-parametric hierarchy.
A technical point is that two additional abstraction classes are introduced:
OperatorSmall, for operators whose instances already belong to the relevant hierarchy levels.OperatorRewPreimage, for operators whose bounded formulas can be inverted through rewriting.The old arithmetic hierarchy did not need these classes because
<was hardcoded and Lean could unfold it as an atomic formula. For anarbitrary
Semiformula.Operator R,R.operator vmay be composite, so the needed smallness and rewriting-preimage assumptions are recordedexplicitly.
This PR does not yet rewrite the hierarchy machinery in
FirstOrder/Arithmetic/Definability, nor does it add the corresponding definabilitymachinery for set theory.
The set-theoretic definability part may not be a straightforward copy-paste from arithmetic. To get analogous definability machinery in set
theory, we may need additional tools involving rudimentary functions, which may be somewhat tricky to formalize. That is left for future work.
If the current part looks acceptable, I will continue working on this.