Documentation

Foundation.IntProp.Heyting.Semantics

@[simp]
theorem LO.IntProp.Formula.hVal_atom {α : Type u} {ℍ : Type u_1} [HeytingAlgebra ] (v : α) (a : α) :
hVal v (atom a) = v a
@[simp]
theorem LO.IntProp.Formula.hVal_verum {α : Type u} {ℍ : Type u_1} [HeytingAlgebra ] (v : α) :
@[simp]
theorem LO.IntProp.Formula.hVal_falsum {α : Type u} {ℍ : Type u_1} [HeytingAlgebra ] (v : α) :
@[simp]
theorem LO.IntProp.Formula.hVal_and {α : Type u} {ℍ : Type u_1} [HeytingAlgebra ] (v : α) (φ ψ : Formula α) :
hVal v (φ ψ) = hVal v φ hVal v ψ
@[simp]
theorem LO.IntProp.Formula.hVal_or {α : Type u} {ℍ : Type u_1} [HeytingAlgebra ] (v : α) (φ ψ : Formula α) :
hVal v (φ ψ) = hVal v φ hVal v ψ
@[simp]
theorem LO.IntProp.Formula.hVal_imp {α : Type u} {ℍ : Type u_1} [HeytingAlgebra ] (v : α) (φ ψ : Formula α) :
hVal v (φ ψ) = hVal v φ hVal v ψ
@[simp]
theorem LO.IntProp.Formula.hVal_neg {α : Type u} {ℍ : Type u_1} [HeytingAlgebra ] (v : α) (φ : Formula α) :
hVal v (φ) = (hVal v φ)
Equations
  • .instHeytingAlgebraAlgebra = .heyting
def LO.IntProp.HeytingSemantics.hVal {α : Type u} (ℍ : HeytingSemantics α) (φ : Formula α) :
.Algebra
Equations
@[simp]
@[simp]
@[simp]
theorem LO.IntProp.HeytingSemantics.hVal_and {α : Type u} (ℍ : HeytingSemantics α) (φ ψ : Formula α) :
.hVal (φ ψ) = .hVal φ .hVal ψ
@[simp]
theorem LO.IntProp.HeytingSemantics.hVal_or {α : Type u} (ℍ : HeytingSemantics α) (φ ψ : Formula α) :
.hVal (φ ψ) = .hVal φ .hVal ψ
@[simp]
theorem LO.IntProp.HeytingSemantics.hVal_imply {α : Type u} (ℍ : HeytingSemantics α) (φ ψ : Formula α) :
.hVal (φ ψ) = .hVal φ .hVal ψ
@[simp]
theorem LO.IntProp.HeytingSemantics.hVal_iff {α : Type u} (ℍ : HeytingSemantics α) (φ ψ : Formula α) :
.hVal (φ ψ) = bihimp (.hVal φ) (.hVal ψ)
@[simp]
theorem LO.IntProp.HeytingSemantics.hVal_not {α : Type u} (ℍ : HeytingSemantics α) (φ : Formula α) :
.hVal (φ) = (.hVal φ)
theorem LO.IntProp.HeytingSemantics.val_def {α : Type u} {ℍ : HeytingSemantics α} {φ : Formula α} :
φ Formula.hVal .valAtom φ =
theorem LO.IntProp.HeytingSemantics.val_def' {α : Type u} {ℍ : HeytingSemantics α} {φ : Formula α} :
φ .hVal φ =
@[simp]
theorem LO.IntProp.HeytingSemantics.val_imply {α : Type u} (ℍ : HeytingSemantics α) {φ ψ : Formula α} :
φ ψ .hVal φ .hVal ψ
@[simp]
theorem LO.IntProp.HeytingSemantics.val_iff {α : Type u} (ℍ : HeytingSemantics α) {φ ψ : Formula α} :
φ ψ .hVal φ = .hVal ψ
theorem LO.IntProp.HeytingSemantics.val_not {α : Type u} (ℍ : HeytingSemantics α) (φ : Formula α) :
φ .hVal φ =
@[simp]
theorem LO.IntProp.HeytingSemantics.val_or {α : Type u} (ℍ : HeytingSemantics α) (φ ψ : Formula α) :
φ ψ .hVal φ .hVal ψ =
theorem LO.IntProp.HeytingSemantics.mod_models_iff {α : Type u} {H : Hilbert α} {φ : Formula α} :
mod H φ ∀ ( : HeytingSemantics α), ⊧* H.axioms φ
theorem LO.IntProp.HeytingSemantics.sound {α : Type u} {H : Hilbert α} {φ : Formula α} (d : H ⊢! φ) :
mod H φ
theorem LO.IntProp.HeytingSemantics.lindenbaum_val_eq {α : Type u} (H : Hilbert α) [DecidableEq α] [H.IncludeEFQ] [System.Consistent H] {φ : Formula α} :
(lindenbaum H).hVal φ = φ
theorem LO.IntProp.HeytingSemantics.complete {α : Type u} {H : Hilbert α} [DecidableEq α] {φ : Formula α} [H.IncludeEFQ] (h : mod H φ) :
H ⊢! φ