Definability by strict-hierarchy formulas

structure FFL.FirstOrder.Arithmetic.IsStrictDefinedBy {V : Type u_1} [ORingStructure V] {k : ℕ} (Γ : Polarity) (s : ℕ) (R : (Fin k → V) → Prop) (φ : ArithmeticSemisentence k) : Prop

• strictHierarchy : StrictHierarchy Γ s φ
• defined : IsDefinedBy R φ

structure FFL.FirstOrder.Arithmetic.IsStrictDefinedByWithParam {V : Type u_1} [ORingStructure V] {k : ℕ} (Γ : Polarity) (s : ℕ) (R : (Fin k → V) → Prop) (φ : ArithmeticSemiformula V k) : Prop

• strictHierarchy : StrictHierarchy Γ s φ
• defined : IsDefinedByWithParam R φ

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.StrictDefinable {V : Type u_1} [ORingStructure V] (Γ : Polarity) (s : ℕ) {k : ℕ} (P : (Fin k → V) → Prop) : Prop

Equations

• FFL.FirstOrder.Arithmetic.StrictDefinable Γ s P = ∃ (φ : FFL.FirstOrder.ArithmeticSemiformula V k), FFL.FirstOrder.Arithmetic.IsStrictDefinedByWithParam Γ s P φ

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.StrictDefinablePred {V : Type u_1} [ORingStructure V] (Γ : Polarity) (s : ℕ) (P : V → Prop) : Prop

Equations

• FFL.FirstOrder.Arithmetic.StrictDefinablePred Γ s P = FFL.FirstOrder.Arithmetic.StrictDefinable Γ s fun (v : Fin 1 → V) => P (v 0)

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.StrictDefinableRel {V : Type u_1} [ORingStructure V] (Γ : Polarity) (s : ℕ) (R : V → V → Prop) : Prop

Equations

• FFL.FirstOrder.Arithmetic.StrictDefinableRel Γ s R = FFL.FirstOrder.Arithmetic.StrictDefinable Γ s fun (v : Fin 2 → V) => R (v 0) (v 1)

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.StrictDefinableRel₃ {V : Type u_1} [ORingStructure V] (Γ : Polarity) (s : ℕ) (R : V → V → V → Prop) : Prop

Equations

• FFL.FirstOrder.Arithmetic.StrictDefinableRel₃ Γ s R = FFL.FirstOrder.Arithmetic.StrictDefinable Γ s fun (v : Fin 3 → V) => R (v 0) (v 1) (v 2)

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.StrictDefinableRel₄ {V : Type u_1} [ORingStructure V] (Γ : Polarity) (s : ℕ) (R : V → V → V → V → Prop) : Prop

Equations

• FFL.FirstOrder.Arithmetic.StrictDefinableRel₄ Γ s R = FFL.FirstOrder.Arithmetic.StrictDefinable Γ s fun (v : Fin 4 → V) => R (v 0) (v 1) (v 2) (v 3)

theorem FFL.FirstOrder.Arithmetic.StrictDefinable.of_iff {V : Type u_1} [ORingStructure V] {k : ℕ} {Γ : Polarity} {s : ℕ} {P Q : (Fin k → V) → Prop} (h : StrictDefinable Γ s Q) (H : ∀ (v : Fin k → V), P v ↔ Q v) : StrictDefinable Γ s P

theorem FFL.FirstOrder.Arithmetic.StrictDefinable.definable {V : Type u_1} [ORingStructure V] {k : ℕ} {Γ : Polarity} {s : ℕ} {P : (Fin k → V) → Prop} (h : StrictDefinable Γ s P) : { Γ := Γ.coe, rank := s }.Definable P

theorem FFL.FirstOrder.Arithmetic.StrictDefinable.exists_eval_iff {V : Type u_1} [ORingStructure V] {k : ℕ} {Γ : Polarity} {s : ℕ} {P : (Fin k → V) → Prop} (h : StrictDefinable Γ s P) : ∃ (e : ℕ → V) (φ : ArithmeticSemiformula ℕ k), StrictHierarchy Γ s φ ∧ ∀ (v : Fin k → V), P v ↔ (Semiformula.Eval v e) φ

theorem FFL.FirstOrder.Arithmetic.StrictDefinable.of_strictHierarchy {V : Type u_1} [ORingStructure V] {Γ : Polarity} {s : ℕ} {ξ : Type u_2} {m : ℕ} {θ : ArithmeticSemiformula ξ (m + 2)} (hθ : StrictHierarchy Γ s θ) (e : Fin m → V) (f : ξ → V) : StrictDefinableRel Γ s fun (x y : V) => (Semiformula.Eval (y :> x :> e) f) θ