Upper bound for size of topology needed to falsify a non-tautology in IPC

I was attempting to answer this question with an algorithm based on an answer I gave as an exercise posed by Z.A.K here.

I think it is easy to show the decidability of IPC by converting to S4 and then appealing to the decidability of some tableau calculus for modal logic.

However, I feel like it should be possible to prove this by computing a conservative upper bound on the size of topology that one needs to check for a well-formed formula of a given size.

I am completely stuck on the inductive step when attempting to prove a bound on the size of finite topologies that I have to check.

My strategy was going to be, for an arbitrary formula $\varphi$, to pick a really dumb upper bound on the size of topologies I am going to look at, and then look at all the finite topologies over sets of that size or smaller.

Let $|\varphi|$ be the number of variables + the number of connectives in $\varphi$.

For safety, I will pick $2^{|\varphi|}$ as the size of the largest set to look at.

Consider all possible topologies on $[1..2^{|\varphi|}]$, with the whole space as the sole designated truth value in each topology $\tau$.

It's easy enough to prove that this bound works for well-formed formulas of the form $A$ and $\lnot A$ (as well as trivially $\top$ and $\bot$).

However, I'm having a really hard time figuring out how to induct on the structure of $\varphi$.

It isn't clear to me how much I have to grow the maximum size of my allowed topology to refute $\lnot \varphi$, given that $n$ refutes a formula of length $|\varphi|$.

Is there an easy bound and a straightfoward way to prove it?

Is the bound perhaps different for each connective? (On a rough impressionistic level, $\land$ seems to suggest maybe looking at a box topology or something.)

Solution 1:

Here's the punchline:

If $\varphi$ is an S4 formula that isn't provable, then there must be a (topological) model $X$ so that $X \not \models \varphi$ and $|X| \leq 2^n$, where $n$ is the number of subformulas of $\varphi$.

Imo, the "standard, straightforward" way to prove this actually goes through the kripke semantics for S4. We know that if an S4 formula isn't provable, then it's refutable in some world of some kripke model, say with worlds $W$ and relation $R$. We can then run a "filtration argument" to ensure the refuting model is finite:

Define an equivalence relation on $W$ so that $w_1 \sim w_2$ if and only if they agree on all subformulas of $\varphi$. That is, $w_1 \models \psi$ if and only if $w_2 \models \psi$. Call the set of equivalence classes $W^*$, and notice there are at most $2^n$ of them, where $n$ is the number of subformulas of $\varphi$ (since any world thinks that a given subformula is either true or false).

Next we put a relation on $W^*$, which isn't complicated, but is too long for me to want to write down here. This relation is chosen so that, for any subformula $\psi$ of $\varphi$,

$$(W, u) \models \psi \implies (W^*, [u]_\sim) \models \psi.$$

You can find a description of this relation in section fil.8 here.

So now what do we know? If $\varphi$ is refutable, then it's refutable in a kripke model of size at most $2^n$, where $n$ is the number of subformulas of $\varphi$ (since we can apply the above machinery to get the satisfiability of $\lnot \varphi$).

We then translate this result to the topological setting by using the topology of upper sets. In particular, if $(W,R)$ is some kripke model, then we define a topological model $(W,\tau)$ on the same underlying set. The open sets of this space are exactly the upwards-closed subsets of $W$, and it turns out that (under the usual topological semantics) $(W,\tau), u \models \varphi$ if and only if $(W,R), u \models \varphi$.

So then, viewing the refuting kripke model $W^*$ as a topological model in this way, if $\varphi$ is refutable, it must be refutable in a topological model of size at most $2^n$ -- as promised.

As a quick aside, notice this is actually doubly exponential to compute with. There are on the order of $2^{2^n}$ possible kripke relations on a model with $2^n$ worlds.

I hope this helps ^_^