Skip to content

feat(FirstOrder/Arith): Arithmetical hierarchy is equivalent to strict arithmetical hierarchy #336

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
iehality wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

feat(FirstOrder/Arith): Arithmetical hierarchy is equivalent to strict arithmetical hierarchy #336

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c5ba54b
positive decidable
iehality Apr 26, 2025
782322a
Merge branch 'master' into strict-hierarchy
iehality May 18, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 11 additions & 3 deletions Foundation/Logic/Predicate/Term.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ section Decidable

variable [∀ k, DecidableEq (L.Func k)] [DecidableEq ξ]

def hasDecEq : (t u : Semiterm L ξ n) → Decidable (Eq t u)
def hasDecEq : (t u : Semiterm L ξ n) → Decidable (t = u)
| #x, #y => by simp; exact decEq x y
| #_, &_ => isFalse Semiterm.noConfusion
| #_, func _ _ => isFalse Semiterm.noConfusion
Expand All @@ -67,7 +67,7 @@ def hasDecEq : (t u : Semiterm L ξ n) → Decidable (Eq t u)
by_cases e : k₁ = k₂
· rcases e with rfl
exact match decEq r₁ r₂ with
| isTrue h => by simp[h]; exact Matrix.decVec _ _ (fun i => hasDecEq (v₁ i) (v₂ i))
| isTrue h => by simpa [h] using Matrix.decVec _ _ fun i ↦ hasDecEq (v₁ i) (v₂ i)
| isFalse h => isFalse (by simp[h])
· exact isFalse (by simp[e])

Expand All @@ -88,7 +88,7 @@ lemma complexity_func {k} (f : L.Func k) (v : Fin k → Semiterm L ξ n) : (func

@[simp] lemma complexity_func_lt {k} (f : L.Func k) (v : Fin k → Semiterm L ξ n) (i) :
(v i).complexity < (func f v).complexity := by
simp [complexity_func, Nat.lt_add_one_iff]; exact Finset.le_sup (f := fun i ↦ complexity (v i)) (by simp)
simpa [complexity_func, Nat.lt_add_one_iff] using Finset.le_sup (f := fun i ↦ complexity (v i)) (by simp)

abbrev func! (k) (f : L.Func k) (v : Fin k → Semiterm L ξ n) := func f v

Expand Down Expand Up @@ -121,6 +121,14 @@ end Positive
lemma bv_eq_empty_of_positive {t : Semiterm L ξ 1} (ht : t.Positive) : t.bv = ∅ :=
Finset.eq_empty_of_forall_not_mem <| by simp [Positive, Fin.eq_zero] at ht ⊢; assumption

instance Positive.dec : (t : Semiterm L ξ (n + 1)) → Decidable t.Positive
| #x => decidable_of_iff (0 < x) (by simp)
| &x => .isTrue (by simp)
| .func f v =>
have : DecidablePred fun i ↦ (v i).Positive := fun i ↦ Positive.dec (v i)
have : Decidable (∀ i, (v i).Positive) := inferInstance
decidable_of_iff (∀ i, (v i).Positive) (by simp)

section freeVariables

variable [DecidableEq ξ]
Expand Down
Loading