I guess today I’m learning about Heyting algebras too.
I don’t think that circle method works. “Not Not A” isn’t necessarily the same thing as “A” in a Heyting algebra, though your method suggests that they are the same. You can try to fix this by adding or removing the circle borders through negation operations, but even that yields inconsistent results. For example, if you add the border on each negation, “A or Not A” yields 1 under your method, though it should not in a Heyting algebra. If you remove the border on each negation “A is a subset of Not Not A” is false under your method, though it should yield true.
I think it’s easier to think of Heyting algebra in terms of functions and arguments. “A implies B” is a function that takes an argument of type A and produces an argument of type B. 0 is null. “A and B” is the set of arguments a,b where a is of type A and b is of type B. If null is in the argument list, then the whole argument list becomes null. “Not A” is a function that takes an argument of type A and produces 0. “Not Not A” can be thought of in two ways: (1) it takes an argument of type Not A and produces 0, or (2) it takes an argument of type [a function that takes an argument of type A and produces 0] and produces 0.
If “(A and B and C and …) → 0” then “A → (B → (C → … → 0))”. If you’ve worked with programming languages where lambda functions are common, it’s like taking a function of 2 arguments and turning it into a function of 1 argument by fixing one of the arguments.
I don’t see it on the Wikipedia page, but I’d guess that “A or B” means “(Not B implies A) and (Not A implies B)”.
If you don’t already, I highly recommend studying category theory. Most abstract mathematical concepts have simple definitions in category theory. The category theoretic definition of Heyting algebras on Wikipedia consists of 6 lines, and it’s enough to understand all of the above except the Or relation.
If you remove the border on each negation “A is a subset of Not Not A” is false under your method, though it should yield true.
How so? I thought removing the border on each negation was the right way. (Also you need to start out with no border, basically you should have open sets at each step.)
Lambda calculus is indeed a nice way to understand intuitionism, that’s how I imagined it since forever :-) Also the connection between Peirce’s law and call/cc is nice. And the way it prevents confluence is also really nice. This stackoverflow question has probably the best explanation.
How so? I thought removing the border on each negation was the right way.
I gave an example of where removing the border gives the wrong result. Are you asking why “A is a subset of Not Not A” is true in a Heyting algebra? I think the proof goes like this:
(1) (a and not(a)) = 0
(2) By #1, (a and not(a)) is a subset of 0
(3) For all c,x,b, ((c and x) is a subset of b) = (c is a subset of (x implies b))
(4) By #2 and #4, a is a subset of (not(a) implies 0)
(5) For all c, not(c) = (c implies 0)
(6) By #4 and #5, a is a subset of not(not(a))
Maybe your method is workable when you interpret a Heyting subset to be a topological superset? Then 1 is the initial (empty) set and 0 is the terminal set. That doesn’t work with intersections though. “A and Not A” must yield 0, but the intersection of two non-terminal sets cannot possibly yield a terminal set. The union can though, so I guess that means you’d have to represent And with a union. That still doesn’t work though because “Not A and Not Not A” must yield 0 in a Heyting algebra, but it’s missing the border of A in the topological method, so it again isn’t terminal.
I don’t see how the topological method is workable for this.
does yield a Heyting algebra. This means that the understanding (but not the explanation) of /u/cousin_it checks out: removing the border on each negation is the “right way”.
Notice that under this interpretation X is always a subset of ¬¬X.:
Int(X^c) is a subset of X^c; by definition of Int(-).
Int(X^c)^c is a superset of X^c^c = X; since taking complements reverses containment.
Int( Int(X^c)^c ) is a superset of Int(X) = X; since Int(-) preserves containment.
But Int( Int(X^c)^c ) is just ¬¬X. So X is always a subset of ¬¬X.
However, in many cases ¬¬X is not a subset of X. For example, take the Euclidean plane with the usual topology, and let X be the plane with one point removed. Then ¬X = Int( X^c ) = ∅ is empty, so ¬¬X is the whole plane. But the whole plane is obviously not a subset of the plane with one point removed.
I guess today I’m learning about Heyting algebras too.
I don’t think that circle method works. “Not Not A” isn’t necessarily the same thing as “A” in a Heyting algebra, though your method suggests that they are the same. You can try to fix this by adding or removing the circle borders through negation operations, but even that yields inconsistent results. For example, if you add the border on each negation, “A or Not A” yields 1 under your method, though it should not in a Heyting algebra. If you remove the border on each negation “A is a subset of Not Not A” is false under your method, though it should yield true.
I think it’s easier to think of Heyting algebra in terms of functions and arguments. “A implies B” is a function that takes an argument of type A and produces an argument of type B. 0 is null. “A and B” is the set of arguments a,b where a is of type A and b is of type B. If null is in the argument list, then the whole argument list becomes null. “Not A” is a function that takes an argument of type A and produces 0. “Not Not A” can be thought of in two ways: (1) it takes an argument of type Not A and produces 0, or (2) it takes an argument of type [a function that takes an argument of type A and produces 0] and produces 0.
If “(A and B and C and …) → 0” then “A → (B → (C → … → 0))”. If you’ve worked with programming languages where lambda functions are common, it’s like taking a function of 2 arguments and turning it into a function of 1 argument by fixing one of the arguments.
I don’t see it on the Wikipedia page, but I’d guess that “A or B” means “(Not B implies A) and (Not A implies B)”.
If you don’t already, I highly recommend studying category theory. Most abstract mathematical concepts have simple definitions in category theory. The category theoretic definition of Heyting algebras on Wikipedia consists of 6 lines, and it’s enough to understand all of the above except the Or relation.
Yeah, I mentioned the topology complications.
How so? I thought removing the border on each negation was the right way. (Also you need to start out with no border, basically you should have open sets at each step.)
Lambda calculus is indeed a nice way to understand intuitionism, that’s how I imagined it since forever :-) Also the connection between Peirce’s law and call/cc is nice. And the way it prevents confluence is also really nice. This stackoverflow question has probably the best explanation.
I gave an example of where removing the border gives the wrong result. Are you asking why “A is a subset of Not Not A” is true in a Heyting algebra? I think the proof goes like this:
(1) (a and not(a)) = 0
(2) By #1, (a and not(a)) is a subset of 0
(3) For all c,x,b, ((c and x) is a subset of b) = (c is a subset of (x implies b))
(4) By #2 and #4, a is a subset of (not(a) implies 0)
(5) For all c, not(c) = (c implies 0)
(6) By #4 and #5, a is a subset of not(not(a))
Maybe your method is workable when you interpret a Heyting subset to be a topological superset? Then 1 is the initial (empty) set and 0 is the terminal set. That doesn’t work with intersections though. “A and Not A” must yield 0, but the intersection of two non-terminal sets cannot possibly yield a terminal set. The union can though, so I guess that means you’d have to represent And with a union. That still doesn’t work though because “Not A and Not Not A” must yield 0 in a Heyting algebra, but it’s missing the border of A in the topological method, so it again isn’t terminal.
I don’t see how the topological method is workable for this.
In a topological space, defining
X ∨ Y as X ∪ Y
X ∧ Y as X ∩ Y
X → Y as Int( X^c ∪ Y )
¬X as Int( X^c )
does yield a Heyting algebra. This means that the understanding (but not the explanation) of /u/cousin_it checks out: removing the border on each negation is the “right way”.
Notice that under this interpretation X is always a subset of ¬¬X.:
Int(X^c) is a subset of X^c; by definition of Int(-).
Int(X^c)^c is a superset of X^c^c = X; since taking complements reverses containment.
Int( Int(X^c)^c ) is a superset of Int(X) = X; since Int(-) preserves containment.
But Int( Int(X^c)^c ) is just ¬¬X. So X is always a subset of ¬¬X.
However, in many cases ¬¬X is not a subset of X. For example, take the Euclidean plane with the usual topology, and let X be the plane with one point removed. Then ¬X = Int( X^c ) = ∅ is empty, so ¬¬X is the whole plane. But the whole plane is obviously not a subset of the plane with one point removed.
I see. Thanks for the explanation.