Formulas sorted by a bounding hierarchy

structure FFL.FirstOrder.Bounding.HierarchySymbol {L : Language} (ℬ : Bounding L) : Type

• Γ : SigmaPiDelta
• rank : ℕ

def FFL.FirstOrder.Bounding.«term_-[_,_]» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

inductive FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula {L : Language} {ℬ : Bounding L} (ξ : Type u_1) (n : ℕ) : ℬ.HierarchySymbol → Type (max u_1 u_2)

• mkSigma {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : Semiformula L ξ n) (hφ : ℬ.Hierarchy 𝚺 m φ := by simp) : HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }
• mkPi {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : Semiformula L ξ n) (hφ : ℬ.Hierarchy 𝚷 m φ := by simp) : HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }
• mkDelta {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} : HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m } → HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m } → HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }

@[reducible, inline]

abbrev FFL.FirstOrder.Bounding.HierarchySymbol.Semisentence {L : Language} {ℬ : Bounding L} (Γ : ℬ.HierarchySymbol) (n : ℕ) : Type u_2

Equations

• Γ.Semisentence n = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula Empty n Γ

@[reducible, inline]

abbrev FFL.FirstOrder.Bounding.HierarchySymbol.Sentence {L : Language} {ℬ : Bounding L} (Γ : ℬ.HierarchySymbol) : Type u_2

Equations

• Γ.Sentence = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula Empty 0 Γ

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : ℬ.HierarchySymbol} : HierarchySymbol.Semiformula ξ n Γ → Semiformula L ξ n

Equations

• ↑(FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkSigma φ hφ) = φ
• ↑(FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPi φ hφ) = φ
• ↑(φ.mkDelta a) = ↑φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_mkSigma {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : Semiformula L ξ n) (hp : ℬ.Hierarchy 𝚺 m φ) : ↑(mkSigma φ hp) = φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_mkPi {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : Semiformula L ξ n) (hp : ℬ.Hierarchy 𝚷 m φ) : ↑(mkPi φ hp) = φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_mkDelta {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }) (ψ : HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }) : ↑(φ.mkDelta ψ) = ↑φ

@[instance_reducible]

instance FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instCoeOutSemisentenceMkSigmaSigmaPiDeltaOfNatNatSemisentence {L : Language} {ℬ : Bounding L} {n : ℕ} : CoeOut ({ Γ := 𝚺, rank := 0 }.Semisentence n) (Semisentence L n)

Equations

• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instCoeOutSemisentenceMkSigmaSigmaPiDeltaOfNatNatSemisentence = { coe := FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val }

@[instance_reducible]

instance FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instCoeOutSemisentenceMkPiSigmaPiDeltaOfNatNatSemisentence {L : Language} {ℬ : Bounding L} {n : ℕ} : CoeOut ({ Γ := 𝚷, rank := 0 }.Semisentence n) (Semisentence L n)

Equations

• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instCoeOutSemisentenceMkPiSigmaPiDeltaOfNatNatSemisentence = { coe := FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val }

@[instance_reducible]

instance FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instCoeOutSemisentenceMkDeltaSigmaPiDeltaOfNatNatSemisentence {L : Language} {ℬ : Bounding L} {n : ℕ} : CoeOut ({ Γ := 𝚫, rank := 0 }.Semisentence n) (Semisentence L n)

Equations

• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instCoeOutSemisentenceMkDeltaSigmaPiDeltaOfNatNatSemisentence = { coe := FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val }

@[instance_reducible]

instance FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instCoeOutSemisentenceMkSigmaSigmaPiDeltaOfNatNatSemisentence_1 {L : Language} {ℬ : Bounding L} {n : ℕ} : CoeOut ({ Γ := 𝚺, rank := 1 }.Semisentence n) (Semisentence L n)

Equations

• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instCoeOutSemisentenceMkSigmaSigmaPiDeltaOfNatNatSemisentence_1 = { coe := FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val }

@[instance_reducible]

instance FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instCoeOutSemisentenceMkPiSigmaPiDeltaOfNatNatSemisentence_1 {L : Language} {ℬ : Bounding L} {n : ℕ} : CoeOut ({ Γ := 𝚷, rank := 1 }.Semisentence n) (Semisentence L n)

Equations

• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instCoeOutSemisentenceMkPiSigmaPiDeltaOfNatNatSemisentence_1 = { coe := FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val }

@[instance_reducible]

instance FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instCoeOutSemisentenceMkDeltaSigmaPiDeltaOfNatNatSemisentence_1 {L : Language} {ℬ : Bounding L} {n : ℕ} : CoeOut ({ Γ := 𝚫, rank := 1 }.Semisentence n) (Semisentence L n)

Equations

• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instCoeOutSemisentenceMkDeltaSigmaPiDeltaOfNatNatSemisentence_1 = { coe := FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val }

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.sigma_prop {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }) : ℬ.Hierarchy 𝚺 m ↑φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.pi_prop {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }) : ℬ.Hierarchy 𝚷 m ↑φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.polarity_prop {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} {Γ : Polarity} (φ : HierarchySymbol.Semiformula ξ n { Γ := Γ.coe, rank := m }) : ℬ.Hierarchy Γ m ↑φ

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.sigma {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} : HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m } → HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }

Equations

• (φ.mkDelta a).sigma = φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.sigma_mkDelta {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }) (ψ : HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }) : (φ.mkDelta ψ).sigma = φ

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.pi {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} : HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m } → HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }

Equations

• (φ.mkDelta a).pi = a

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.pi_mkDelta {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }) (ψ : HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }) : (φ.mkDelta ψ).pi = ψ

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_sigma {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) : ↑φ.sigma = ↑φ

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPolarity {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : Semiformula L ξ n) (Γ : Polarity) : ℬ.Hierarchy Γ m φ → HierarchySymbol.Semiformula ξ n { Γ := Γ.coe, rank := m }

Equations

• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPolarity φ FFL.Polarity.sigma h = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkSigma φ h
• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPolarity φ FFL.Polarity.pi h = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPi φ h

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_mkPolarity {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : Semiformula L ξ n) {Γ : Polarity} (h : ℬ.Hierarchy Γ m φ) : ↑(mkPolarity φ Γ h) = φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.hierarchy_sigma {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }) : ℬ.Hierarchy 𝚺 m ↑φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.hierarchy_pi {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }) : ℬ.Hierarchy 𝚷 m ↑φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.hierarchy_zero {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : SigmaPiDelta} {Γ' : Polarity} {m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Γ, rank := 0 }) : ℬ.Hierarchy Γ' m ↑φ

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.hierarchy_of_lt {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {C : ℬ.HierarchySymbol} {Γ : Polarity} {s : ℕ} (φ : HierarchySymbol.Semiformula ξ n C) (h : C.rank < s) : ℬ.Hierarchy Γ s ↑φ

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperOn {L : Language} {ℬ : Bounding L} {n m : ℕ} (M : Type u_4) [Tarski.Structure L M] (φ : { Γ := 𝚫, rank := m }.Semisentence n) : Prop

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperWithParamOn {L : Language} {ℬ : Bounding L} {n m : ℕ} (M : Type u_4) [Tarski.Structure L M] (φ : HierarchySymbol.Semiformula M n { Γ := 𝚫, rank := m }) : Prop

Equations

• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperWithParamOn M φ = ∀ (e : Fin n → M), (FFL.FirstOrder.Semiformula.Eval e id) ↑φ.sigma ↔ (FFL.FirstOrder.Semiformula.Eval e id) ↑φ.pi

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProvablyProperOn {L : Language} {ℬ : Bounding L} {n m : ℕ} (φ : { Γ := 𝚫, rank := m }.Semisentence n) (T : Theory L) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperOn.iff {L : Language} {ℬ : Bounding L} {n m : ℕ} {M : Type u_4} [Tarski.Structure L M] {φ : { Γ := 𝚫, rank := m }.Semisentence n} (h : ProperOn M φ) (e : Fin n → M) : (Semiformula.Evalb e) ↑(sigma φ) ↔ (Semiformula.Evalb e) ↑(pi φ)

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperWithParamOn.iff {L : Language} {ℬ : Bounding L} {n m : ℕ} {M : Type u_4} [Tarski.Structure L M] {φ : HierarchySymbol.Semiformula M n { Γ := 𝚫, rank := m }} (h : ProperWithParamOn M φ) (e : Fin n → M) : (Semiformula.Eval e id) ↑φ.sigma ↔ (Semiformula.Eval e id) ↑φ.pi

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperOn.iff' {L : Language} {ℬ : Bounding L} {n m : ℕ} {M : Type u_4} [Tarski.Structure L M] {φ : { Γ := 𝚫, rank := m }.Semisentence n} (h : ProperOn M φ) (e : Fin n → M) : (Semiformula.Evalb e) ↑(pi φ) ↔ (Semiformula.Evalb e) ↑φ

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperWithParamOn.iff' {L : Language} {ℬ : Bounding L} {n m : ℕ} {M : Type u_4} [Tarski.Structure L M] {φ : HierarchySymbol.Semiformula M n { Γ := 𝚫, rank := m }} (h : ProperWithParamOn M φ) (e : Fin n → M) : (Semiformula.Eval e id) ↑φ.pi ↔ (Semiformula.Eval e id) ↑φ

inductive FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProvablyProperOn' {L : Language} {ℬ : Bounding L} {n m : ℕ} (T : Theory L) {Γ : ℬ.HierarchySymbol} {n✝ : ℕ} (φ : Γ.Semisentence n✝) : Prop

• sigma {L : Language} {ℬ : Bounding L} {n m : ℕ} {T : Theory L} (φ : { Γ := 𝚺, rank := m }.Semisentence n) : ProvablyProperOn' T φ
• pi {L : Language} {ℬ : Bounding L} {n m : ℕ} {T : Theory L} (φ : { Γ := 𝚷, rank := m }.Semisentence n) : ProvablyProperOn' T φ
• delta {L : Language} {ℬ : Bounding L} {n m : ℕ} {T : Theory L} (φ : { Γ := 𝚫, rank := m }.Semisentence n) : ProvablyProperOn φ T → ProvablyProperOn' T φ

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProvablyProperOn.properOn {L : Language} {ℬ : Bounding L} {n m : ℕ} {T : Theory L} {φ : { Γ := 𝚫, rank := m }.Semisentence n} (h : ProvablyProperOn φ T) (M : Type w) [Nonempty M] [Tarski.Structure L M] [M↓[L] ⊧* T] : ProperOn M φ

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.rew {L : Language} {ℬ : Bounding L} {n₁ n₂ : ℕ} {ξ₁ : Type u_2} {ξ₂ : Type u_3} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {Γ : ℬ.HierarchySymbol} : HierarchySymbol.Semiformula ξ₁ n₁ Γ → HierarchySymbol.Semiformula ξ₂ n₂ Γ

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_rew {L : Language} {ℬ : Bounding L} {n₁ n₂ : ℕ} {ξ₁ : Type u_2} {ξ₂ : Type u_3} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {Γ : ℬ.HierarchySymbol} (φ : HierarchySymbol.Semiformula ξ₁ n₁ Γ) : ↑(rew ω φ) = (Rewriting.app ω) ↑φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperOn.rew {L : Language} {ℬ : Bounding L} {m n₁ n₂ : ℕ} {M : Type u_4} [Tarski.Structure L M] {φ : { Γ := 𝚫, rank := m }.Semisentence n₁} (h : ProperOn M φ) (ω : Rew L Empty n₁ Empty n₂) : ProperOn M (Semiformula.rew ω φ)

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperOn.rew' {L : Language} {ℬ : Bounding L} {m n₁ n₂ : ℕ} {M : Type u_4} [Tarski.Structure L M] {φ : { Γ := 𝚫, rank := m }.Semisentence n₁} (h : ProperOn M φ) (ω : Rew L Empty n₁ M n₂) : ProperWithParamOn M (Semiformula.rew ω φ)

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperWithParamOn.rew {L : Language} {ℬ : Bounding L} {m n₁ n₂ : ℕ} {M : Type u_4} [Tarski.Structure L M] {φ : HierarchySymbol.Semiformula M n₁ { Γ := 𝚫, rank := m }} (h : ProperWithParamOn M φ) (f : Fin n₁ → Semiterm L M n₂) : ProperWithParamOn M (Semiformula.rew (Rew.subst f) φ)

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.sigmaZero {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {k : ℕ} {Γ : SigmaPiDelta} (φ : HierarchySymbol.Semiformula ξ k { Γ := Γ, rank := 0 }) : ℬ.Hierarchy 𝚺 0 ↑φ

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ofZero {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {k : ℕ} {Γ' : SigmaPiDelta} (φ : HierarchySymbol.Semiformula ξ k { Γ := Γ', rank := 0 }) (Γ : ℬ.HierarchySymbol) : HierarchySymbol.Semiformula ξ k Γ

Equations

• One or more equations did not get rendered due to their size.
• φ.ofZero { Γ := FFL.SigmaPiDelta.sigma, rank := rank } = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkSigma ↑φ ⋯
• φ.ofZero { Γ := FFL.SigmaPiDelta.pi, rank := rank } = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPi ↑φ ⋯

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ofDeltaOne {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {k : ℕ} (φ : HierarchySymbol.Semiformula ξ k { Γ := 𝚫, rank := 1 }) (Γ : SigmaPiDelta) (m : ℕ) : HierarchySymbol.Semiformula ξ k { Γ := Γ, rank := m + 1 }

Equations

• φ.ofDeltaOne FFL.SigmaPiDelta.sigma x✝ = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkSigma ↑φ.sigma ⋯
• φ.ofDeltaOne FFL.SigmaPiDelta.pi x✝ = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPi ↑φ.pi ⋯
• φ.ofDeltaOne FFL.SigmaPiDelta.delta x✝ = (FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkSigma ↑φ.sigma ⋯).mkDelta (FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPi ↑φ.pi ⋯)

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ofZero_val {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ' : SigmaPiDelta} (φ : HierarchySymbol.Semiformula ξ n { Γ := Γ', rank := 0 }) (Γ : ℬ.HierarchySymbol) : ↑(φ.ofZero Γ) = ↑φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperOn.of_zero {L : Language} {ℬ : Bounding L} {k : ℕ} {Γ' : Polarity} {M : Type u_4} [Tarski.Structure L M] (φ : { Γ := Γ'.coe, rank := 0 }.Semisentence k) (m : ℕ) : ProperOn M (ofZero φ { Γ := 𝚫, rank := m })

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperWithParamOn.of_zero {L : Language} {ℬ : Bounding L} {k : ℕ} {Γ' : Polarity} {M : Type u_4} [Tarski.Structure L M] (φ : HierarchySymbol.Semiformula M k { Γ := Γ'.coe, rank := 0 }) (m : ℕ) : ProperWithParamOn M (φ.ofZero { Γ := 𝚫, rank := m })

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.verum {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : ℬ.HierarchySymbol} : HierarchySymbol.Semiformula ξ n Γ

Equations

• One or more equations did not get rendered due to their size.
• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.verum = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkSigma ⊤ ⋯
• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.verum = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPi ⊤ ⋯

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.falsum {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : ℬ.HierarchySymbol} : HierarchySymbol.Semiformula ξ n Γ

Equations

• One or more equations did not get rendered due to their size.
• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.falsum = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkSigma ⊥ ⋯
• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.falsum = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPi ⊥ ⋯

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.and {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : ℬ.HierarchySymbol} : HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ

Equations

• φ.and ψ = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkSigma (↑φ ⋏ ↑ψ) ⋯
• φ.and ψ = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPi (↑φ ⋏ ↑ψ) ⋯
• φ.and ψ = (FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkSigma (↑φ.sigma ⋏ ↑ψ.sigma) ⋯).mkDelta (FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPi (↑φ.pi ⋏ ↑ψ.pi) ⋯)

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.or {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : ℬ.HierarchySymbol} : HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ

Equations

• φ.or ψ = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkSigma (↑φ ⋎ ↑ψ) ⋯
• φ.or ψ = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPi (↑φ ⋎ ↑ψ) ⋯
• φ.or ψ = (FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkSigma (↑φ.sigma ⋎ ↑ψ.sigma) ⋯).mkDelta (FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPi (↑φ.pi ⋎ ↑ψ.pi) ⋯)

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.negSigma {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }) : HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }

Equations

• φ.negSigma = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPi (∼↑φ) ⋯

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.negPi {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }) : HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }

Equations

• φ.negPi = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkSigma (∼↑φ) ⋯

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.negDelta {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) : HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }

Equations

• φ.negDelta = φ.pi.negPi.mkDelta φ.sigma.negSigma

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ball {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {R : Semiformula.Operator L 2} (hR : R ∈ ℬ) (t : Semiterm L ξ n) {Γ : ℬ.HierarchySymbol} : HierarchySymbol.Semiformula ξ (n + 1) Γ → HierarchySymbol.Semiformula ξ n Γ

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.bexs {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {R : Semiformula.Operator L 2} (hR : R ∈ ℬ) (t : Semiterm L ξ n) {Γ : ℬ.HierarchySymbol} : HierarchySymbol.Semiformula ξ (n + 1) Γ → HierarchySymbol.Semiformula ξ n Γ

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.all {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ (n + 1) { Γ := 𝚷, rank := m + 1 }) : HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m + 1 }

Equations

• φ.all = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkPi (∀¹ ↑φ) ⋯

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.exs {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ (n + 1) { Γ := 𝚺, rank := m + 1 }) : HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m + 1 }

Equations

• φ.exs = FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.mkSigma (∃¹ ↑φ) ⋯

@[instance_reducible]

instance FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instTop {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : ℬ.HierarchySymbol} : Top (HierarchySymbol.Semiformula ξ n Γ)

Equations

• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instTop = { top := FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.verum }

@[instance_reducible]

instance FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instBot {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : ℬ.HierarchySymbol} : Bot (HierarchySymbol.Semiformula ξ n Γ)

Equations

• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instBot = { bot := FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.falsum }

@[instance_reducible]

instance FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instWedge {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : ℬ.HierarchySymbol} : Wedge (HierarchySymbol.Semiformula ξ n Γ)

Equations

• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instWedge = { wedge := FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.and }

@[instance_reducible]

instance FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instVee {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : ℬ.HierarchySymbol} : Vee (HierarchySymbol.Semiformula ξ n Γ)

Equations

• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instVee = { vee := FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.or }

@[instance_reducible]

instance FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instTildeMkDeltaSigmaPiDelta {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} : Tilde (HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m })

Equations

• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instTildeMkDeltaSigmaPiDelta = { tilde := FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.negDelta }

@[instance_reducible]

instance FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instLogicalConnectiveMkDeltaSigmaPiDelta {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} : LogicalConnective (HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m })

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instExsQuantifierMkSigmaSigmaPiDeltaHAddNatOfNat {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {m : ℕ} : ExsQuantifier fun (n : ℕ) => HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m + 1 }

Equations

• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instExsQuantifierMkSigmaSigmaPiDeltaHAddNatOfNat = { exs := fun {n : ℕ} => FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.exs }

@[instance_reducible]

instance FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instUnivQuantifierMkPiSigmaPiDeltaHAddNatOfNat {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {m : ℕ} : UnivQuantifier fun (n : ℕ) => HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m + 1 }

Equations

• FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.instUnivQuantifierMkPiSigmaPiDeltaHAddNatOfNat = { all := fun {n : ℕ} => FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.all }

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.substSigma {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ 1 { Γ := 𝚺, rank := m + 1 }) (F : HierarchySymbol.Semiformula ξ (n + 1) { Γ := 𝚺, rank := m + 1 }) : HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m + 1 }

Equations

• φ.substSigma F = (F ⋏ FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.rew (FFL.FirstOrder.Rew.subst ![FFL.FirstOrder.Semiterm.bvar 0]) φ).exs

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_verum {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : ℬ.HierarchySymbol} : ↑⊤ = ⊤

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.sigma_verum {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} : ⊤.sigma = ⊤

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.pi_verum {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} : ⊤.pi = ⊤

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_falsum {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : ℬ.HierarchySymbol} : ↑⊥ = ⊥

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.sigma_falsum {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} : ⊥.sigma = ⊥

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.pi_falsum {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} : ⊥.pi = ⊥

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_and {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : ℬ.HierarchySymbol} (φ ψ : HierarchySymbol.Semiformula ξ n Γ) : ↑(φ ⋏ ψ) = ↑φ ⋏ ↑ψ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.sigma_and {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ ψ : HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) : (φ ⋏ ψ).sigma = φ.sigma ⋏ ψ.sigma

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.pi_and {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ ψ : HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) : (φ ⋏ ψ).pi = φ.pi ⋏ ψ.pi

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_or {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : ℬ.HierarchySymbol} (φ ψ : HierarchySymbol.Semiformula ξ n Γ) : ↑(φ ⋎ ψ) = ↑φ ⋎ ↑ψ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.sigma_or {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ ψ : HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) : (φ ⋎ ψ).sigma = φ.sigma ⋎ ψ.sigma

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.pi_or {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ ψ : HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) : (φ ⋎ ψ).pi = φ.pi ⋎ ψ.pi

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_negSigma {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }) : ↑φ.negSigma = ∼↑φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_negPi {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }) : ↑φ.negPi = ∼↑φ

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_negDelta {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) : ↑(∼φ) = ∼↑φ.pi

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.sigma_negDelta {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) : (∼φ).sigma = φ.pi.negPi

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.sigma_negPi {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) : (∼φ).pi = φ.sigma.negSigma

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_ball {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : ℬ.HierarchySymbol} {R : Semiformula.Operator L 2} (hR : R ∈ ℬ) (t : Semiterm L ξ n) (φ : HierarchySymbol.Semiformula ξ (n + 1) Γ) : ↑(ball hR t φ) = ∀¹[R.operator ![Semiterm.bvar 0, Rew.bShift t]] ↑φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_bexs {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n : ℕ} {Γ : ℬ.HierarchySymbol} {R : Semiformula.Operator L 2} (hR : R ∈ ℬ) (t : Semiterm L ξ n) (φ : HierarchySymbol.Semiformula ξ (n + 1) Γ) : ↑(bexs hR t φ) = ∃¹[R.operator ![Semiterm.bvar 0, Rew.bShift t]] ↑φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_exsSigma {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ (n + 1) { Γ := 𝚺, rank := m + 1 }) : ↑φ.exs = ∃¹ ↑φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.val_allPi {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ (n + 1) { Γ := 𝚷, rank := m + 1 }) : ↑φ.all = ∀¹ ↑φ

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperOn.verum {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] : ProperOn M ⊤

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperOn.falsum {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] : ProperOn M ⊥

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperOn.and {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] {φ ψ : { Γ := 𝚫, rank := m }.Semisentence k} (hp : ProperOn M φ) (hq : ProperOn M ψ) : ProperOn M (φ ⋏ ψ)

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperOn.or {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] {φ ψ : { Γ := 𝚫, rank := m }.Semisentence k} (hp : ProperOn M φ) (hq : ProperOn M ψ) : ProperOn M (φ ⋎ ψ)

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperOn.neg {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] {φ : { Γ := 𝚫, rank := m }.Semisentence k} (hp : ProperOn M φ) : ProperOn M (∼φ)

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperOn.eval_neg {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] {φ : { Γ := 𝚫, rank := m }.Semisentence k} (hp : ProperOn M φ) (e : Fin k → M) : (Semiformula.Evalb e) ↑(∼φ) ↔ ¬(Semiformula.Evalb e) ↑φ

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperOn.ball {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] {R : Semiformula.Operator L 2} (hR : R ∈ ℬ) {t : Semiterm L Empty k} {φ : { Γ := 𝚫, rank := m + 1 }.Semisentence (k + 1)} (hp : ProperOn M φ) : ProperOn M (Semiformula.ball hR t φ)

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperOn.bexs {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] {R : Semiformula.Operator L 2} (hR : R ∈ ℬ) {t : Semiterm L Empty k} {φ : { Γ := 𝚫, rank := m + 1 }.Semisentence (k + 1)} (hp : ProperOn M φ) : ProperOn M (Semiformula.bexs hR t φ)

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperWithParamOn.verum {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] : ProperWithParamOn M ⊤

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperWithParamOn.falsum {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] : ProperWithParamOn M ⊥

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperWithParamOn.and {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] {φ ψ : HierarchySymbol.Semiformula M k { Γ := 𝚫, rank := m }} (hp : ProperWithParamOn M φ) (hq : ProperWithParamOn M ψ) : ProperWithParamOn M (φ ⋏ ψ)

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperWithParamOn.or {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] {φ ψ : HierarchySymbol.Semiformula M k { Γ := 𝚫, rank := m }} (hp : ProperWithParamOn M φ) (hq : ProperWithParamOn M ψ) : ProperWithParamOn M (φ ⋎ ψ)

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperWithParamOn.neg {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] {φ : HierarchySymbol.Semiformula M k { Γ := 𝚫, rank := m }} (hp : ProperWithParamOn M φ) : ProperWithParamOn M (∼φ)

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperWithParamOn.eval_neg {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] {φ : HierarchySymbol.Semiformula M k { Γ := 𝚫, rank := m }} (hp : ProperWithParamOn M φ) (e : Fin k → M) : (Semiformula.Eval e id) ↑(∼φ) ↔ ¬(Semiformula.Eval e id) ↑φ

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperWithParamOn.ball {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] {R : Semiformula.Operator L 2} (hR : R ∈ ℬ) {t : Semiterm L M k} {φ : HierarchySymbol.Semiformula M (k + 1) { Γ := 𝚫, rank := m }} (hp : ProperWithParamOn M φ) : ProperWithParamOn M (Semiformula.ball hR t φ)

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.ProperWithParamOn.bexs {L : Language} {ℬ : Bounding L} {m k : ℕ} {M : Type u_4} [Tarski.Structure L M] {R : Semiformula.Operator L 2} (hR : R ∈ ℬ) {t : Semiterm L M k} {φ : HierarchySymbol.Semiformula M (k + 1) { Γ := 𝚫, rank := m }} (hp : ProperWithParamOn M φ) : ProperWithParamOn M (Semiformula.bexs hR t φ)

def FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.graphDelta {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {m k : ℕ} [L.Eq] (φ : HierarchySymbol.Semiformula ξ (k + 1) { Γ := 𝚺, rank := m }) : HierarchySymbol.Semiformula ξ (k + 1) { Γ := 𝚫, rank := m }

Equations

• One or more equations did not get rendered due to their size.
• φ_2.graphDelta = φ_2.ofZero { Γ := 𝚫, rank := 0 }

@[simp]

theorem FFL.FirstOrder.Bounding.HierarchySymbol.Semiformula.graphDelta_val {L : Language} {ℬ : Bounding L} {ξ : Type u_1} {m k : ℕ} [L.Eq] (φ : HierarchySymbol.Semiformula ξ (k + 1) { Γ := 𝚺, rank := m }) : ↑φ.graphDelta = ↑φ