# Alternate proof that infinite complete binary branching tree as a Kripke frame generates the S4-tautologies.

The $$\mathsf{S4}$$ tautologies are precisely the formulas of modal logic that hold in all transitive, reflexive Kripke frames.

I think I've found an example of a single Kripke frame, the infinite binary tree with the subpath accessibility relation given below, that's universal in the sense that all tautologies that hold for it (when we vary the valuation maps) hold for $$\mathsf{S4}$$ in general and vice versa.

However, my method of proving that it does indeed generate precisely the $$\mathsf{S4}$$ tautologies seems a bit circuitous. I'm wondering if there's a more direct way to prove it.

The proof might also just be wrong. I'm also interested in hearing if it's wrong and how.

By the canonical domains theorem given in Computability and Logic, first-order logic with only binary relation symbols and no $$=$$ symbol, any model of the aforementioned fragment of first-order logic can be converted into a model over $$\mathbb{N}$$.

In a Kripke model, we can convert the set of worlds to the domain of a first-order model. For every primitive proposition $$A$$, we can define $$A(x, y)$$ as true if and only if $$A$$ holds at world $$x$$. We can then define the accessibility relation $$R$$.

We can then convert our expanded model over $$\mathbb{N}$$ back into a Kripke frame with $$\mathbb{N}$$ as the set of possible worlds.

Let $$M$$ be a transitive, reflexive Kripke model over $$M$$ and let $$w$$ be a starting world.

$$M \models \alpha$$ if and only if $$M, w \models \alpha$$ for all worlds $$w$$.

Let $$\mathcal{F}$$ be the set of all transitive, symmetric Kripke models over $$\mathbb{N}$$ and let $$\mathcal{F}''$$ be the set of all transitive, symmetric Kripke models over $$\mathbb{N}$$ equipped with a distinguished world $$w$$ in $$\mathbb{N}$$.

It follows that $$\mathcal{F} \models \alpha$$ if and only if $$\mathcal{F}'' \models \alpha$$.

Given an arbitrary model equipped with a distinguished world $$w$$, I will describe a procedure for converting it into a binary tree without affecting the truth of any sentences.

First, I take my graph and convert it into a tree of arbitrary arity branching out from the origin, by duplicating worlds as necessary and renaming them $$u, u, u \cdots \mapsto u, u', u''' \cdots$$. Along any path, any time I would revisit a previously visited node, I instead duplicate the world and create a new artificially-unvisited node.

Suppose I have an infinitely branching node $$u$$ with children $$v_1, v_2, \cdots$$.

I can build a tree in the following way, by building a linked list of sorts which grows to the right. Since my accessibility relation is transitive and reflexive, adding additional redundant $$u$$ nodes is harmless.

     u
v1    u
v2    u
v3   ...


A finitely branching note can be paraphrased away using a modified version of the same trick, for example a node with degree five would paraphrased into the following.

   u
v1  u
v2  u
v3  u
v4 v5


For the sake of explicitness, $$nRm$$ holds if and only if the path of $$\mathbf{left}, \mathbf{right}$$ steps taken from the root to $$n$$ is a prefix of the path from the root to $$m$$.

Performing the process leaves me with particular worlds such as $$u$$ in the above examples appearing multiple times in the tree, but we can fix this up by minting fresh worlds $$u', u'', u''', u'''', u'''''$$ and so on and making the same primitive propositions true in those worlds as in the base world.

This completes the construction of a Kripke model with a distinguished world over a complete binary tree.

Completing the proof of the intended claim:

Suppose $$\alpha$$ is true in all Kripke frames. Then $$\alpha$$ is true in all Kripke models. Thus $$\alpha$$ is true in all Kripke models with distinguished worlds, including those over $$\mathbb{N}$$ with the requisite binary branching accessibility relation.

Suppose $$\alpha$$ is false in at least one Kripke frame. Then $$\alpha$$ is false in at least one Kripke model. Thus $$\alpha$$ is false in at least one Kripke model with a distinguished world $$w$$. We can apply the canonical domains theorem and produce a Kripke model with a distinguished world over $$M$$. We can then apply the construction above to unfold the accessibility relation into a tree, and then convert the tree into a binary tree. Call the new Kripke model with a distinguished world $$M''$$.

Thus, we have at least one witness of the desired shape, $$M''$$, to the falsity of $$\alpha$$.

This completes the proof of the theorem.