Using Geometry in Logic

17 Apr 2022

One thing that I talk a lot about is the (surprisingly tight) connection between geometry and logic. I feel like this is something that one usually gains an appreciation for by seeing lots of examples, and I found a particularly simple example today on mse.

For completeness, OP wanted to know how to formally derive

$B \leftrightarrow A \land B, A \leftrightarrow \neg B ⊢ A$

and when I first saw this, I thought it looked vaguely LEM-y, so my first question was whether it was true intuitionistically. If it isn’t true intuitionistically, I would also want to find an intuitionistic model which invalidates it in order to give a complete answer (since I like to justify my uses of LEM for problems like this).

But how, you might ask, does geometry come into the picture? Well, we know that a sequent is provable intuitionistically if and only if it’s valid on all topological spaces with the following semantics¹:

primitive propositions $A, B, C, \dots$ are open sets
$φ \land ψ$ is the intersection of $φ$ and $ψ$
$φ \lor ψ$ is the union of $φ$ and $ψ$
$\neg φ$ is the interior of the complement of $φ$
$φ$ is “true” exactly when it’s the whole space
$φ$ is “false” exactly when it’s the empty set

In fact, we can say more: it’s enough² to check when the primitive propositions are open subsets of $R$ . To summarize this situation, cool kids will say that the topological semantics of $R$ are complete for intuitionistic logic.

By this completeness theorem,

B \leftrightarrow A \land B, A \leftrightarrow \neg B ⊢ A

is provable intuitionistically if and only if³

for any two open subsets $A$ and $B$ of $R$
if $B = A \cap B$ and $A$ is the interior of $B^{c}$
then $A = R$

But now we see that we can start applying our geometric intuition to this problem! After all, we know what open subsets of $R$ look like, and (at least for me), it’s much faster to show that $A$ must be all of $R$ in the above example than to look for a formal derivation.

Of course, to really answer OP’s question, we should provide a derivation. It’s not enough to argue abstractly that one should exist⁴, and thankfully this is also not hard. Since we now know that the claim is true intuitionistically, we can switch over to a programming interpretation by curry-howard! Since I have a lot of experience with functional programming, this is also easier for me than working with the logic directly. The idea is that writing programs is the same thing as writing proofs, and there’s a totally algorithmic way to convert some code (which I’ll outline below) into the desired proof tree:

Say we have programs

$f_{1} : B \to A \times B$
$f_{2} : A \times B \to B$
$g_{1} : A \to B \to 0$
$g_{2} : (B \to 0) \to A$

You’ll recognize these as our assumptions (where I’ve unpacked the $\leftrightarrow$ s). We want to build a program of type $A$ .

By $g_{2}$ , if we can build a program of type $B \to 0$ , we’ll be done! But if we’re given a $b : B$ , then it’s almost immediate to build the desired term as follows

B \overset{f_{1}}{⟶} A \times B \overset{g_{1} \times {id}_{B}}{⟶} \neg B \times B ⟶ 0

As a quick exercise, you might try to write down the actual code of type $A$ in your favorite functional programming language, assuming the existence of these functions $f_{1}$ , $f_{2}$ , $g_{1}$ , and $g_{2}$ .

If you don’t have anything better to do (or if you’ve never done it before) you might then convert this program into the proof tree that OP asked for.

This all worked out quite smoothly, since it turned out that the claim was actually true intuitionistically. If we got a claim that isn’t intuitionistically valid, can we use geometry in order to find a model where it’s false?

The answer, of course, is “yes”!

As an easy example, let’s take double negation elimination

⊢ \neg \neg A \leftrightarrow A

under our topological interpretation, this says that “the interior of the complement of the interior of the complement of $A$ is $A$ ”. A moment’s thought shows that this is the same thing as “the interior of the closure of $A$ equals $A$ ”, and there are well known open sets which don’t have this property⁵.

As another quick exercise, find an open set $A$ which is not the interior of its closure!

Then the heyting algebra of open subsets of $R$ equipped with this open set $A$ provides a countermodel for double negation elimination.

Another quick one tonight! I know I talk a lot about how my interests lie in the intersection of geometry and logic, but I think it can be tricky to really understand what that means. When I answered this mse question, I realized it would make a good expository post to give the general flavor of my interests. The fact that these things are also related to functional programming and PL theory is not an accident, and I’m also interested in those fields for similar reasons!

Obviously the rabbit hole goes much deeper than this. First via locales, which are geometric objects that “classify” propositional theories, and later via toposes, which are geoemtric objects that classify predicate (and higher order) theories in an analogous way. For more details about this, see Vicker’s excellent paper Locales and Toposes and Spaces, available here, for instance.

Stay warm, and I’ll see you all soon ^_^

Here, for simplicity, I’m identifying a formula $φ$ with its interpretation. If you want to be less sloppy than me, you should write $[[φ]]$ , but this is too annoying for me to type in mathjax – there aren’t enough hours in the day to write

[ \! [ \varphi ] \! ]

the number of times that would be required of me. ↩
It’s also enough to check $R^{n}$ for any fixed $n$ (I often have $R^{2}$ in mind), or $2^{ω}$ cantor space, or many other concrete spaces. ↩
Again we may take, for example, $R^{2}$ , $2^{ω}$ , etc. instead of $R$ if we prefer. ↩
I read a great (albeit somewhat aggressive) blog post a while ago which gave an analogy that now lives in my head rent free. If there are any readers confused by the (admittedly subtle!) distinction between giving a derivation and checking semantically that a sequent must be valid, hopefully this analogy helps!

When asked to derive a sequent $Γ ⊢ φ$ , it’s not enough to just check that it’s valid semantically.

This would be like being asked to compute the inverse of a matrix, and instead checking that the determinant is nonzero. Yes, this is equivalent to the existence of an inverse, but finding the inverse itself carries more information!

↩
Indeed, those open sets which satisfy this property are called regular. ↩