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