def LO.IntProp.Formula.hVal {α : Type u} {ℍ : Type u_1} [HeytingAlgebra ℍ] (v : α → ℍ) : LO.IntProp.Formula α → ℍ

Equations

• LO.IntProp.Formula.hVal v (LO.IntProp.Formula.atom a) = v a
• LO.IntProp.Formula.hVal v LO.IntProp.Formula.verum = ⊤
• LO.IntProp.Formula.hVal v LO.IntProp.Formula.falsum = ⊥
• LO.IntProp.Formula.hVal v (φ.and ψ) = LO.IntProp.Formula.hVal v φ ⊓ LO.IntProp.Formula.hVal v ψ
• LO.IntProp.Formula.hVal v (φ.or ψ) = LO.IntProp.Formula.hVal v φ ⊔ LO.IntProp.Formula.hVal v ψ
• LO.IntProp.Formula.hVal v (φ.imp ψ) = LO.IntProp.Formula.hVal v φ ⇨ LO.IntProp.Formula.hVal v ψ
• LO.IntProp.Formula.hVal v φ.neg = (LO.IntProp.Formula.hVal v φ)ᶜ

@[simp]

theorem LO.IntProp.Formula.hVal_atom {α : Type u} {ℍ : Type u_1} [HeytingAlgebra ℍ] (v : α → ℍ) (a : α) : LO.IntProp.Formula.hVal v (LO.IntProp.Formula.atom a) = v a

@[simp]

theorem LO.IntProp.Formula.hVal_verum {α : Type u} {ℍ : Type u_1} [HeytingAlgebra ℍ] (v : α → ℍ) : LO.IntProp.Formula.hVal v ⊤ = ⊤

@[simp]

theorem LO.IntProp.Formula.hVal_falsum {α : Type u} {ℍ : Type u_1} [HeytingAlgebra ℍ] (v : α → ℍ) : LO.IntProp.Formula.hVal v ⊥ = ⊥

@[simp]

theorem LO.IntProp.Formula.hVal_and {α : Type u} {ℍ : Type u_1} [HeytingAlgebra ℍ] (v : α → ℍ) (φ ψ : LO.IntProp.Formula α) : LO.IntProp.Formula.hVal v (φ ⋏ ψ) = LO.IntProp.Formula.hVal v φ ⊓ LO.IntProp.Formula.hVal v ψ

@[simp]

theorem LO.IntProp.Formula.hVal_or {α : Type u} {ℍ : Type u_1} [HeytingAlgebra ℍ] (v : α → ℍ) (φ ψ : LO.IntProp.Formula α) : LO.IntProp.Formula.hVal v (φ ⋎ ψ) = LO.IntProp.Formula.hVal v φ ⊔ LO.IntProp.Formula.hVal v ψ

@[simp]

theorem LO.IntProp.Formula.hVal_imp {α : Type u} {ℍ : Type u_1} [HeytingAlgebra ℍ] (v : α → ℍ) (φ ψ : LO.IntProp.Formula α) : LO.IntProp.Formula.hVal v (φ ➝ ψ) = LO.IntProp.Formula.hVal v φ ⇨ LO.IntProp.Formula.hVal v ψ

@[simp]

theorem LO.IntProp.Formula.hVal_neg {α : Type u} {ℍ : Type u_1} [HeytingAlgebra ℍ] (v : α → ℍ) (φ : LO.IntProp.Formula α) : LO.IntProp.Formula.hVal v (∼φ) = (LO.IntProp.Formula.hVal v φ)ᶜ

structure LO.IntProp.HeytingSemantics (α : Type u_1) : Type (max u_1 (u_2 + 1))

• Algebra : Type u_2
• valAtom : α → self.Algebra
• heyting : HeytingAlgebra self.Algebra
• nontrivial : Nontrivial self.Algebra

instance LO.IntProp.HeytingSemantics.instCoeSortType {α : Type u} : CoeSort (LO.IntProp.HeytingSemantics α) (Type u_1)

Equations

• LO.IntProp.HeytingSemantics.instCoeSortType = { coe := LO.IntProp.HeytingSemantics.Algebra }

instance LO.IntProp.HeytingSemantics.instHeytingAlgebraAlgebra {α : Type u} (ℍ : LO.IntProp.HeytingSemantics α) : HeytingAlgebra ℍ.Algebra

Equations

• ℍ.instHeytingAlgebraAlgebra = ℍ.heyting

instance LO.IntProp.HeytingSemantics.instNontrivialAlgebra {α : Type u} (ℍ : LO.IntProp.HeytingSemantics α) : Nontrivial ℍ.Algebra

Equations

• ⋯ = ⋯

def LO.IntProp.HeytingSemantics.hVal {α : Type u} (ℍ : LO.IntProp.HeytingSemantics α) (φ : LO.IntProp.Formula α) : ℍ.Algebra

Equations

• ℍ.hVal φ = LO.IntProp.Formula.hVal ℍ.valAtom φ

def LO.IntProp.«term_⊧ₕ_» : Lean.TrailingParserDescr

Equations

• LO.IntProp.«term_⊧ₕ_» = Lean.ParserDescr.trailingNode `LO.IntProp.«term_⊧ₕ_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊧ₕ ") (Lean.ParserDescr.cat `term 46))

@[simp]

theorem LO.IntProp.HeytingSemantics.hVal_verum {α : Type u} (ℍ : LO.IntProp.HeytingSemantics α) : ℍ.hVal ⊤ = ⊤

@[simp]

theorem LO.IntProp.HeytingSemantics.hVal_falsum {α : Type u} (ℍ : LO.IntProp.HeytingSemantics α) : ℍ.hVal ⊥ = ⊥

@[simp]

theorem LO.IntProp.HeytingSemantics.hVal_and {α : Type u} (ℍ : LO.IntProp.HeytingSemantics α) (φ ψ : LO.IntProp.Formula α) : ℍ.hVal (φ ⋏ ψ) = ℍ.hVal φ ⊓ ℍ.hVal ψ

@[simp]

theorem LO.IntProp.HeytingSemantics.hVal_or {α : Type u} (ℍ : LO.IntProp.HeytingSemantics α) (φ ψ : LO.IntProp.Formula α) : ℍ.hVal (φ ⋎ ψ) = ℍ.hVal φ ⊔ ℍ.hVal ψ

@[simp]

theorem LO.IntProp.HeytingSemantics.hVal_imply {α : Type u} (ℍ : LO.IntProp.HeytingSemantics α) (φ ψ : LO.IntProp.Formula α) : ℍ.hVal (φ ➝ ψ) = ℍ.hVal φ ⇨ ℍ.hVal ψ

@[simp]

theorem LO.IntProp.HeytingSemantics.hVal_iff {α : Type u} (ℍ : LO.IntProp.HeytingSemantics α) (φ ψ : LO.IntProp.Formula α) : ℍ.hVal (φ ⭤ ψ) = bihimp (ℍ.hVal φ) (ℍ.hVal ψ)

@[simp]

theorem LO.IntProp.HeytingSemantics.hVal_not {α : Type u} (ℍ : LO.IntProp.HeytingSemantics α) (φ : LO.IntProp.Formula α) : ℍ.hVal (∼φ) = (ℍ.hVal φ)ᶜ

instance LO.IntProp.HeytingSemantics.instSemanticsFormula {α : Type u} : LO.Semantics (LO.IntProp.Formula α) (LO.IntProp.HeytingSemantics α)

Equations

• LO.IntProp.HeytingSemantics.instSemanticsFormula = { Realize := fun (ℍ : LO.IntProp.HeytingSemantics α) (φ : LO.IntProp.Formula α) => ℍ.hVal φ = ⊤ }

theorem LO.IntProp.HeytingSemantics.val_def {α : Type u} {ℍ : LO.IntProp.HeytingSemantics α} {φ : LO.IntProp.Formula α} : ℍ ⊧ φ ↔ LO.IntProp.Formula.hVal ℍ.valAtom φ = ⊤

theorem LO.IntProp.HeytingSemantics.val_def' {α : Type u} {ℍ : LO.IntProp.HeytingSemantics α} {φ : LO.IntProp.Formula α} : ℍ ⊧ φ ↔ ℍ.hVal φ = ⊤

instance LO.IntProp.HeytingSemantics.instTopFormula {α : Type u} : LO.Semantics.Top (LO.IntProp.HeytingSemantics α)

Equations

• ⋯ = ⋯

instance LO.IntProp.HeytingSemantics.instBotFormula {α : Type u} : LO.Semantics.Bot (LO.IntProp.HeytingSemantics α)

Equations

• ⋯ = ⋯

instance LO.IntProp.HeytingSemantics.instAndFormula {α : Type u} : LO.Semantics.And (LO.IntProp.HeytingSemantics α)

Equations

• ⋯ = ⋯

@[simp]

theorem LO.IntProp.HeytingSemantics.val_imply {α : Type u} (ℍ : LO.IntProp.HeytingSemantics α) {φ ψ : LO.IntProp.Formula α} : ℍ ⊧ φ ➝ ψ ↔ ℍ.hVal φ ≤ ℍ.hVal ψ

@[simp]

theorem LO.IntProp.HeytingSemantics.val_iff {α : Type u} (ℍ : LO.IntProp.HeytingSemantics α) {φ ψ : LO.IntProp.Formula α} : ℍ ⊧ φ ⭤ ψ ↔ ℍ.hVal φ = ℍ.hVal ψ

theorem LO.IntProp.HeytingSemantics.val_not {α : Type u} (ℍ : LO.IntProp.HeytingSemantics α) (φ : LO.IntProp.Formula α) : ℍ ⊧ ∼φ ↔ ℍ.hVal φ = ⊥

@[simp]

theorem LO.IntProp.HeytingSemantics.val_or {α : Type u} (ℍ : LO.IntProp.HeytingSemantics α) (φ ψ : LO.IntProp.Formula α) : ℍ ⊧ φ ⋎ ψ ↔ ℍ.hVal φ ⊔ ℍ.hVal ψ = ⊤

def LO.IntProp.HeytingSemantics.mod {α : Type u} (H : LO.IntProp.Hilbert α) : Set (LO.IntProp.HeytingSemantics α)

Equations

• LO.IntProp.HeytingSemantics.mod H = LO.Semantics.models (LO.IntProp.HeytingSemantics α) H.axioms

instance LO.IntProp.HeytingSemantics.instIntuitionisticHilbertFormulaOfIncludeEFQ {α : Type u} {H : LO.IntProp.Hilbert α} [H.IncludeEFQ] : LO.System.Intuitionistic H

Equations

• LO.IntProp.HeytingSemantics.instIntuitionisticHilbertFormulaOfIncludeEFQ = LO.System.Intuitionistic.mk

theorem LO.IntProp.HeytingSemantics.mod_models_iff {α : Type u} {H : LO.IntProp.Hilbert α} {φ : LO.IntProp.Formula α} : LO.IntProp.HeytingSemantics.mod H ⊧ φ ↔ ∀ (ℍ : LO.IntProp.HeytingSemantics α), ℍ ⊧* H.axioms → ℍ ⊧ φ

theorem LO.IntProp.HeytingSemantics.sound {α : Type u} {H : LO.IntProp.Hilbert α} {φ : LO.IntProp.Formula α} (d : H ⊢! φ) : LO.IntProp.HeytingSemantics.mod H ⊧ φ

instance LO.IntProp.HeytingSemantics.instSoundHilbertFormulaSetMod {α : Type u} {H : LO.IntProp.Hilbert α} : LO.Sound H (LO.IntProp.HeytingSemantics.mod H)

Equations

• ⋯ = ⋯

def LO.IntProp.HeytingSemantics.lindenbaum {α : Type u} (H : LO.IntProp.Hilbert α) [DecidableEq α] [H.IncludeEFQ] [LO.System.Consistent H] : LO.IntProp.HeytingSemantics α

Equations

• LO.IntProp.HeytingSemantics.lindenbaum H = LO.IntProp.HeytingSemantics.mk (LO.System.LindenbaumAlgebra H) fun (a : α) => ⟦LO.IntProp.Formula.atom a⟧

theorem LO.IntProp.HeytingSemantics.lindenbaum_val_eq {α : Type u} (H : LO.IntProp.Hilbert α) [DecidableEq α] [H.IncludeEFQ] [LO.System.Consistent H] {φ : LO.IntProp.Formula α} : (LO.IntProp.HeytingSemantics.lindenbaum H).hVal φ = ⟦φ⟧

theorem LO.IntProp.HeytingSemantics.lindenbaum_complete_iff {α : Type u} {H : LO.IntProp.Hilbert α} [DecidableEq α] [H.IncludeEFQ] [LO.System.Consistent H] [LO.System.Consistent H] {φ : LO.IntProp.Formula α} : LO.IntProp.HeytingSemantics.lindenbaum H ⊧ φ ↔ H ⊢! φ

instance LO.IntProp.HeytingSemantics.instSoundHilbertFormulaLindenbaum {α : Type u} {H : LO.IntProp.Hilbert α} [DecidableEq α] [H.IncludeEFQ] [LO.System.Consistent H] : LO.Sound H (LO.IntProp.HeytingSemantics.lindenbaum H)

Equations

• ⋯ = ⋯

instance LO.IntProp.HeytingSemantics.instCompleteHilbertFormulaLindenbaum {α : Type u} {H : LO.IntProp.Hilbert α} [DecidableEq α] [H.IncludeEFQ] [LO.System.Consistent H] : LO.Complete H (LO.IntProp.HeytingSemantics.lindenbaum H)

Equations

• ⋯ = ⋯

theorem LO.IntProp.HeytingSemantics.complete {α : Type u} {H : LO.IntProp.Hilbert α} [DecidableEq α] {φ : LO.IntProp.Formula α} [H.IncludeEFQ] (h : LO.IntProp.HeytingSemantics.mod H ⊧ φ) : H ⊢! φ

instance LO.IntProp.HeytingSemantics.instCompleteHilbertFormulaSetModOfDecidableEqOfIncludeEFQ {α : Type u} {H : LO.IntProp.Hilbert α} [DecidableEq α] [H.IncludeEFQ] : LO.Complete H (LO.IntProp.HeytingSemantics.mod H)

Equations

• ⋯ = ⋯