Wittingly using first-order compactness to prove König's Lemma

Question

I am trying to prove König's Lemma using the compactness theorem of first-order logic (I know how to prove it using propositional compacness). That is, let $S$ be a set of first-order sentences. Then $S$ is satisfiable if and only if each finite subset of $S$ is satisfiable.

In order to avoid confusion, allow me to state below all the relevant definitions involved in the statement of König's Lemma.

A tree consists of

1. A set $T$.
2. A function $\ell:T\rightarrow \mathbb{N}$.
3. A binary relation $\mathcal{P}$ on $T$.

The elements of $T$ are called the nodes of the tree. For $x\in T$, $\ell(x)$ is the level of $x$, and we denote by $T_{n}$ the $n^{th}$ level of $T$. The relation $x\mathcal{P}y$ is read as $x$ immediately precedes $y$ (or $y$ immediately succeeds $x$). We require that (1) there is exactly one node $x\in T$ such that $\ell(x)=1$, called the root of the tree; (2) each node other than the root has exactly one immediate predecessor; and (3) $\ell(y)=\ell(x)+1$ for all $x,y\in T$ such that $x\mathcal{P}y$.

A subtree of $T$ is a nonempty set $T'\subseteq T$ such that for all $y\in T'$ and $x\mathcal{P}y$, $x\in T'$. Note that $T'$ is itself a tree under the restriction of $\ell$ and $\mathcal{P}$ to $T'$. Moreover, the root of $T'$ is the same as the root of $T$.

An end node of $T$ is a node with no (immediate) successors. A branch in $T$ is a set $S\subseteq T$ such that (1) the root of $T$ belongs to $S$, (2) for each $x\in S$, either (i) $x$ is an end node of $T$ or (ii) there is exactly one $y\in S$ such that $x\mathcal{P}y$. A branch satisfying (1) and (2-i) is a finite branch, while a branch satisfying (1) and (2-ii) is an infinite branch.

Let $\preceq$ be the transitive closure of $\mathcal{P}$, i.e., the smallest reflexive and transitive relation on $T$ containing $\mathcal{P}$. For $x,y\in T$, we have $x\preceq y$ if and only if $x$ precedes $y$, i.e., $y$ succeeds $x$, i.e., there exists a finite sequence $x\mathcal{P}x_{1},x_{1}\mathcal{P}x_{2},\ldots,x_{n-1}\mathcal{P}y$. Note that the relation $\preceq$ is reflexive, transitive and antisymmetric. Thus $\preceq$ is a partial order on $T$.

A tree $T$ is finitely branchingf if each node of $T$ has only finitely many immediate successors in $T$.

König's Lemma: Let $T$ be an infinite, finitely branching tree. Then $T$ has an infinite branch.

In order to prove König's Lemma using the compactness theorem I define a language $L$ with $=$ to contain:

1. A constant $a^{u}$ for each node $u\in T$ such that $a^{u}\neq a^{v}$ for distinct nodes $u\neq v$ in $T$.
2. A unary predicate $P$ (where $Px$ intuitively means $x$ is in the infinite branch).
3. A binary predicate $R$ (where $Rxy$ intuitively means $x$ precedes $y$, i.e. $x\preceq y$)
4. A binary predicate $S$ (where $Sxy$ intuitively means $x$ and $y$ are in the same level of $T$).

Then I define a set $\mathcal{S}$ of $L$-sentences to contain:

1. $Ra^{u}a^{v}$ for each pair of nodes $u,v\in T$ such that $u\preceq v$.
2. $Sa^{u}a^{v}$ for each pair of nodes $u,v\in T$ such that $\ell(u)=\ell(v)$ (on the same level of $T$).
3. $\forall x\, Rxx$.
4. $\forall x\,\forall y\, (Rxy\wedge Ryx)\Rightarrow (x=y)$.
5. $\forall x\,\forall y\, \forall z\, (Rxy\wedge Ryz)\Rightarrow Rxz$.
6. $\forall x\,\forall y\, (Py\wedge Rxy)\Rightarrow Px$ (i.e. if $y$ is in the infinite brach and $x$ precedes $y$ then $x$ is also in the infinite branch).
7. $\forall x\,\forall y\, (Sxy\wedge\neg(x=y))\Rightarrow\neg(Px\wedge Py)$ (there is at most one node at each level of the infinite branch)
8. $\forall x\,\exists y\, (Sxy\wedge Py)$ (there is at least one node at each level of the infinite branch).

Question: Have I defined the language $L$ and the set $\mathcal{S}$ correctly? I am running into some trouble showing each finite subset of $\mathcal{S}$ is satisfiable in some $L$-structure, and I think it is because something is wrong here.

Thank you for reading this far :)

---

Edit: My goal is to show that $\mathcal{S}$ is satisfiable in some $L$-structure $M=\left(U_{M},R_{M},S_{M},P_{M},a^{u}_{M}:u\in T\right)$. That way, the axioms 1-5 of $\mathcal{S}$ imply that $M$ is a tree containing an isomorphic copy of $T$ as a subtree. That is, the subset $U^{'}_{M}=\{a^{u}_{M}:u\in T\}\subseteq U_{M}$, together with $R_{M}$ and $S_{M}$ restricted to $U^{'}_{M}$ is a subtree of $M$ isomorphic to $T$ in the sense that the map $T\rightarrow U^{'}_{M}$ given by $u\mapsto a^{u}_{M}$ is an order preserving bijection. Since $M$ also satisfies 6-8, it has an infinite path, and so must $T$ as well. Does this reasoning make sense?

Answer 1

No need to use full first-order logic here: compactness for propositional logic suffices.

Let $T$ be a finitely branching tree. Consider the language with one proposition symbol $P_v$ for each node $v\in T$. Consider the following theory $\Sigma_T$:

• $P_r$, where $r$ is the root.
• $P_w\rightarrow P_v$, whenever $v$ is the immediate predecessor of $w$.
• $P_v \rightarrow \bigvee_{i=1}^n (P_{w_i}\land \bigwedge_{j\neq i} \lnot P_{w_j})$, whenever $v$ is a node with immediate successors $\{w_1,\dots,w_n\}$. Note that if $v$ is an end node, then $n = 0$, so the axiom is $P_v\rightarrow \bot$, or equivalently, $\lnot P_v$.

Note that if $M$ is a model of $\Sigma_T$ (i.e. an assignment of truth values to the proposition symbols satisfying the axioms), then $\{v\in T\mid M\models P_v\}$ is an infinite path in $T$. Conversely, if $S$ is an infinite path in $T$, then defining $M\models P_v$ if and only if $v\in S$, $M$ is a model of $\Sigma_T$.

Now assume that $T$ is infinite. We would like to show that $\Sigma_T$ is consistent. By compactness, it suffices to show that every finite subset of $\Sigma_T$ is consistent. Let $\Delta$ be a finite subset of $\Sigma_T$, and let $k$ be the maximum level in the tree such that some axiom in $\Delta$ mentions a node at level $k$.

Since $T$ is finitely branching, it's easy to prove by induction that there are only finitely many nodes at each level in $T$. So there are only finitely many nodes at levels $\leq k$ in $T$. Since $T$ is infinite, there is some node $w$ at level $\ell$ in $T$, where $\ell>k$. Let $S = \{v\in T\mid v\preceq w\}$, and define a truth assignment by $M\models P_v$ if and only if $v\in S$. Then $M\models \Delta$, as desired.

---

To give you some feedback on the attempted proof in your question:

What is a model $M$ of your axioms 1-8? Well, axioms 3-5 ensure that $R$ is a partial order on $M$, and axiom 1 ensures that the order $(T,\preceq)$ admits a homomorphism to $(M,R)$. Note that $M$ may not be a tree, and you have not ensured that $M$ contains an isomorphic copy of $T$. To do the latter, you should include axioms $a_u\neq a_v$ when $u\neq v$ and $\lnot a_uRa_v$ when $u\not\preceq v$.

Now $S$ is a binary relation on $M$, which you want to think of as the "same level" equivalence relation. But all you've said about $S$ is that it is some arbitrary binary relation on $M$, which restricts to the real "same level" equivalence relation on the copy of $T$ (axiom 2). Let's add axioms asserting that $S$ is an equivalence relation, so that we can better make sense of axioms 6-8.

Axioms 6-8 say that $P$ is a downwards-closed subset of $(M,R)$, which contains exactly one element of each equivalence class for $S$.

Now the question is: Does a model of your axioms allow us to find an infinite path through $T$? The answer is no. For example, consider $T\sqcup \mathbb{N}$, where $T$ is our tree, $\mathbb{N}$ is a disjoint copy of the natural numbers, $R$ is interpreted as $\preceq$ on $T$ and the usual $\leq$ on $\mathbb{N}$, and the natural number $n$ is in the $S$-class of the nodes of $T$ at level $n$. Finally, let $P$ be interpreted as $\mathbb{N}$. This is a model of your axioms, but the "path" $\mathbb{N}$ tells us nothing about the tree $T$.

One way to fix this is to add axioms saying that the finitely many nodes at level $n$ in $T$ are the only elements at their level. For example, if $r$ is the root of $T$, we write down $\forall x\,( xSa_r\rightarrow x=a_r)$. And if $\{v_1,\dots,v_n\}$ are the immediate successors of the root, we write down $\forall x\, (xSa_{v_1}\rightarrow \bigvee_{i=1}^n x = a_{v_i})$. Now a model might still look very strange "above" and "below" $T$, but it is required to pick a real element of the isomorphic copy of $T$ from each level to put in the path.

How do you show this theory is finitely satisfiable? Write $T_n$ for the tree obtained from $T$ by throwing away all nodes above level $n$. By the argument in my answer above, each $T_n$ admits a path $P_n$ from the root to a node at level $n$.

Now given a finite subset $\Delta$ of our theory, let $n$ be the maximum level of a node whose constant appears in $\Delta$. The tree $T_n$, equipped with $P_n$, and with the rest of the unmentioned constants interpreted arbitrarily (say, interpret them all as the root), is a model of $\Delta$.