Substitution

@[reducible, inline]

abbrev LO.IntProp.Substitution (α : Type u_1) : Type u_1

Imported declaration from the Incompleteness formalization.

Equations

• LO.IntProp.Substitution α = (α → LO.IntProp.Formula α)

@[reducible, inline]

abbrev LO.IntProp.Substitution.id {α : Type u_1} : Substitution α

Imported declaration from the Incompleteness formalization.

Equations

• LO.IntProp.Substitution.id a = LO.IntProp.Formula.atom a

def LO.IntProp.Formula.subst {α : Type u_1} (s : Substitution α) : Formula α → Formula α

Imported declaration from the Incompleteness formalization.

Equations

• LO.IntProp.Formula.atom a⟦s⟧ = s a
• LO.IntProp.Formula.falsum⟦s⟧ = ⊥
• φ.and ψ⟦s⟧ = φ⟦s⟧ ⋏ ψ⟦s⟧
• φ.or ψ⟦s⟧ = φ⟦s⟧ ⋎ ψ⟦s⟧
• φ.imp ψ⟦s⟧ = φ⟦s⟧ ==> ψ⟦s⟧

def LO.IntProp.Formula.«term_⟦_⟧» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.IntProp.Formula.subst_atom {α : Type u_1} {s : Substitution α} {a : α} : atom a⟦s⟧ = s a

@[simp]

theorem LO.IntProp.Formula.subst_bot {α : Type u_1} {s : Substitution α} : ⊥⟦s⟧ = ⊥

@[simp]

theorem LO.IntProp.Formula.subst_top {α : Type u_1} {s : Substitution α} : ⊤⟦s⟧ = ⊤

@[simp]

theorem LO.IntProp.Formula.subst_imp {α : Type u_1} {φ ψ : Formula α} {s : Substitution α} : (φ ==> ψ)⟦s⟧ = φ⟦s⟧ ==> ψ⟦s⟧

@[simp]

theorem LO.IntProp.Formula.subst_neg {α : Type u_1} {φ : Formula α} {s : Substitution α} : (∼φ)⟦s⟧ = ∼φ⟦s⟧

@[simp]

theorem LO.IntProp.Formula.subst_and {α : Type u_1} {φ ψ : Formula α} {s : Substitution α} : (φ ⋏ ψ)⟦s⟧ = φ⟦s⟧ ⋏ ψ⟦s⟧

@[simp]

theorem LO.IntProp.Formula.subst_or {α : Type u_1} {φ ψ : Formula α} {s : Substitution α} : (φ ⋎ ψ)⟦s⟧ = φ⟦s⟧ ⋎ ψ⟦s⟧

@[simp]

theorem LO.IntProp.Formula.subst_iff {α : Type u_1} {φ ψ : Formula α} {s : Substitution α} : (φ <=> ψ)⟦s⟧ = φ⟦s⟧ <=> ψ⟦s⟧

@[simp]

theorem LO.IntProp.subst_id {α : Type u_1} {φ : Formula α} : φ⟦Substitution.id⟧ = φ

def LO.IntProp.Substitution.comp {α : Type u_1} (s₁ s₂ : Substitution α) : Substitution α

Imported declaration from the Incompleteness formalization.

Equations

• (s₁ ∘ s₂) a = s₁ a⟦s₂⟧

def LO.IntProp.«term_∘_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.IntProp.«term_∘_» = Lean.ParserDescr.trailingNode `LO.IntProp.«term_∘_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘ ") (Lean.ParserDescr.cat `term 80))

@[simp]

theorem LO.IntProp.subst_comp {α : Type u_1} {s₁ s₂ : Substitution α} {φ : Formula α} : φ⟦s₁ ∘ s₂⟧ = φ⟦s₁⟧⟦s₂⟧

class LO.IntProp.SubstitutionClosed {α : Type u_1} (S : Set (Formula α)) : Prop

Imported declaration from the Incompleteness formalization.

• closed (φ : Formula α) : φ ∈ S → ∀ (s : Substitution α), φ⟦s⟧ ∈ S