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