Lω₁ω Semantics

This file defines the semantics of Lω₁ω formulas.

Main Definitions

• FirstOrder.Language.BoundedFormulaω.Realize: Evaluation of a bounded formula in a structure.
• FirstOrder.Language.Formulaω.Realize: Evaluation of a formula with variable assignment.
• FirstOrder.Language.Sentenceω.Realize: Truth of a sentence in a structure.

Main Results

• Simp lemmas for all connectives and quantifiers.

def FirstOrder.Language.BoundedFormulaω.Realize {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} : L.BoundedFormulaω α 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.BoundedFormulaω.falsum.Realize x✝¹ x✝ = False
• (FirstOrder.Language.BoundedFormulaω.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.BoundedFormulaω.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.BoundedFormulaω.iSup φs).Realize x✝¹ x✝ = ∃ (i : ℕ), (φs i).Realize x✝¹ x✝
• (FirstOrder.Language.BoundedFormulaω.iInf φs).Realize x✝¹ x✝ = ∀ (i : ℕ), (φs i).Realize x✝¹ x✝

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.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.BoundedFormulaω.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.BoundedFormulaω.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.BoundedFormulaω.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.BoundedFormulaω.realize_imp {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ ψ : L.BoundedFormulaω α n) : (φ.imp ψ).Realize v xs ↔ φ.Realize v xs → ψ.Realize v xs

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.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.BoundedFormulaω.realize_not {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ : L.BoundedFormulaω α n) : φ.not.Realize v xs ↔ ¬φ.Realize v xs

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.realize_einf {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} {ι : Type u_1} [Encodable ι] (φs : ι → L.BoundedFormulaω α n) : (einf φs).Realize v xs ↔ ∀ (i : ι), (φs i).Realize v xs

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.realize_esup {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} {ι : Type u_1} [Encodable ι] (φs : ι → L.BoundedFormulaω α n) : (esup φs).Realize v xs ↔ ∃ (i : ι), (φs i).Realize v xs

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

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

Equations

• φ.Realize v = FirstOrder.Language.BoundedFormulaω.Realize φ v Fin.elim0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.Formulaω.realize_einf {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} {ι : Type u_1} [Encodable ι] (φs : ι → L.Formulaω α) : Realize (BoundedFormulaω.einf φs) v ↔ ∀ (i : ι), (φs i).Realize v

@[simp]

theorem FirstOrder.Language.Formulaω.realize_esup {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} {ι : Type u_1} [Encodable ι] (φs : ι → L.Formulaω α) : Realize (BoundedFormulaω.esup φs) v ↔ ∃ (i : ι), (φs i).Realize v

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

A sentence can be evaluated in a structure.

Equations

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

def FirstOrder.Language.Sentenceω.«term_⊨ω_» : Lean.TrailingParserDescr

Notation for a structure satisfying a sentence.

Equations

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