Heyting algebras #
This file defines Heyting, co-Heyting and bi-Heyting algebras.
An Heyting algebra is a bounded distributive lattice with an implication operation ⇨⇨
such that
a ≤ b ⇨ c ↔ a ⊓ b ≤ c≤ b ⇨ c ↔ a ⊓ b ≤ c⇨ c ↔ a ⊓ b ≤ c↔ a ⊓ b ≤ c⊓ b ≤ c≤ c
. It also comes with a pseudo-complement ᶜ
, such that aᶜ = a ⇨ ⊥⇨ ⊥⊥
.
Co-Heyting algebras are dual to Heyting algebras. They have a difference \
and a negation ¬¬
such that a \ b ≤ c ↔ a ≤ b ⊔ c≤ c ↔ a ≤ b ⊔ c↔ a ≤ b ⊔ c≤ b ⊔ c⊔ c
and ¬a = ⊤ \ a¬a = ⊤ \ a⊤ \ a
.
Bi-Heyting algebras are Heyting algebras that are also co-Heyting algebras.
From a logic standpoint, Heyting algebras precisely model intuitionistic logic, whereas boolean algebras model classical logic.
Heyting algebras are the order theoretic equivalent of cartesian-closed categories.
Main declarations #
GeneralizedHeytingAlgebra
: Heyting algebra without a top element (nor negation).GeneralizedCoheytingAlgebra
: Co-Heyting algebra without a bottom element (nor complement).HeytingAlgebra
: Heyting algebra.CoheytingAlgebra
: Co-Heyting algebra.BiheytingAlgebra
: bi-Heyting algebra.
Notation #
⇨⇨
: Heyting implication\
: Difference¬¬
: Heyting negationᶜ
: (Pseudo-)complement
References #
- [Francis Borceux, Handbook of Categorical Algebra III][borceux-vol3]
Tags #
Heyting, Brouwer, algebra, implication, negation, intuitionistic
Notation #
Heyting negation
¬¬
hnot : α → α
Syntax typeclass for Heyting negation ¬¬
.
The difference between HasCompl
and HNot
is that the former belongs to Heyting algebras,
while the latter belongs to co-Heyting algebras. They are both pseudo-complements, but compl
underestimates while HNot
overestimates. In boolean algebras, they are equal.
See hnot_eq_compl
.
Instances
Heyting implication
Equations
- «term_⇨_» = Lean.ParserDescr.trailingNode `term_⇨_ 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇨ ") (Lean.ParserDescr.cat `term 60))
Heyting negation
Equations
- «term¬_» = Lean.ParserDescr.node `term¬_ 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "¬") (Lean.ParserDescr.cat `term 72))
⊤⊤
is a greatest elementa ⇨⇨
is right adjoint toa ⊓⊓
A generalized Heyting algebra is a lattice with an additional binary operation ⇨⇨
called
Heyting implication such that a ⇨⇨
is right adjoint to a ⊓⊓
.
This generalizes HeytingAlgebra
by not requiring a bottom element.
Instances
⊥⊥
is a least element\ a
is right adjoint to⊔ a⊔ a
A generalized co-Heyting algebra is a lattice with an additional binary
difference operation \
such that \ a
is right adjoint to ⊔ a⊔ a
.
This generalizes CoheytingAlgebra
by not requiring a top element.
Instances
⊥⊥
is a least elementa ⇨⇨
is right adjoint toa ⊓⊓
A Heyting algebra is a bounded lattice with an additional binary operation ⇨⇨
called Heyting
implication such that a ⇨⇨
is right adjoint to a ⊓⊓
.
Instances
⊤⊤
is a greatest element⊤ \ a⊤ \ a
is¬a¬a
A co-Heyting algebra is a bounded lattice with an additional binary difference operation \
such that \ a
is right adjoint to ⊔ a⊔ a
.
Instances
\ a
is right adjoint to⊔ a⊔ a
⊤ \ a⊤ \ a
is¬a¬a
A bi-Heyting algebra is a Heyting algebra that is also a co-Heyting algebra.
Instances
Equations
- GeneralizedHeytingAlgebra.toOrderTop = let src := inst; OrderTop.mk (_ : ∀ (a : α), a ≤ ⊤)
Equations
- GeneralizedCoheytingAlgebra.toOrderBot = let src := inst; OrderBot.mk (_ : ∀ (a : α), ⊥ ≤ a)
Equations
- HeytingAlgebra.toBoundedOrder = BoundedOrder.mk
Equations
- CoheytingAlgebra.toBoundedOrder = let src := inst; BoundedOrder.mk
Construct a Heyting algebra from the lattice structure and Heyting implication alone.
Equations
- HeytingAlgebra.ofHImp himp le_himp_iff = let src := inst; let src_1 := inst; HeytingAlgebra.mk (_ : ∀ (a : α), ⊥ ≤ a) (_ : ∀ (a : α), a ⇨ ⊥ = a ⇨ ⊥)
Construct a Heyting algebra from the lattice structure and complement operator alone.
Equations
- HeytingAlgebra.ofCompl compl le_himp_iff = let src := inst; let src_1 := inst; HeytingAlgebra.mk (_ : ∀ (a : α), ⊥ ≤ a) (_ : ∀ (a : α), compl a ⊔ ⊥ = compl a)
Construct a co-Heyting algebra from the lattice structure and the difference alone.
Equations
- CoheytingAlgebra.ofSDiff sdiff sdiff_le_iff = let src := inst; let src_1 := inst; CoheytingAlgebra.mk (_ : ∀ (a : α), a ≤ ⊤) (_ : ∀ (a : α), ⊤ \ a = ⊤ \ a)
Construct a co-Heyting algebra from the difference and Heyting negation alone.
Equations
- CoheytingAlgebra.ofHNot hnot sdiff_le_iff = let src := inst; let src_1 := inst; CoheytingAlgebra.mk (_ : ∀ (a : α), a ≤ ⊤) (_ : ∀ (a : α), ⊤ ⊓ hnot a = hnot a)
The deduction theorem in the Heyting algebra model of intuitionistic logic: an implication holds iff the conclusion follows from the hypothesis.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Alias of sdiff_sup_self
.
Alias of sup_sdiff_self
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Alias of the reverse direction of le_compl_iff_disjoint_right
.
Alias of the reverse direction of le_compl_iff_disjoint_left
.
Alias of le_compl_comm
.
Alias of the forward direction of le_compl_comm
.
Equations
- instCoheytingAlgebraOrderDual = let src := OrderDual.lattice α; let src_1 := OrderDual.boundedOrder α; CoheytingAlgebra.mk (_ : ∀ (a : αᵒᵈ), a ≤ ⊤) (_ : ∀ (a : α), a ⇨ ⊥ = aᶜ)
Equations
- One or more equations did not get rendered due to their size.
Alias of the reverse direction of hnot_le_iff_codisjoint_right
.
Alias of the reverse direction of hnot_le_iff_codisjoint_left
.
Equations
- instHeytingAlgebraOrderDual = let src := OrderDual.lattice α; let src_1 := OrderDual.boundedOrder α; HeytingAlgebra.mk (_ : ∀ (a : αᵒᵈ), ⊥ ≤ a) (_ : ∀ (a : α), ⊤ \ a = ¬a)
Equations
- One or more equations did not get rendered due to their size.
Propositions form a Heyting algebra with implication as Heyting implication and negation as complement.
Equations
- Prop.heytingAlgebra = let src := Prop.distribLattice; let src_1 := Prop.boundedOrder; HeytingAlgebra.mk Prop.heytingAlgebra.proof_3 Prop.heytingAlgebra.proof_4
A bounded linear order is a bi-Heyting algebra by setting
a ⇨ b = ⊤⇨ b = ⊤⊤
ifa ≤ b≤ b
anda ⇨ b = b⇨ b = b
otherwise.a \ b = ⊥⊥
ifa ≤ b≤ b
anda \ b = a
otherwise.
Equations
- One or more equations did not get rendered due to their size.
Pullback a GeneralizedHeytingAlgebra
along an injection.
Equations
- One or more equations did not get rendered due to their size.
Pullback a GeneralizedCoheytingAlgebra
along an injection.
Equations
- One or more equations did not get rendered due to their size.
Pullback a HeytingAlgebra
along an injection.
Equations
- One or more equations did not get rendered due to their size.
Pullback a CoheytingAlgebra
along an injection.
Equations
- One or more equations did not get rendered due to their size.
Pullback a BiheytingAlgebra
along an injection.
Equations
- One or more equations did not get rendered due to their size.