Supporting results for pointwise provable equality.

Formulas of first-order logic

This file defines the formulas of first-order logic.

φ : Semiformula L ξ n is a (semi-)formula of language L with bounded variables of Fin n and free variables of ξ. The quantification is represented by de Bruijn index.

inductive PointwiseComposition.FFL.FirstOrder.Semiformula (L : Language) (ξ : Type u_1) : ℕ → Type (max u_1 u_2)

A semiformula of language L. Free variables are of type ξ, and bound variables are implemented as de Bruijn indices, of a type Fin n separate from free variables.

• verum {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformula L ξ n
• falsum {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformula L ξ n
• rel {L : Language} {ξ : Type u_1} {n arity : ℕ} : L.Rel arity → (Fin arity → Semiterm L ξ n) → Semiformula L ξ n
• nrel {L : Language} {ξ : Type u_1} {n arity : ℕ} : L.Rel arity → (Fin arity → Semiterm L ξ n) → Semiformula L ξ n
• and {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformula L ξ n → Semiformula L ξ n → Semiformula L ξ n
• or {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformula L ξ n → Semiformula L ξ n → Semiformula L ξ n
• all {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformula L ξ (n + 1) → Semiformula L ξ n
• exs {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformula L ξ (n + 1) → Semiformula L ξ n

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Formula (L : Language) (ξ : Type u_1) : Type (max u_1 u_2)

The Formula construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.Formula L ξ = PointwiseComposition.FFL.FirstOrder.Semiformula L ξ 0

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Sentence (L : Language) : Type u_1

The Sentence construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.Sentence L = PointwiseComposition.FFL.FirstOrder.Formula L Empty

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semisentence (L : Language) (n : ℕ) : Type u_1

The Semisentence construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.Semisentence L n = PointwiseComposition.FFL.FirstOrder.Semiformula L Empty n

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiproposition (L : Language) (n : ℕ) : Type u_1

The Semiproposition construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiproposition L n = PointwiseComposition.FFL.FirstOrder.Semiformula L ℕ n

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Proposition (L : Language) : Type u_1

The Proposition construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.Proposition L = PointwiseComposition.FFL.FirstOrder.Semiproposition L 0

def PointwiseComposition.FFL.FirstOrder.Semiformula.neg {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformula L ξ n → Semiformula L ξ n

The neg construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.verum.neg = PointwiseComposition.FFL.FirstOrder.Semiformula.falsum
• PointwiseComposition.FFL.FirstOrder.Semiformula.falsum.neg = PointwiseComposition.FFL.FirstOrder.Semiformula.verum
• (PointwiseComposition.FFL.FirstOrder.Semiformula.rel r v).neg = PointwiseComposition.FFL.FirstOrder.Semiformula.nrel r v
• (PointwiseComposition.FFL.FirstOrder.Semiformula.nrel r v).neg = PointwiseComposition.FFL.FirstOrder.Semiformula.rel r v
• (φ.and ψ).neg = φ.neg.or ψ.neg
• (φ.or ψ).neg = φ.neg.and ψ.neg
• φ.all.neg = φ.neg.exs
• φ.exs.neg = φ.neg.all

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.neg_neg {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) : φ.neg.neg = φ

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiformula.instLogicalConnective {L : Language} {ξ : Type u_1} {n : ℕ} : LogicalConnective (Semiformula L ξ n)

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiformula.instLogicalNeutral {L : Language} {ξ : Type u_1} {n : ℕ} : LogicalNeutral (Semiformula L ξ n)

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Semiformula.instTildeInvolutive {L : Language} {ξ : Type u_1} {n : ℕ} : TildeInvolutive (Semiformula L ξ n)

instance PointwiseComposition.FFL.FirstOrder.Semiformula.instDeMorgan {L : Language} {ξ : Type u_1} {n : ℕ} : LogicalConnective.DeMorgan (Semiformula L ξ n)

instance PointwiseComposition.FFL.FirstOrder.Semiformula.instDeMorgan_1 {L : Language} {ξ : Type u_1} {n : ℕ} : LogicalNeutral.DeMorgan (Semiformula L ξ n)

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiformula.instQuantifier {L : Language} {ξ : Type u_1} : Quantifier (Semiformula L ξ)

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiformula.toStr {L : Language} {ξ : Type u_1} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] [ToString ξ] {n : ℕ} : Semiformula L ξ n → String

The to Str construction in FFL.FirstOrder.Semiformula.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.Semiformula.verum.toStr = "\\top"
• PointwiseComposition.FFL.FirstOrder.Semiformula.falsum.toStr = "\\bot"
• (PointwiseComposition.FFL.FirstOrder.Semiformula.rel r a).toStr = "{" ++ toString r ++ "}"
• (PointwiseComposition.FFL.FirstOrder.Semiformula.nrel r a).toStr = "\\lnot {" ++ toString r ++ "}"
• (φ.and ψ).toStr = "\\left(" ++ φ.toStr ++ " \\land " ++ ψ.toStr ++ "\\right)"
• (φ.or ψ).toStr = "\\left(" ++ φ.toStr ++ " \\lor " ++ ψ.toStr ++ "\\right)"
• φ.all.toStr = "(\\forall x_{" ++ toString n ++ "}) " ++ φ.toStr
• φ.exs.toStr = "(\\exists x_{" ++ toString n ++ "}) " ++ φ.toStr

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiformula.instRepr {L : Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] [ToString ξ] : Repr (Semiformula L ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.instRepr = { reprPrec := fun (t : PointwiseComposition.FFL.FirstOrder.Semiformula L ξ n) (x : ℕ) => Std.Format.text t.toStr }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiformula.instToString {L : Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] [ToString ξ] : ToString (Semiformula L ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.instToString = { toString := PointwiseComposition.FFL.FirstOrder.Semiformula.toStr }

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.neg_rel {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : ∼rel r v = nrel r v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.neg_nrel {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : ∼nrel r v = rel r v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.neg_all {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) : ∼(∀¹ φ) = ∃¹ ∼φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.neg_ex {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) : ∼(∃¹ φ) = ∀¹ ∼φ

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiformula.toPrenex {L : Language} {ξ : Type u_1} {n : ℕ} (Γ : Polarity) (s : ℕ) (φ : Semiformula L ξ (n + s)) : Semiformula L ξ n

φ.toPrenex Γ s prefixes φ with s alternating quantifiers, the outermost one being Γ.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.toPrenex Γ s φ = Γ.quantItr s φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.neg_quant {L : Language} {ξ : Type u_1} {n : ℕ} (Γ : Polarity) (φ : Semiformula L ξ (n + 1)) : ∼Γ.quant φ = Γ.alt.quant (∼φ)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.neg_toPrenex {L : Language} {ξ : Type u_1} {n : ℕ} (Γ : Polarity) (s : ℕ) (φ : Semiformula L ξ (n + s)) : ∼toPrenex Γ s φ = toPrenex Γ.alt s (∼φ)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.neg_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : ∼φ = ∼ψ ↔ φ = ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.neg_allClosure {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) : ∼(∀¹* φ) = ∃¹* ∼φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.neg_exsClosure {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) : ∼(∃¹* φ) = ∀¹* ∼φ

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.neg_eq {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) : ∼φ = φ.neg

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.imp_eq {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : φ ⇒ₗ ψ = ∼φ ⋎ ψ

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.iff_eq {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : φ ⇔ₗ ψ = (∼φ ⋎ ψ) ⋏ (∼ψ ⋎ φ)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.ball_eq {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ (n + 1)) : (∀¹[φ] ψ) = ∀¹ (φ ⇒ₗ ψ)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.bexs_eq {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ (n + 1)) : (∃¹[φ] ψ) = ∃¹ φ ⋏ ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.neg_ball {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ (n + 1)) : ∼(∀¹[φ] ψ) = ∃¹[φ] ∼ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.neg_bexs {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ (n + 1)) : ∼(∃¹[φ] ψ) = ∀¹[φ] ∼ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.and_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ₁ ψ₁ φ₂ ψ₂ : Semiformula L ξ n) : φ₁ ⋏ φ₂ = ψ₁ ⋏ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.or_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ₁ ψ₁ φ₂ ψ₂ : Semiformula L ξ n) : φ₁ ⋎ φ₂ = ψ₁ ⋎ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.all_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ (n + 1)) : ∀¹ φ = ∀¹ ψ ↔ φ = ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.exs_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ (n + 1)) : ∃¹ φ = ∃¹ ψ ↔ φ = ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.allClosure_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : ∀¹* φ = ∀¹* ψ ↔ φ = ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.exsClosure_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : ∃¹* φ = ∃¹* ψ ↔ φ = ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.allItr_inj {L : Language} {ξ : Type u_1} {n k : ℕ} (φ ψ : Semiformula L ξ (n + k)) : ∀¹^[k] φ = ∀¹^[k] ψ ↔ φ = ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.exsItr_inj {L : Language} {ξ : Type u_1} {n k : ℕ} (φ ψ : Semiformula L ξ (n + k)) : ∃¹^[k] φ = ∃¹^[k] ψ ↔ φ = ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.imp_inj {L : Language} {ξ : Type u_1} {n : ℕ} {φ₁ φ₂ ψ₁ ψ₂ : Semiformula L ξ n} : φ₁ ⇒ₗ φ₂ = ψ₁ ⇒ₗ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiformula.relProof {ξ : Type u_1} {n : ℕ} (L : Language) (k : ℕ) (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : Semiformula L ξ n

The rel! construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.relProof L k r v = PointwiseComposition.FFL.FirstOrder.Semiformula.rel r v

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiformula.nrelProof {ξ : Type u_1} {n : ℕ} (L : Language) (k : ℕ) (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : Semiformula L ξ n

The nrel! construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.nrelProof L k r v = PointwiseComposition.FFL.FirstOrder.Semiformula.nrel r v

def PointwiseComposition.FFL.FirstOrder.Semiformula.complexity {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformula L ξ n → ℕ

The complexity of a semiformula, taking max at logical connectives.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.verum.complexity = 0
• PointwiseComposition.FFL.FirstOrder.Semiformula.falsum.complexity = 0
• (PointwiseComposition.FFL.FirstOrder.Semiformula.rel r v).complexity = 0
• (PointwiseComposition.FFL.FirstOrder.Semiformula.nrel r v).complexity = 0
• (φ.and ψ).complexity = max φ.complexity ψ.complexity + 1
• (φ.or ψ).complexity = max φ.complexity ψ.complexity + 1
• φ.all.complexity = φ.complexity + 1
• φ.exs.complexity = φ.complexity + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.complexity_top {L : Language} {ξ : Type u_1} {n : ℕ} : ⊤.complexity = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.complexity_bot {L : Language} {ξ : Type u_1} {n : ℕ} : ⊥.complexity = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.complexity_rel {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : (rel r v).complexity = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.complexity_nrel {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : (nrel r v).complexity = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.complexity_and {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ ⋏ ψ).complexity = max φ.complexity ψ.complexity + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.complexity_and' {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ.and ψ).complexity = max φ.complexity ψ.complexity + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.complexity_or {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ ⋎ ψ).complexity = max φ.complexity ψ.complexity + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.complexity_or' {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ.or ψ).complexity = max φ.complexity ψ.complexity + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.complexity_all {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) : (∀¹ φ).complexity = φ.complexity + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.complexity_all' {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) : φ.all.complexity = φ.complexity + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.complexity_exs {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) : (∃¹ φ).complexity = φ.complexity + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.complexity_exs' {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) : φ.exs.complexity = φ.complexity + 1

def PointwiseComposition.FFL.FirstOrder.Semiformula.cases' {L : Language} {ξ : Type u_1} {C : (n : ℕ) → Semiformula L ξ n → Sort w} (hverum : {n : ℕ} → C n ⊤) (hfalsum : {n : ℕ} → C n ⊥) (hrel : {n k : ℕ} → (r : L.Rel k) → (v : Fin k → Semiterm L ξ n) → C n (rel r v)) (hnrel : {n k : ℕ} → (r : L.Rel k) → (v : Fin k → Semiterm L ξ n) → C n (nrel r v)) (hand : {n : ℕ} → (φ ψ : Semiformula L ξ n) → C n (φ ⋏ ψ)) (hor : {n : ℕ} → (φ ψ : Semiformula L ξ n) → C n (φ ⋎ ψ)) (hall : {n : ℕ} → (φ : Semiformula L ξ (n + 1)) → C n (∀¹ φ)) (hexs : {n : ℕ} → (φ : Semiformula L ξ (n + 1)) → C n (∃¹ φ)) {n : ℕ} (φ : Semiformula L ξ n) : C n φ

The cases' construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hexs PointwiseComposition.FFL.FirstOrder.Semiformula.verum = hverum
• PointwiseComposition.FFL.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hexs PointwiseComposition.FFL.FirstOrder.Semiformula.falsum = hfalsum
• PointwiseComposition.FFL.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hexs (PointwiseComposition.FFL.FirstOrder.Semiformula.rel r v) = hrel r v
• PointwiseComposition.FFL.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hexs (PointwiseComposition.FFL.FirstOrder.Semiformula.nrel r v) = hnrel r v
• PointwiseComposition.FFL.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hexs (φ.and ψ) = hand φ ψ
• PointwiseComposition.FFL.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hexs (φ.or ψ) = hor φ ψ
• PointwiseComposition.FFL.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hexs φ.all = hall φ
• PointwiseComposition.FFL.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hexs φ.exs = hexs φ

def PointwiseComposition.FFL.FirstOrder.Semiformula.rec' {L : Language} {ξ : Type u_1} {C : (n : ℕ) → Semiformula L ξ n → Sort w} (hverum : {n : ℕ} → C n ⊤) (hfalsum : {n : ℕ} → C n ⊥) (hrel : {n k : ℕ} → (r : L.Rel k) → (v : Fin k → Semiterm L ξ n) → C n (rel r v)) (hnrel : {n k : ℕ} → (r : L.Rel k) → (v : Fin k → Semiterm L ξ n) → C n (nrel r v)) (hand : {n : ℕ} → (φ ψ : Semiformula L ξ n) → C n φ → C n ψ → C n (φ ⋏ ψ)) (hor : {n : ℕ} → (φ ψ : Semiformula L ξ n) → C n φ → C n ψ → C n (φ ⋎ ψ)) (hall : {n : ℕ} → (φ : Semiformula L ξ (n + 1)) → C (n + 1) φ → C n (∀¹ φ)) (hexs : {n : ℕ} → (φ : Semiformula L ξ (n + 1)) → C (n + 1) φ → C n (∃¹ φ)) {n : ℕ} (φ : Semiformula L ξ n) : C n φ

The rec' construction in FFL.FirstOrder.Semiformula.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hexs PointwiseComposition.FFL.FirstOrder.Semiformula.verum = hverum
• PointwiseComposition.FFL.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hexs PointwiseComposition.FFL.FirstOrder.Semiformula.falsum = hfalsum
• PointwiseComposition.FFL.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hexs (PointwiseComposition.FFL.FirstOrder.Semiformula.rel r v) = hrel r v
• PointwiseComposition.FFL.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hexs (PointwiseComposition.FFL.FirstOrder.Semiformula.nrel r v) = hnrel r v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.complexity_neg {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) : (∼φ).complexity = φ.complexity

def PointwiseComposition.FFL.FirstOrder.Semiformula.hasDecEq {L : Language} {ξ : Type u_1} [L.DecidableEq] [DecidableEq ξ] {n : ℕ} (φ ψ : Semiformula L ξ n) : Decidable (φ = ψ)

The has Dec Eq construction in FFL.FirstOrder.Semiformula.

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiformula.instDecidableEq {L : Language} {ξ : Type u_1} {n : ℕ} [L.DecidableEq] [DecidableEq ξ] : DecidableEq (Semiformula L ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.instDecidableEq = PointwiseComposition.FFL.FirstOrder.Semiformula.hasDecEq

Quantifier rank

def PointwiseComposition.FFL.FirstOrder.Semiformula.qr {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformula L ξ n → ℕ

The qr construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.verum.qr = 0
• PointwiseComposition.FFL.FirstOrder.Semiformula.falsum.qr = 0
• (PointwiseComposition.FFL.FirstOrder.Semiformula.rel r v).qr = 0
• (PointwiseComposition.FFL.FirstOrder.Semiformula.nrel r v).qr = 0
• (φ.and ψ).qr = max φ.qr ψ.qr
• (φ.or ψ).qr = max φ.qr ψ.qr
• φ.all.qr = φ.qr + 1
• φ.exs.qr = φ.qr + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.qr_top {L : Language} {ξ : Type u_1} {n : ℕ} : ⊤.qr = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.qr_bot {L : Language} {ξ : Type u_1} {n : ℕ} : ⊥.qr = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.qr_rel {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : (rel r v).qr = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.qr_nrel {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : (nrel r v).qr = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.qr_and {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ ⋏ ψ).qr = max φ.qr ψ.qr

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.qr_or {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ ⋎ ψ).qr = max φ.qr ψ.qr

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.qr_all {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) : (∀¹ φ).qr = φ.qr + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.qr_exs {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) : (∃¹ φ).qr = φ.qr + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.qr_neg {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) : (∼φ).qr = φ.qr

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.qr_imply {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ ⇒ₗ ψ).qr = max φ.qr ψ.qr

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.qr_iff {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ ⇔ₗ ψ).qr = max φ.qr ψ.qr

Open (Semi-)Formula

def PointwiseComposition.FFL.FirstOrder.Semiformula.Open {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) : Prop

The Open construction in FFL.FirstOrder.Semiformula.

Equations

• φ.Open = (φ.qr = 0)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.open_top {L : Language} {ξ : Type u_1} {n : ℕ} : ⊤.Open

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.open_bot {L : Language} {ξ : Type u_1} {n : ℕ} : ⊥.Open

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.open_rel {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : (rel r v).Open

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.open_nrel {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : (nrel r v).Open

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.open_and {L : Language} {ξ : Type u_1} {n : ℕ} {φ ψ : Semiformula L ξ n} : (φ ⋏ ψ).Open ↔ φ.Open ∧ ψ.Open

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.open_or {L : Language} {ξ : Type u_1} {n : ℕ} {φ ψ : Semiformula L ξ n} : (φ ⋎ ψ).Open ↔ φ.Open ∧ ψ.Open

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.not_open_all {L : Language} {ξ : Type u_1} {n : ℕ} {φ : Semiformula L ξ (n + 1)} : ¬(∀¹ φ).Open

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.not_open_exs {L : Language} {ξ : Type u_1} {n : ℕ} {φ : Semiformula L ξ (n + 1)} : ¬(∃¹ φ).Open

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.open_neg {L : Language} {ξ : Type u_1} {n : ℕ} {φ : Semiformula L ξ n} : (∼φ).Open ↔ φ.Open

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.open_imply {L : Language} {ξ : Type u_1} {n : ℕ} {φ ψ : Semiformula L ξ n} : (φ ⇒ₗ ψ).Open ↔ φ.Open ∧ ψ.Open

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.open_iff {L : Language} {ξ : Type u_1} {n : ℕ} {φ ψ : Semiformula L ξ n} : (φ ⇔ₗ ψ).Open ↔ φ.Open ∧ ψ.Open

Free Variables

def PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables {L : Language} {ξ : Type u_1} [DecidableEq ξ] {n : ℕ} : Semiformula L ξ n → Finset ξ

The free Variables construction in FFL.FirstOrder.Semiformula.

Equations

• (PointwiseComposition.FFL.FirstOrder.Semiformula.rel a v).freeVariables = Finset.univ.biUnion fun (i : Fin arity) => (v i).freeVariables
• (PointwiseComposition.FFL.FirstOrder.Semiformula.nrel a v).freeVariables = Finset.univ.biUnion fun (i : Fin arity) => (v i).freeVariables
• PointwiseComposition.FFL.FirstOrder.Semiformula.verum.freeVariables = ∅
• PointwiseComposition.FFL.FirstOrder.Semiformula.falsum.freeVariables = ∅
• (φ.and ψ).freeVariables = φ.freeVariables ∪ ψ.freeVariables
• (φ.or ψ).freeVariables = φ.freeVariables ∪ ψ.freeVariables
• φ.all.freeVariables = φ.freeVariables
• φ.exs.freeVariables = φ.freeVariables

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables_rel {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : (rel r v).freeVariables = Finset.univ.biUnion fun (i : Fin k) => (v i).freeVariables

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables_nrel {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : (nrel r v).freeVariables = Finset.univ.biUnion fun (i : Fin k) => (v i).freeVariables

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables_verum {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] : ⊤.freeVariables = ∅

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables_falsum {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] : ⊥.freeVariables = ∅

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables_and {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (φ ψ : Semiformula L ξ n) : (φ ⋏ ψ).freeVariables = φ.freeVariables ∪ ψ.freeVariables

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables_or {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (φ ψ : Semiformula L ξ n) : (φ ⋎ ψ).freeVariables = φ.freeVariables ∪ ψ.freeVariables

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables_all {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ (n + 1)) : (∀¹ φ).freeVariables = φ.freeVariables

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables_exs {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ (n + 1)) : (∃¹ φ).freeVariables = φ.freeVariables

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables_not {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ n) : (∼φ).freeVariables = φ.freeVariables

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables_imp {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (φ ψ : Semiformula L ξ n) : (φ ⇒ₗ ψ).freeVariables = φ.freeVariables ∪ ψ.freeVariables

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables_allClosure {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ n) : (∀¹* φ).freeVariables = φ.freeVariables

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables_sentence {L : Language} {n : ℕ} {ο : Type u_5} [IsEmpty ο] (φ : Semiformula L ο n) : φ.freeVariables = ∅

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiformula.HasFreeVariable {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ n) (x : ξ) : Prop

The FVar? construction in FFL.FirstOrder.Semiformula.

Equations

• φ.HasFreeVariable x = (x ∈ φ.freeVariables)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.hasFreeVariable_rel {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {x : ξ} {k : ℕ} {R : L.Rel k} {v : Fin k → Semiterm L ξ n} : (rel R v).HasFreeVariable x ↔ ∃ (i : Fin k), (v i).HasFreeVariable x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.hasFreeVariable_nrel {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {x : ξ} {k : ℕ} {R : L.Rel k} {v : Fin k → Semiterm L ξ n} : (nrel R v).HasFreeVariable x ↔ ∃ (i : Fin k), (v i).HasFreeVariable x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.hasFreeVariable_top {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x : ξ) : ¬⊤.HasFreeVariable x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.hasFreeVariable_falsum {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x : ξ) : ¬⊥.HasFreeVariable x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.hasFreeVariable_and {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x : ξ) (φ ψ : Semiformula L ξ n) : (φ ⋏ ψ).HasFreeVariable x ↔ φ.HasFreeVariable x ∨ ψ.HasFreeVariable x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.hasFreeVariable_or {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x : ξ) (φ ψ : Semiformula L ξ n) : (φ ⋎ ψ).HasFreeVariable x ↔ φ.HasFreeVariable x ∨ ψ.HasFreeVariable x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.hasFreeVariable_all {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x : ξ) (φ : Semiformula L ξ (n + 1)) : (∀¹ φ).HasFreeVariable x ↔ φ.HasFreeVariable x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.hasFreeVariable_exs {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x : ξ) (φ : Semiformula L ξ (n + 1)) : (∃¹ φ).HasFreeVariable x ↔ φ.HasFreeVariable x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.hasFreeVariable_allClosure {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x : ξ) (φ : Semiformula L ξ n) : (∀¹* φ).HasFreeVariable x ↔ φ.HasFreeVariable x

def PointwiseComposition.FFL.FirstOrder.Semiformula.fvSup {L : Language} {n : ℕ} (φ : Semiproposition L n) : ℕ

The fv Sup construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.fvSup φ = WithBot.recBotCoe 0 Nat.succ (PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables φ).max

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lt_fvSup_of_hasFreeVariable {L : Language} {n m : ℕ} {φ : Semiproposition L n} : HasFreeVariable φ m → m < fvSup φ

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.not_hasFreeVariable_of_lt_fvSup {L : Language} {n m : ℕ} (φ : Semiproposition L n) (h : fvSup φ ≤ m) : ¬HasFreeVariable φ m

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.not_hasFreeVariable_fvSup {L : Language} {n : ℕ} (φ : Semiproposition L n) : ¬HasFreeVariable φ (fvSup φ)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.List.maximumOption_some_of_not_nil {α : Type u_5} [LinearOrder α] {l : List α} (h : l ≠ []) : l.max?.isSome = true

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.List.maximumOption_eq_some {α : Type u_5} [LinearOrder α] [Std.LawfulOrderSup α] {l : List α} {a : α} (h : l.max? = some a) (x : α) : x ∈ l → x ≤ a

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.ne_of_ne_complexity {L : Language} {ξ : Type u_1} {n : ℕ} {φ ψ : Semiformula L ξ n} (h : φ.complexity ≠ ψ.complexity) : φ ≠ ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.ne_or_left {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : φ ≠ φ ⋎ ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.ne_or_right {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : ψ ≠ φ ⋎ ψ

def PointwiseComposition.FFL.FirstOrder.Semiformula.lMapAux {L₁ : Language} {L₂ : Language} {ξ : Type u_5} (Φ : L₁.Hom L₂) {n : ℕ} : Semiformula L₁ ξ n → Semiformula L₂ ξ n

The l Map Aux construction in FFL.FirstOrder.Semiformula.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.Semiformula.lMapAux Φ PointwiseComposition.FFL.FirstOrder.Semiformula.verum = ⊤
• PointwiseComposition.FFL.FirstOrder.Semiformula.lMapAux Φ PointwiseComposition.FFL.FirstOrder.Semiformula.falsum = ⊥
• PointwiseComposition.FFL.FirstOrder.Semiformula.lMapAux Φ (φ.and ψ) = PointwiseComposition.FFL.FirstOrder.Semiformula.lMapAux Φ φ ⋏ PointwiseComposition.FFL.FirstOrder.Semiformula.lMapAux Φ ψ
• PointwiseComposition.FFL.FirstOrder.Semiformula.lMapAux Φ (φ.or ψ) = PointwiseComposition.FFL.FirstOrder.Semiformula.lMapAux Φ φ ⋎ PointwiseComposition.FFL.FirstOrder.Semiformula.lMapAux Φ ψ
• PointwiseComposition.FFL.FirstOrder.Semiformula.lMapAux Φ φ.all = ∀¹ PointwiseComposition.FFL.FirstOrder.Semiformula.lMapAux Φ φ
• PointwiseComposition.FFL.FirstOrder.Semiformula.lMapAux Φ φ.exs = ∃¹ PointwiseComposition.FFL.FirstOrder.Semiformula.lMapAux Φ φ

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMapAux_neg {L₁ : Language} {L₂ : Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} {n : ℕ} (φ : Semiformula L₁ ξ n) : lMapAux Φ (∼φ) = ∼lMapAux Φ φ

def PointwiseComposition.FFL.FirstOrder.Semiformula.lMap {L₁ : Language} {L₂ : Language} {ξ : Type u_5} (Φ : L₁.Hom L₂) {n : ℕ} : Semiformula L₁ ξ n →ˡᶜ Semiformula L₂ ξ n

The map on semiformulas induced by a homomorphism between languages.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_rel {n : ℕ} {L₁ : Language} {L₂ : Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} {k : ℕ} (r : L₁.Rel k) (v : Fin k → Semiterm L₁ ξ n) : (lMap Φ) (rel r v) = rel (Φ.rel r) (Semiterm.lMap Φ ∘ v)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_nrel {n : ℕ} {L₁ : Language} {L₂ : Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} {k : ℕ} (r : L₁.Rel k) (v : Fin k → Semiterm L₁ ξ n) : (lMap Φ) (nrel r v) = nrel (Φ.rel r) (Semiterm.lMap Φ ∘ v)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_all {n : ℕ} {L₁ : Language} {L₂ : Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} (φ : Semiformula L₁ ξ (n + 1)) : (lMap Φ) (∀¹ φ) = ∀¹ (lMap Φ) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_exs {n : ℕ} {L₁ : Language} {L₂ : Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} (φ : Semiformula L₁ ξ (n + 1)) : (lMap Φ) (∃¹ φ) = ∃¹ (lMap Φ) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_ball {n : ℕ} {L₁ : Language} {L₂ : Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} (φ ψ : Semiformula L₁ ξ (n + 1)) : (lMap Φ) (∀¹[φ] ψ) = ∀¹[(lMap Φ) φ] (lMap Φ) ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_bexs {n : ℕ} {L₁ : Language} {L₂ : Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} (φ ψ : Semiformula L₁ ξ (n + 1)) : (lMap Φ) (∃¹[φ] ψ) = ∃¹[(lMap Φ) φ] (lMap Φ) ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_allClosure {n : ℕ} {L₁ : Language} {L₂ : Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} (φ : Semiformula L₁ ξ n) : (lMap Φ) (∀¹* φ) = ∀¹* (lMap Φ) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_exsClosure {n : ℕ} {L₁ : Language} {L₂ : Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} (φ : Semiformula L₁ ξ n) : (lMap Φ) (∃¹* φ) = ∃¹* (lMap Φ) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_allItr {n : ℕ} {L₁ : Language} {L₂ : Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} {k : ℕ} (φ : Semiformula L₁ ξ (n + k)) : (lMap Φ) (∀¹^[k] φ) = ∀¹^[k] (lMap Φ) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_exsItr {n : ℕ} {L₁ : Language} {L₂ : Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} {k : ℕ} (φ : Semiformula L₁ ξ (n + k)) : (lMap Φ) (∃¹^[k] φ) = ∃¹^[k] (lMap Φ) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables_lMap {n : ℕ} {L₁ : Language} {L₂ : Language} {ξ : Type u_5} [DecidableEq ξ] (Φ : L₁.Hom L₂) (φ : Semiformula L₁ ξ n) : ((lMap Φ) φ).freeVariables = φ.freeVariables

def PointwiseComposition.FFL.FirstOrder.Semiformula.fvarList {L : Language} {ξ : Type u_5} {n : ℕ} : Semiformula L ξ n → List ξ

The fvar List construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.verum.fvarList = []
• PointwiseComposition.FFL.FirstOrder.Semiformula.falsum.fvarList = []
• (PointwiseComposition.FFL.FirstOrder.Semiformula.rel r v).fvarList = (PointwiseComposition.Matrix.toList fun (i : Fin arity) => (v i).fvarList).flatten
• (PointwiseComposition.FFL.FirstOrder.Semiformula.nrel r v).fvarList = (PointwiseComposition.Matrix.toList fun (i : Fin arity) => (v i).fvarList).flatten
• (φ.and ψ).fvarList = φ.fvarList ++ ψ.fvarList
• (φ.or ψ).fvarList = φ.fvarList ++ ψ.fvarList
• φ.all.fvarList = φ.fvarList
• φ.exs.fvarList = φ.fvarList

def PointwiseComposition.FFL.FirstOrder.Semiformula.idxOfFVar {n : ℕ} {L : Language} {ξ : Type u_5} [DecidableEq ξ] (φ : Semiformula L ξ n) : ξ → ℕ

The idx Of FVar construction in FFL.FirstOrder.Semiformula.

Equations

• φ.idxOfFVar a = List.idxOf a φ.fvarList

def PointwiseComposition.FFL.FirstOrder.Semiformula.enumerateFVar {n : ℕ} {L : Language} {ξ : Type u_5} [Inhabited ξ] (φ : Semiformula L ξ n) : ℕ → ξ

The enumerate FVar construction in FFL.FirstOrder.Semiformula.

Equations

• φ.enumerateFVar i = if hi : i < φ.fvarList.length then φ.fvarList.get ⟨i, hi⟩ else default

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.enumerateFVar_idxOfFVar {n : ℕ} {L : Language} {ξ : Type u_5} [DecidableEq ξ] [Inhabited ξ] {φ : Semiformula L ξ n} {x : ξ} (hx : x ∈ φ.fvarList) : φ.enumerateFVar (φ.idxOfFVar x) = x

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.mem_fvarList_iff_hasFreeVariable {n : ℕ} {L : Language} {ξ : Type u_5} {x : ξ} [DecidableEq ξ] {φ : Semiformula L ξ n} : x ∈ φ.fvarList ↔ φ.HasFreeVariable x

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Theory (L : Language) : Type u_1

The Theory construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.Theory L = Set (PointwiseComposition.FFL.FirstOrder.Sentence L)

def PointwiseComposition.FFL.FirstOrder.Theory.lMap {L₁ : Language} {L₂ : Language} (Φ : L₁.Hom L₂) (T : Theory L₁) : Theory L₂

The l Map construction in FFL.FirstOrder.Theory.

Equations

• PointwiseComposition.FFL.FirstOrder.Theory.lMap Φ T = ⇑(PointwiseComposition.FFL.FirstOrder.Semiformula.lMap Φ) '' T