Foundation.IntProp.Heyting.Semantics

source

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

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 φ)ᶜ

Instances For

source

@[simp]

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

hVal v (atom a) = v a

source

@[simp]

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

hVal v ⊤ = ⊤

source

@[simp]

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

hVal v ⊥ = ⊥

source

@[simp]

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

hVal v (φ ⋏ ψ) = hVal v φ ⊓ hVal v ψ

source

@[simp]

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

hVal v (φ ⋎ ψ) = hVal v φ ⊔ hVal v ψ

source

@[simp]

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

hVal v (φ ➝ ψ) = hVal v φ ⇨ hVal v ψ

source

@[simp]

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

hVal v (∼φ) = (hVal v φ)ᶜ

source

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

Instances For

source

instance LO.IntProp.HeytingSemantics.instCoeSortType {α : Type u} :

CoeSort (HeytingSemantics α) (Type u_1)

Equations

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

source

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

HeytingAlgebra ℍ.Algebra

Equations

ℍ.instHeytingAlgebraAlgebra = ℍ.heyting

source

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

Nontrivial ℍ.Algebra

source

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

ℍ.Algebra

Equations

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

Instances For

source

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))

Instances For

source

@[simp]

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

ℍ.hVal ⊤ = ⊤

source

@[simp]

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

ℍ.hVal ⊥ = ⊥

source

@[simp]

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

ℍ.hVal (φ ⋏ ψ) = ℍ.hVal φ ⊓ ℍ.hVal ψ

source

@[simp]

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

ℍ.hVal (φ ⋎ ψ) = ℍ.hVal φ ⊔ ℍ.hVal ψ

source

@[simp]

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

ℍ.hVal (φ ➝ ψ) = ℍ.hVal φ ⇨ ℍ.hVal ψ

source

@[simp]

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

ℍ.hVal (φ ⭤ ψ) = bihimp (ℍ.hVal φ) (ℍ.hVal ψ)

source

@[simp]

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

ℍ.hVal (∼φ) = (ℍ.hVal φ)ᶜ

source

instance LO.IntProp.HeytingSemantics.instSemanticsFormula {α : Type u} :

Semantics (Formula α) (HeytingSemantics α)

Equations

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

source

theorem LO.IntProp.HeytingSemantics.val_def {α : Type u} {ℍ : HeytingSemantics α} {φ : Formula α} :

ℍ ⊧ φ ↔ Formula.hVal ℍ.valAtom φ = ⊤

source

theorem LO.IntProp.HeytingSemantics.val_def' {α : Type u} {ℍ : HeytingSemantics α} {φ : Formula α} :

ℍ ⊧ φ ↔ ℍ.hVal φ = ⊤

source

instance LO.IntProp.HeytingSemantics.instTopFormula {α : Type u} :

Semantics.Top (HeytingSemantics α)

source

instance LO.IntProp.HeytingSemantics.instBotFormula {α : Type u} :

Semantics.Bot (HeytingSemantics α)

source

instance LO.IntProp.HeytingSemantics.instAndFormula {α : Type u} :

Semantics.And (HeytingSemantics α)

source

@[simp]

theorem LO.IntProp.HeytingSemantics.val_imply {α : Type u} (ℍ : HeytingSemantics α) {φ ψ : Formula α} :

ℍ ⊧ φ ➝ ψ ↔ ℍ.hVal φ ≤ ℍ.hVal ψ

source

@[simp]

theorem LO.IntProp.HeytingSemantics.val_iff {α : Type u} (ℍ : HeytingSemantics α) {φ ψ : Formula α} :

ℍ ⊧ φ ⭤ ψ ↔ ℍ.hVal φ = ℍ.hVal ψ

source

theorem LO.IntProp.HeytingSemantics.val_not {α : Type u} (ℍ : HeytingSemantics α) (φ : Formula α) :

ℍ ⊧ ∼φ ↔ ℍ.hVal φ = ⊥

source

@[simp]

theorem LO.IntProp.HeytingSemantics.val_or {α : Type u} (ℍ : HeytingSemantics α) (φ ψ : Formula α) :

ℍ ⊧ φ ⋎ ψ ↔ ℍ.hVal φ ⊔ ℍ.hVal ψ = ⊤

source

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

Set (HeytingSemantics α)

Equations

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

Instances For

source

theorem LO.IntProp.HeytingSemantics.mod_models_iff {α : Type u} {H : Hilbert α} {φ : Formula α} :

mod H ⊧ φ ↔ ∀ (ℍ : HeytingSemantics α), ℍ ⊧* H.axioms → ℍ ⊧ φ

source

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

mod H ⊧ φ

source

instance LO.IntProp.HeytingSemantics.instSoundHilbertFormulaSetMod {α : Type u} {H : Hilbert α} :

Sound H (mod H)

source

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

HeytingSemantics α

Equations

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

Instances For

source

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

(lindenbaum H).hVal φ = ⟦φ⟧

source

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

lindenbaum H ⊧ φ ↔ H ⊢! φ

source

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

Sound H (lindenbaum H)

source

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

Complete H (lindenbaum H)

source

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

H ⊢! φ

source

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

Complete H (mod H)