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.
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.