Heyting algebra

Stream: maths

[Yaël Dillies]

Do the axioms of a Heyting algebra imply the existence of a bot? The definition I have over at branch#heyting_algebra doesn't seem to imply it...

[Yaël Dillies]

@Yakov Pechersky, this means I have to integrate order_top within heyting_algebra, but not order_bot. That's a funny situation but I think it's okay?

[Reid Barton]

Ah, for people who talk about Heyting algebras, "lattice" means something with all finite meets and joins, including the empty ones. So yes, a Heyting algebra has a bottom (and top) element by definition.

[David Wärn]

Do you know that compl_sup_eq_himp only holds in Boolean algebras, not in general Heyting algebras? One always has $(p \implies p) = \top$, but $(p \sqcup \neg p) = \top$ means that your Heyting algebra is Boolean. The definition of Heyting algebra should be "finite meets and joins and an implication operator satisfying le_himp_iff_inf_le" (from this you can deduce distributivity and define pseudocomplements as $\neg p \coloneqq (p \implies \bot)$).

[David Wärn]

By the way, Flypitch has a nice tactic framework for reasoning internally to Boolean algebras, which can easily be adapted to Heyting algebras. I wrote a version for Cartesian closed categories a while ago. At the bottom of the gist is an example proof of the double-negated law of excluded middle, $\neg \neg (p \vee \neg p)$:

example : Γ ⟶ ((X ⨿ (X ⟹ Y)) ⟹ Y) ⟹ Y :=
begin
  c_intro hn,
  refine hn (_ ≫ coprod.inr),
  c_intro hx,
  exact hn (hx ≫ coprod.inl),
end

Here c_intro is a custom tactic for introducing a function / Heyting implication, analogous to intro, and hn _ only makes sense because of a coercion from $p \le (q \implies r)$ to $(p \le q) \to (p \le r)$. There's also a custom tactic for eliminating from a coproduct / disjunction (using distributivity). What's nice about these tactics is that the user experience is the same as when reasoning about Props in tactic mode.

[Junyan Xu]

I've got a puzzle about Heyting algebras in another thread; if anyone is interested they can start reading from here.

There are also some intuitionistic implications in this gist that could get you more familiar with intuitionistic logic.

[Yaël Dillies]

Oh, me dumb. I knew that something was not quite right!