Talk:Heyting algebra

From Wikipedia, the free encyclopedia

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:

$(H, \wedge, \vee)$ is a distributive lattice.
$x \wedge 0 = 0$ and $x \vee 1 = 1$
$x \rightarrow x = 1$
$(x \rightarrow y) \wedge y = y$ and $x \wedge (x \rightarrow y) = x \rightarrow y$
$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)

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

Retrieved from "http://en.wikipedia.org../../../h/e/y/Talk%7EHeyting_algebra_dc22.html"

Talk:Heyting algebra

From Wikipedia, the free encyclopedia

[edit] Algebraic definition

[edit] Peirce's Law

Views

Navigation

Search