Talk:Heyting algebra

From Wikipedia, the free encyclopedia

WikiProject Mathematics
Mathematics Portal
This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.
Mathematics rating: Start Class Mid Priority  Field: Algebra
Please update this rating as the article progresses, or if the rating is inaccurate. Please also add comments to suggest improvements to the article.


Contents

[edit] 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)

[edit] 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)

[edit] 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)

[edit] 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)

[edit] Wrong claim about total orders

The statement

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)