L∞ω Semantics

This file defines the semantics of L∞ω formulas.

Main Definitions

• FirstOrder.Language.BoundedFormulaInf.Realize: Evaluation of a bounded formula in a structure.
• FirstOrder.Language.FormulaInf.Realize: Evaluation of a formula with variable assignment.
• FirstOrder.Language.SentenceInf.Realize: Truth of a sentence in a structure.

Main Results

• Simp lemmas for all connectives and quantifiers.

def FirstOrder.Language.BoundedFormulaInf.Realize {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} : L.BoundedFormulaInf α n → (α → M) → (Fin n → M) → Prop

A bounded L∞ω formula can be evaluated as true or false by giving values to each free and bound variable.

Equations

• FirstOrder.Language.BoundedFormulaInf.falsum.Realize x✝¹ x✝ = False
• (FirstOrder.Language.BoundedFormulaInf.equal t₁ t₂).Realize x✝¹ x✝ = (FirstOrder.Language.Term.realize (Sum.elim x✝¹ x✝) t₁ = FirstOrder.Language.Term.realize (Sum.elim x✝¹ x✝) t₂)
• (FirstOrder.Language.BoundedFormulaInf.rel R ts).Realize x✝¹ x✝ = FirstOrder.Language.Structure.RelMap R fun (i : Fin l) => FirstOrder.Language.Term.realize (Sum.elim x✝¹ x✝) (ts i)
• (φ.imp ψ).Realize x✝¹ x✝ = (φ.Realize x✝¹ x✝ → ψ.Realize x✝¹ x✝)
• φ.all.Realize x✝¹ x✝ = ∀ (x : M), φ.Realize x✝¹ (Fin.snoc x✝ x)
• (FirstOrder.Language.BoundedFormulaInf.iSup φs).Realize x✝¹ x✝ = ∃ (i : ι), (φs i).Realize x✝¹ x✝
• (FirstOrder.Language.BoundedFormulaInf.iInf φs).Realize x✝¹ x✝ = ∀ (i : ι), (φs i).Realize x✝¹ x✝

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_falsum {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} : falsum.Realize v xs ↔ False

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_bot {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} : ⊥.Realize v xs ↔ False

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_equal {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (t₁ t₂ : L.Term (α ⊕ Fin n)) : (equal t₁ t₂).Realize v xs ↔ Term.realize (Sum.elim v xs) t₁ = Term.realize (Sum.elim v xs) t₂

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_rel {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} {l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) : (rel R ts).Realize v xs ↔ Structure.RelMap R fun (i : Fin l) => Term.realize (Sum.elim v xs) (ts i)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_imp {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ ψ : L.BoundedFormulaInf α n) : (φ.imp ψ).Realize v xs ↔ φ.Realize v xs → ψ.Realize v xs

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_all {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ : L.BoundedFormulaInf α (n + 1)) : φ.all.Realize v xs ↔ ∀ (x : M), φ.Realize v (Fin.snoc xs x)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_iSup {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} {ι : Type} (φs : ι → L.BoundedFormulaInf α n) : (iSup φs).Realize v xs ↔ ∃ (i : ι), (φs i).Realize v xs

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_iInf {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} {ι : Type} (φs : ι → L.BoundedFormulaInf α n) : (iInf φs).Realize v xs ↔ ∀ (i : ι), (φs i).Realize v xs

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_top {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} : ⊤.Realize v xs ↔ True

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_not {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ : L.BoundedFormulaInf α n) : φ.not.Realize v xs ↔ ¬φ.Realize v xs

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_and {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ ψ : L.BoundedFormulaInf α n) : (φ.and ψ).Realize v xs ↔ φ.Realize v xs ∧ ψ.Realize v xs

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_inf {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ ψ : L.BoundedFormulaInf α n) : (φ ⊓ ψ).Realize v xs ↔ φ.Realize v xs ∧ ψ.Realize v xs

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_or {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ ψ : L.BoundedFormulaInf α n) : (φ.or ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_sup {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ ψ : L.BoundedFormulaInf α n) : (φ ⊔ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_ex {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ : L.BoundedFormulaInf α (n + 1)) : φ.ex.Realize v xs ↔ ∃ (x : M), φ.Realize v (Fin.snoc xs x)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_iff {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ ψ : L.BoundedFormulaInf α n) : (φ.iff ψ).Realize v xs ↔ (φ.Realize v xs ↔ ψ.Realize v xs)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_emptyiSup {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} : emptyiSup.Realize v xs ↔ False

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_emptyiInf {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} : emptyiInf.Realize v xs ↔ True

def FirstOrder.Language.FormulaInf.Realize {L : Language} {M : Type w} [L.Structure M] {α : Type u'} (φ : L.FormulaInf α) (v : α → M) : Prop

A formula can be evaluated by giving values to its free variables.

Equations

• φ.Realize v = FirstOrder.Language.BoundedFormulaInf.Realize φ v Fin.elim0

@[simp]

theorem FirstOrder.Language.FormulaInf.realize_not {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {φ : L.FormulaInf α} {v : α → M} : Realize (BoundedFormulaInf.not φ) v ↔ ¬φ.Realize v

@[simp]

theorem FirstOrder.Language.FormulaInf.realize_bot {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} : ⊥.Realize v ↔ False

@[simp]

theorem FirstOrder.Language.FormulaInf.realize_top {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} : ⊤.Realize v ↔ True

@[simp]

theorem FirstOrder.Language.FormulaInf.realize_imp {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} (φ ψ : L.FormulaInf α) : Realize (BoundedFormulaInf.imp φ ψ) v ↔ φ.Realize v → ψ.Realize v

@[simp]

theorem FirstOrder.Language.FormulaInf.realize_inf {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} (φ ψ : L.FormulaInf α) : (φ ⊓ ψ).Realize v ↔ φ.Realize v ∧ ψ.Realize v

@[simp]

theorem FirstOrder.Language.FormulaInf.realize_sup {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} (φ ψ : L.FormulaInf α) : (φ ⊔ ψ).Realize v ↔ φ.Realize v ∨ ψ.Realize v

@[simp]

theorem FirstOrder.Language.FormulaInf.realize_iSup {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} {ι : Type} (φs : ι → L.FormulaInf α) : Realize (BoundedFormulaInf.iSup φs) v ↔ ∃ (i : ι), (φs i).Realize v

@[simp]

theorem FirstOrder.Language.FormulaInf.realize_iInf {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} {ι : Type} (φs : ι → L.FormulaInf α) : Realize (BoundedFormulaInf.iInf φs) v ↔ ∀ (i : ι), (φs i).Realize v

def FirstOrder.Language.SentenceInf.Realize {L : Language} (φ : L.SentenceInf) (M : Type w) [L.Structure M] : Prop

A sentence can be evaluated in a structure.

Equations

• φ.Realize M = FirstOrder.Language.BoundedFormulaInf.Realize φ Empty.elim Fin.elim0

def FirstOrder.Language.SentenceInf.«term_⊨∞_» : Lean.TrailingParserDescr

Notation for a structure satisfying a sentence.

Equations

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