Heyting regular elements #
This file defines Heyting regular elements, elements of an Heyting algebra that are their own double complement, and proves that they form a boolean algebra.
From a logic standpoint, this means that we can perform classical logic within intuitionistic logic by simply double-negating all propositions. This is practical for synthetic computability theory.
Main declarations #
IsRegular
:a
is Heyting-regular ifaᶜᶜ = a
.Regular
: The subtype of Heyting-regular elements.Regular.BooleanAlgebra
: Heyting-regular elements form a boolean algebra.
References #
- [Francis Borceux, Handbook of Categorical Algebra III][borceux-vol3]
theorem
Heyting.IsRegular.eq
{α : Type u_1}
[inst : HasCompl α]
{a : α}
:
Heyting.IsRegular a → aᶜᶜ = a
instance
Heyting.IsRegular.decidablePred
{α : Type u_1}
[inst : HasCompl α]
[inst : DecidableEq α]
:
DecidablePred Heyting.IsRegular
Equations
- Heyting.IsRegular.decidablePred x = inst (xᶜᶜ) x
theorem
Heyting.IsRegular.inf
{α : Type u_1}
[inst : HeytingAlgebra α]
{a : α}
{b : α}
(ha : Heyting.IsRegular a)
(hb : Heyting.IsRegular b)
:
Heyting.IsRegular (a ⊓ b)
theorem
Heyting.IsRegular.himp
{α : Type u_1}
[inst : HeytingAlgebra α]
{a : α}
{b : α}
(ha : Heyting.IsRegular a)
(hb : Heyting.IsRegular b)
:
Heyting.IsRegular (a ⇨ b)
theorem
Heyting.IsRegular.disjoint_compl_left_iff
{α : Type u_1}
[inst : HeytingAlgebra α]
{a : α}
{b : α}
(ha : Heyting.IsRegular a)
:
theorem
Heyting.IsRegular.disjoint_compl_right_iff
{α : Type u_1}
[inst : HeytingAlgebra α]
{a : α}
{b : α}
(hb : Heyting.IsRegular b)
:
def
BooleanAlgebra.ofRegular
{α : Type u_1}
[inst : HeytingAlgebra α]
(h : ∀ (a : α), Heyting.IsRegular (a ⊔ aᶜ))
:
A Heyting algebra with regular excluded middle is a boolean algebra.
Equations
- One or more equations did not get rendered due to their size.
The boolean algebra of Heyting regular elements.
Equations
- Heyting.Regular α = { a // Heyting.IsRegular a }
The coercion Regular α → α→ α
Equations
- Heyting.Regular.val = Subtype.val
instance
Heyting.Regular.instCoeRegular
{α : Type u_1}
[inst : HeytingAlgebra α]
:
Coe (Heyting.Regular α) α
Equations
- Heyting.Regular.instCoeRegular = { coe := Heyting.Regular.val }
theorem
Heyting.Regular.coe_injective
{α : Type u_1}
[inst : HeytingAlgebra α]
:
Function.Injective Heyting.Regular.val
@[simp]
theorem
Heyting.Regular.coe_inj
{α : Type u_1}
[inst : HeytingAlgebra α]
{a : Heyting.Regular α}
{b : Heyting.Regular α}
:
Equations
- Heyting.Regular.top = { top := { val := ⊤, property := (_ : Heyting.IsRegular ⊤) } }
Equations
- Heyting.Regular.bot = { bot := { val := ⊥, property := (_ : Heyting.IsRegular ⊥) } }
Equations
- Heyting.Regular.inf = { inf := fun a b => { val := ↑a ⊓ ↑b, property := (_ : Heyting.IsRegular (↑a ⊓ ↑b)) } }
Equations
- Heyting.Regular.himp = { himp := fun a b => { val := ↑a ⇨ ↑b, property := (_ : Heyting.IsRegular (↑a ⇨ ↑b)) } }
Equations
- Heyting.Regular.hasCompl = { compl := fun a => { val := ↑aᶜ, property := (_ : Heyting.IsRegular (↑aᶜ)) } }
@[simp]
theorem
Heyting.Regular.coe_inf
{α : Type u_1}
[inst : HeytingAlgebra α]
(a : Heyting.Regular α)
(b : Heyting.Regular α)
:
@[simp]
theorem
Heyting.Regular.coe_himp
{α : Type u_1}
[inst : HeytingAlgebra α]
(a : Heyting.Regular α)
(b : Heyting.Regular α)
:
@[simp]
theorem
Heyting.Regular.coe_compl
{α : Type u_1}
[inst : HeytingAlgebra α]
(a : Heyting.Regular α)
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Heyting.Regular.coe_le_coe
{α : Type u_1}
[inst : HeytingAlgebra α]
{a : Heyting.Regular α}
{b : Heyting.Regular α}
:
@[simp]
theorem
Heyting.Regular.coe_lt_coe
{α : Type u_1}
[inst : HeytingAlgebra α]
{a : Heyting.Regular α}
{b : Heyting.Regular α}
:
Regularization of a
. The smallest regular element greater than a
.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[simp]
theorem
Heyting.Regular.toRegular_coe
{α : Type u_1}
[inst : HeytingAlgebra α]
(a : Heyting.Regular α)
:
↑Heyting.Regular.toRegular ↑a = a
def
Heyting.Regular.gi
{α : Type u_1}
[inst : HeytingAlgebra α]
:
GaloisInsertion (↑Heyting.Regular.toRegular) Heyting.Regular.val
The Galois insertion between Regular.toRegular
and coe
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Heyting.Regular.lattice = GaloisInsertion.liftLattice Heyting.Regular.gi
@[simp]
theorem
Heyting.Regular.coe_sup
{α : Type u_1}
[inst : HeytingAlgebra α]
(a : Heyting.Regular α)
(b : Heyting.Regular α)
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Heyting.Regular.coe_sdiff
{α : Type u_1}
[inst : HeytingAlgebra α]
(a : Heyting.Regular α)
(b : Heyting.Regular α)
:
A decidable proposition is intuitionistically Heyting-regular.