Is There a First-Order Logic Formula for Describing a Finite, Full Tree with Leaves at Even Levels?

Question

This question is about first-order logic.

Let the dictionary $ \Sigma $ consist of a single two-place relation symbol $\text{Child} $ i.e. $\Sigma=\{\text{Child} (\cdot,\cdot )\} $. A structure $ \mathcal{M} $ over $\Sigma$ is called a "tree" if its interpretation as a graph is a tree. Furthermore, a tree is "full" if every non-leaf node has exactly 2 children (sons). Lastly, the "level" of a node in the tree is defined as its distance from the root.

My question is: Does there exist a first-order logic formula $\phi $ such that for every structure $ \mathcal{M}, \phi $ holds in $ \mathcal{M}$ if and only if $ \mathcal{M} $ is a finite, full tree where all leaves are at even levels?

My intuition says there is no such a formal, since "properties of properties" is a bit out of the scope of FOL. As I know, proving "there is no such a formal $\phi$ such that.." start by by assuming that exist $\phi$, then construct some unsatisfiable formula's set $\Gamma$ where $\phi \in \Gamma$, and then following Compactness proof that any$\Delta\subset\Gamma$ is satisfiable. and I'm struggling to come up with such a $\Gamma$

Answer 1

Let's assume that such a $ \phi $ exists that characterizes finite, full trees where all leaves are at even levels. We will construct a set $ \Gamma $ such that $ \phi \in \Gamma $ and show that $ \Gamma $ is not satisfiable, thereby reaching a contradiction.

Let $ \Gamma = \{ \phi \} \cup \{ \psi_{2n} : n \in \mathbb{N} \} $, where $ \psi_n $ asserts that there exists a node at the $n$-th level.

Formally, $ \psi_n $ could be something like:

$$ \psi_n = \exists x_1 \exists x_2 \ldots \exists x_{n} \left( \bigwedge_{i=1}^{n-1} \text{Child}(x_i, x_{i+1}) \land \underbrace{\forall y(\lnot \text{Child}(y, x_{1}))}_{\text{root}} \right)$$

Claim 1: Every finite subset $ \Delta \subseteq \Gamma $ is satisfiable.

Proof: Any finite subset $ \Delta $ will contain $ \phi $ and finitely many $ \psi_{2k} $ for some finitely . We can always construct a finite, where all leaves are at even levels that satisfies $ \phi $ and all the $ \psi_n $ in $ \Delta $, thus by compactness we have that $\Gamma$ is satisfiable.

Claim 2: $ \Gamma $ itself is not satisfiable.

Proof: Assume that $ \Gamma $ is satisfiable. Then there exists a structure $ \mathcal{M} $ that satisfies $ \phi $ and all $ \psi_{2n}$. This would mean $ \mathcal{M} $ is a finite, full tree with some rank $2k$, but $ \psi_{2k+2}$ is also true in $ \mathcal{M} $, which is a contradiction.

Answer 2

So, first of all, if all models of a sentence $\phi$ are finite, then there is a uniform bound on the size of models of $\phi$ (by compactness). This rules out the possibility of such a sentence existing.

Beyond that though, even if you ask a weaker question, specifically whether there is a sentence $\phi$ such that finite models of $\phi$ are precisely the full trees where all leaves are at even levels, then the answer is still no.

You can formalize being a tree and fullness as first-order properties, but the difficulty is with evenness. Let $F$ be the collection of 'fully' full binary trees of finite height (i.e., full trees in which all leaves are at the same level). One can show using an Ehrenfeucht–Fraïssé game that for any sentence $\phi$, $\phi$ is satisfied by either only finitely many members of $F$ or all but finitely many members of $F$. In particular, no sentence picks out precisely the elements of $F$ with even height.