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.