Zulip Chat Archive

Stream: maths

Topic: Heyting algebra


Yaël Dillies (Jan 30 2022 at 11:38):

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 (Jan 30 2022 at 11:40):

@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 (Jan 30 2022 at 11:42):

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 (Jan 30 2022 at 12:24):

Do you know that compl_sup_eq_himp only holds in Boolean algebras, not in general Heyting algebras? One always has (p    p)=(p \implies p) = \top, but (p¬p)=(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 ¬p(p    )\neg p \coloneqq (p \implies \bot)).

David Wärn (Jan 30 2022 at 13:48):

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, ¬¬(p¬p)\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(q    r)p \le (q \implies r) to (pq)(pr)(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 (Jan 30 2022 at 16:15):

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 (Jan 30 2022 at 18:07):

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


Last updated: Dec 20 2023 at 11:08 UTC