Talk:Heyting algebra

Definition needs clarification

The statement "A Heyting algebra H is a bounded lattice such that for all a and b in H there is a greatest element x of H such that

   a ∧ x ≤ b . {\displaystyle a\wedge x\leq b.} a \wedge x \le b."

suggests that the element x does not depend on the choice of a and b. But subsequent discussion suggests that x does indeed depend on the choice of a and b. Please remove this ambiguity. 73.32.71.188 (talk) 11:25, 16 June 2021 (UTC)

Symbol for the relative pseudo-complement

I propose to replace $\Rightarrow$ by $\rightarrow$ in the article. Having the relative pseudo-complement use the same symbol as logical implication is problematic. It complicates proofs, runs contrary to common usage (including in other wikipedia articles), and runs the risk to blurry the important distinction between material implication and logical implication in the minds of readers. I'll do the change if no one opposes it. Ceroklis 17:48, 27 September 2007 (UTC)

Done. Ceroklis 15:23, 29 September 2007 (UTC)

x

This definition looks identical to that of the concepf of Boolean algebra: a Boolean algebra is a complemented distributive lattice, provided one includes boundedness in the definition of lattice. What is the difference, if any, supposed to be? Michael Hardy 03:27, 9 Nov 2003 (UTC)

Unclear, certainly. Heyting algebras are not in general Boolean algebras. The point is that negation is defined as not x = 'x implies bottom', and this doesn't in general satisfy not not x = x. I think relatively complemented mis-states the definition, which is presumably meant to be that x implies y always exists , as a supremum.

Charles Matthews 08:31, 9 Nov 2003 (UTC)

Algebraic definition

I would like to propose the following alternative definition:

A Heyting algebra $(H,\wedge ,\vee ,\rightarrow ,0,1)$ is a tuple consisting of a non-empty set $H$, three binary operations $\wedge$, $\vee$ and $\rightarrow$ on this set (called meet, join, and implication, respectively), and two special elements 0 and 1 of this set, such that with the following properties hold:

1. $(H,\wedge ,\vee )$ is a distributive lattice.
2. $x\wedge 0=0$ and $x\vee 1=1$
3. $x\rightarrow x=1$
4. $(x\rightarrow y)\wedge y=y$ and $x\wedge (x\rightarrow y)=x\rightarrow y$
5. $x\rightarrow (y\wedge z)=(x\rightarrow y)\wedge (x\rightarrow z)$ and $(x\vee y)\rightarrow z=(x\rightarrow y)\wedge (x\rightarrow z)$

Heyting algebras were first introduced under the name Brouwer algebras by Garrett Birkhoff who used them to study implication in L. E. J. Brouwer's intuitionistic logic.

This more algebraic definition is probably not as succinct as the definition using the relative pseudo-complement that is currently used in the article but should make the connection to intuitionistic logic more obvious. What do the other wikipedians think? —Tobias Bergemann 08:29, 22 March 2006 (UTC)

User: Phys did a great job on this from the get-go. I think the article as it stands is a cut above every Wikipedia article on Boolean algebra. It covers all the important basics in a fine order (though the point about Heyting algebras being definable equationally might be stated more explicitly, and the example of complete distributive lattices should be included, along with the remark that the Lindenbaum algebra is not a complete distributive lattice). Your axiomatization btw is unsound in two places: both 4(b) and 5(b) are refuted by x=y=0 and (in the case of 5(b)) z=1. 5(b) is presumably just a typo, but what was 4(b) supposed to be? And why are your equations an improvement over those in the article? --Vaughan Pratt 06:39, 10 July 2007 (UTC)

I don't remember where from I took the definition above, probably from http://www.mathe.tu-freiberg.de/~hebisch/cafe/algebra/heytingalg.html. I guess what I meant at the time was that like most topics in lattice theory Heyting algebras too can be defined both as posets and as algebraic structures, and that the article could/should present both definitions, as it is/was done for example with boolean algebra and lattice. I guess when I wrote the above I thought the algebraic definition would make clearer the link to intuitionistic logic. — Tobias Bergemann 07:16, 10 July 2007 (UTC)

Addendum: 4(b) was meant to read $x\wedge (x\rightarrow y)=x\wedge y$, 5(b) was meant to read $(x\vee y)\rightarrow z=(x\rightarrow z)\wedge (y\rightarrow z)$— Tobias Bergemann 10:09, 10 July 2007 (UTC)

Peirce's Law

The article states: No simple proof is known that Peirce's law cannot be deduced from the basic laws of intuitionistic logic.. However, dialogic logic provides an easy way of acheiving that:

     O                      P
                            ((A -> B) -> A) -> A
   ? (A -> B) -> A          A
   ?                      ? A -> B
   ? A                      B
   ?

The proponent cannot defend against the attacks on basic statements like A and B. I reckon similarly easy proofs can be given in tablaux solvers, too. '-129.247.247.238 11:12, 11 May 2006 (UTC)'

Yes. For that matter, the same section also constructs a small Heyting algebra invalidating Peirce's law. I guess it depends what you call "simple" -Dan 21:23, 22 May 2006 (UTC)

Wrong claim about total orders

The statement

• Every totally ordered set that is a bounded lattice is also a Heyting algebra, where $\lnot 0=1$ and ...

is not true: consider the trivial total order consisting of one point. --Tillmo 11:43, 6 October 2007 (UTC)

No, it's true. For the one-point case it's trivially true. --Zundark 12:01, 6 October 2007 (UTC)

For the one-point case, $\lnot 0=1$ is not true. --Tillmo (talk) 22:46, 20 August 2008 (UTC)

Oh sorry, it is true, I confused $(\lnot 0)=1$ with $\lnot (0=1)$. --Tillmo (talk) 07:57, 21 August 2008 (UTC)

Organization

I find the organization of this article confusing. The relationship with intuitionistic logic is spread out throughout the article in such a way that to my relatively uninformed eye the article sounds like its repeating itself. It would be nice if the relationship with intuitionistic logic was together in one section. -- Walt Pohl (talk) 23:39, 22 December 2009 (UTC)

Well, roll up your sleeves and get stuck in dear boy. You can't break anything, and all changes are revertible! ~~ Dr Dec (Talk) ~~ 01:27, 23 December 2009 (UTC)

Horribly meta...

...why is this under "Mathematics articles with no comments"? And, (portraying my wiki-ignorance)... how? The discussion doesn't seem to have category markers in it. Abb3w (talk) 04:49, 12 March 2011 (UTC)

The maths rating template at the top of the page puts it in Category:Mathematics articles with no comments, because it detects that there's no Talk:Heyting algebra/Comments page. I don't see how it's useful, but that's how it works. Compare with Talk:Group (mathematics), which does have a comment. --Zundark (talk) 08:57, 12 March 2011 (UTC)

Looks like all (?) comments pages have gone (as of this month?), with their comments merged into the corresponding talk page (much better), though I was unable to find any relevant discussion bearing on this. Vaughan Pratt (talk) 15:28, 15 May 2016 (UTC)

Yes, all comment subpages should be gone now. The discussion is at Wikipedia talk:Discontinuation of comments subpages. --Zundark (talk) 15:46, 15 May 2016 (UTC)

The implication $1\to 2$

The page currently says "The implication $1\to 2$ is extremely useful and is the principal practical method for proving identities in Heyting algebras.

But it also says:

"We write 1 and 0 for the largest and the smallest element of $H$, respectively."

How can it be useful, in a proof, to consider values which are explicitly not defined in the system?

96.255.156.195 (talk) 02:25, 18 June 2012 (UTC)

The implication “$1\to 2$” referred to by your first quoted sentence says that if a formula F is an intuitionistic tautology, then the identity $F=1$ holds in all Heyting algebras. I fail to see the connection to the definition of 1 and 0, nor do I see here any “values which are explicitly not defined in the system”. Could you please clarify your question?—Emil J. 10:07, 19 June 2012 (UTC)

It would probably help a lot to replace “$1\to 2$” by “1 $\to$ 2”, since this makes clearer that 1 and 2 refer to the numbered statements and not to elements of the Heyting algebra. --Tillmo (talk) 11:52, 19 June 2012 (UTC)

This reading did not occur to me, but now that you mention it, it might indeed be the root of the IP’s problem. In that case I would suggest 1 ⇒ 2.—Emil J. 17:24, 19 June 2012 (UTC)

I extended this to the three other instances, and also changed "implication" to "metaimplication." However perhaps "entailment" with symbol ⊢ might be more standard here? --Vaughan Pratt (talk) 15:52, 9 July 2012 (UTC)

One-sided distributivity

Very nice. I was thinking about how to fix the problem you pointed out but you beat me to it. My fault for giving an unnecessarily strong condition in the first place. Vaughan Pratt (talk) 07:32, 24 January 2014 (UTC)

Assessment comment

The comment(s) below were originally left at Talk:Heyting algebra/Comments, and are posted here for posterity. Following several discussions in past years, these subpages are now deprecated. The comments may be irrelevant or outdated; if so, please feel free to remove this section.

I don't see how the article would benefit from a comments page, maybe someone can comment on this. --Vaughan Pratt (talk) 23:59, 31 March 2011 (UTC)

Last edited at 23:59, 31 March 2011 (UTC). Substituted at 02:10, 5 May 2016 (UTC)

dual heyting algebras

There is no section on dual heyting algebras, which lead to the dual of intuitionistic logic, which is paraconsistent. That is, the logic of open sets is formally dual to the logic of closed sets, where a point on the boundary of a set can be seen to be both in the set and in its complement (a = ¬a). An expert should add a section on dual heyting algebra and its relation to Interior Algebra and Paraconsistent Logic — Preceding unsigned comment added by 156.40.187.164 (talk) 15:53, 15 March 2018 (UTC)

Intuitionist vs. intuitionistic

The article alternates between "intuitionistic logic" and "intuitionist logic". I believe the former is more correct. In my understanding, "intuitionistic" (like "democratic") is an adjective, and "intuitionist" (like "democrat") is a noun. As in: Brouwer was an intuitionist, and championed the use of intuitionistic logic. — Preceding unsigned comment added by 156.57.124.2 (talk) 14:53, 1 March 2021 (UTC)