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 (p.and q) = LO.IntProp.Formula.hVal v p ⊓ LO.IntProp.Formula.hVal v q
• LO.IntProp.Formula.hVal v (p.or q) = LO.IntProp.Formula.hVal v p ⊔ LO.IntProp.Formula.hVal v q
• LO.IntProp.Formula.hVal v (p.imp q) = LO.IntProp.Formula.hVal v p ⇨ LO.IntProp.Formula.hVal v q
• LO.IntProp.Formula.hVal v p.neg = (LO.IntProp.Formula.hVal v p)ᶜ

@[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 : α → ℍ) (p : LO.IntProp.Formula α) (q : LO.IntProp.Formula α) : LO.IntProp.Formula.hVal v (p ⋏ q) = LO.IntProp.Formula.hVal v p ⊓ LO.IntProp.Formula.hVal v q

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem LO.IntProp.HeytingSemantics.nontrivial {α : Type u_1} (self : LO.IntProp.HeytingSemantics α) : 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 α) (p : LO.IntProp.Formula α) : ℍ.Algebra

Equations

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

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 α) (p : LO.IntProp.Formula α) (q : LO.IntProp.Formula α) : ℍ.hVal (p ⋏ q) = ℍ.hVal p ⊓ ℍ.hVal q

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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 α) (p : LO.IntProp.Formula α) => ℍ.hVal p = ⊤ }

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

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

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

Equations

• LO.IntProp.HeytingSemantics.instTopFormula = { realize_top := ⋯ }

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

Equations

• LO.IntProp.HeytingSemantics.instBotFormula = { realize_bot := ⋯ }

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

Equations

• LO.IntProp.HeytingSemantics.instAndFormula = { realize_and := ⋯ }

@[simp]

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

@[simp]

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

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

@[simp]

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

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

Equations

• LO.IntProp.HeytingSemantics.mod Λ = LO.Semantics.models (LO.IntProp.HeytingSemantics α) Ax(Λ)

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

Equations

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

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

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

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

Equations

• ⋯ = ⋯

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

Equations

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

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯