Let a, b, c : O(X) be open sets in your topology. The open sets become propositions in the logic. Let p:I⇒O(X) be an indexed set of open sets. These become predicates in the logic. The following define logical operators and relations in terms of topology.
- a⊨b ≝ a⊆b (entailment)
- ⊤ ≝ X (true)
- ⊥ ≝ ∅ (false)
- a∧b ≝ a∩b (and)
- a∨b ≝ a∪b (or)
- a⇒b ≝ ⋃{c:O(X)|c∩a⊆b} (implies)
- ∃x:I.p(x) ≝ ⋃{p(x)|x:I} (exists)
- ∀x:I.p(x) ≝ ⋃{c:O(X)|∀x:I.c⊆p(x)} (for all)
The definitions of entailment, true, false, and, and or are all straightforward. We want to create a definition of implies so that the deduction theorem, c∧a⊨b iff c⊨a⇒b, holds. This yields the above definition of implies. The definition of exists is the supremum of all p(x).
The definition of for all is the infimum of all p(x). The open sets form a lattice with supremums; however all lattices with supremums also have infimums. I have expanded the definition of infimum in the definition of for all so that it is entirely in terms of topological operations. It’s a bit unfortunate that for all is used in the definition of for all. ∀x:I.p(x) can also be though of as the interior of the intersection of all p(x).
Finally negation is defined in the usual way: ¬a ≝ a⇒⊥, and it can be thought of as the interior of the complement of a.
Notice that X⊨a∨¬a if and only if a is a clopen set. In general you will have a constructive logic. You get classical logic when you have a discrete topology.
My current understanding of a⇒b is that it is the set ¬a∨b plus the boundary shared by a and b. Thus while ¬a∨a is missing the boundary of a, a⇒a is ¬a∨a plus the boundary of a, and therefore a⇒a is all of X.
This whole definition is point-free, so it applies to point-free topology as well.