<p>As noted in the comments it takes some care to phrase this question in a nontrivial way. However, this can be done in at least a couple ways, one yielding a positive answer and the other yielding a negative answer.</p>
<hr />
<p>As clarified in your edit, you have in mind the following question: is there a non-first-order property <span class="math-container">$X$</span> of structures which is <em>existentially second-order</em> (= <span class="math-container">$\Sigma^1_1$</span> or <span class="math-container">$\mathsf{ESO}$</span>) characterizable? Here <span class="math-container">$\mathsf{ESO}$</span> is the logic which allows expressions of the form &quot;Some expansion of the universe satisfies <span class="math-container">$\varphi$</span>&quot; for <span class="math-container">$\varphi\in\mathsf{FOL}$</span>. Note that <span class="math-container">$\mathsf{ESO}$</span> is quite a nice logic in many respects - e.g. it is fully compact and has downward Lowenheim-Skolem - but it is not closed under negation (so we don't contradict <a href="https://en.wikipedia.org/wiki/Lindstr%C3%B6m%27s_theorem" rel="nofollow noreferrer">Lindstrom's theorem</a>, and in fact <a href="https://arxiv.org/abs/2008.01145" rel="nofollow noreferrer">Shelah/Vaananen</a> showed that there is no direct analogue of Lindstrom's theorem for logics without negation). Broadly speaking, a good rule of thumb is that existential second-order logic is &quot;tame&quot; in a way that its dual (universal second-order logic) isn't; for example, the latter but not the former can characterize well-foundedness, which turns out to be a very strong anti-tameness property.</p>
<p>The answer to this question is <strong>yes</strong>. There is a vast literature on the topic, and the term &quot;existential second-order&quot; will be a useful search term. One easy example is that a structure is infinite iff it can be expanded to a model of (say) Robinson's arithmetic <span class="math-container">$\mathsf{Q}$</span> in a fresh signature. Note that this leans heavily on the lack of negation in <span class="math-container">$\mathsf{ESO}$</span>: the reason infinitude is not <span class="math-container">$\mathsf{FOL}$</span>-expressible is roughly that if it were then finiteness would also be <span class="math-container">$\mathsf{FOL}$</span>-expressible and that would contradict compactness, but this relies on <span class="math-container">$\mathsf{FOL}$</span> having negation.</p>
<hr />
<p>Interestingly, if we ask for the stronger property of both <span class="math-container">$X$</span> and <span class="math-container">$\neg X$</span> being &quot;detectable&quot; in this way (and this was how I originally interpreted your question), we get a <strong>negative</strong> answer.</p>
<p>Let <span class="math-container">$\Sigma$</span> be a fixed language and suppose <span class="math-container">$X$</span> is a property of <span class="math-container">$\Sigma$</span>-structures of interest. Suppose <span class="math-container">$R_1, R_2$</span> are relation symbols not in <span class="math-container">$\Sigma$</span> and there are sentences <span class="math-container">$\varphi_1,\varphi_2$</span> in <span class="math-container">$\Sigma\sqcup\{R_1\},\Sigma\sqcup\{R_2\}$</span> respectively which &quot;detect <span class="math-container">$X$</span>-ness&quot; in the sense that for every <span class="math-container">$\Sigma$</span>-structure <span class="math-container">$\mathcal{M}$</span> we have</p>
<ul>
<li><p><span class="math-container">$\mathcal{M}$</span> has property <span class="math-container">$X$</span> iff <strong>some</strong> expansion of <span class="math-container">$\mathcal{M}$</span> satisfies <span class="math-container">$\varphi_1$</span>, and</p>
</li>
<li><p><span class="math-container">$\mathcal{M}$</span> fails property <span class="math-container">$X$</span> iff <strong>some</strong> expansion of <span class="math-container">$\mathcal{M}$</span> satisfies <span class="math-container">$\varphi_2$</span>.</p>
</li>
</ul>
<p>In this case, the pair <span class="math-container">$\varphi_1\wedge\varphi_2$</span> is inconsistent (given a putative model of <span class="math-container">$\varphi_1\wedge\varphi_2$</span>, does the reduct to <span class="math-container">$\Sigma$</span> satisfy <span class="math-container">$X$</span> or not?). This means <span class="math-container">$\vdash\varphi_1\rightarrow\neg\varphi_2$</span>. Applying <a href="https://en.wikipedia.org/wiki/Craig_interpolation" rel="nofollow noreferrer">Craig's interpolation theorem</a>, we get a <span class="math-container">$\Sigma$</span>-sentence <span class="math-container">$\theta$</span> entailed by <span class="math-container">$\varphi_1$</span> and entailing <span class="math-container">$\neg\varphi_2$</span>. This <span class="math-container">$\theta$</span>, then, exactly characterizes <span class="math-container">$X$</span>.</p>
<hr />
<p>At this point, it's worth seeing an example of a logic (necessarily not first-order logic <span class="math-container">$\mathsf{FOL}$</span>) for which Craig interpolation <em>fails</em>. The two most common extensions of <span class="math-container">$\mathsf{FOL}$</span>, namely the &quot;small&quot; infinitary logic <span class="math-container">$\mathcal{L}_{\omega_1,\omega}$</span> and second-order logic <span class="math-container">$\mathsf{SOL}$</span>, each do have the interpolation property (interestingly and trivially, respectively), so we have to go into the weeds a bit.</p>
<p>My personal favorite example is <span class="math-container">$\mathsf{FOL}(Q_\mathit{fin})$</span>, where we add to first-order logic the quantifier &quot;For finitely many.&quot; The point is that <span class="math-container">$(i)$</span> <strong>unlike</strong> <span class="math-container">$\mathsf{FOL}$</span> this logic we can pin down the standard model of arithmetic <span class="math-container">$\mathcal{N}=(\mathbb{N};+,\times)$</span> up to isomorphism, but <span class="math-container">$(ii)$</span> <strong>like</strong> <span class="math-container">$\mathsf{FOL}$</span> this logic can in <span class="math-container">$\mathcal{N}$</span> give an inductive definition of its own full theory of <span class="math-container">$\mathcal{N}$</span>. These facts, combined with (the proof of) <a href="https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem" rel="nofollow noreferrer">Tarski's undefinability theorem</a>, give us the failure of Beth definability (a corollary of Craig interpolation) for <span class="math-container">$\mathsf{FOL}(Q_\mathit{fin})$</span>.</p>
<p>Vaananen's article <a href="https://link.springer.com/article/10.1007/s11229-008-9357-z" rel="nofollow noreferrer"><em>The Craig interpolation theorem in abstract model theory</em></a> contains a lot of good information about this topic, albeit at a high level.</p>

CC BY-SA 4.0
2023-09-15T16:21:26.240Z
As noted in the comments, the question is unclear. But under the “for every expansion” reading that you seem to have adopted, you don’t need anything as heavy-handed as Craig’s interpolation (which fails for finite model theory, anyway); it follows trivially by interpreting $R$ as $\varnothing$, as also noted in the comments.
Emil Jeřábek
CC BY-SA 4.0
2023-09-15T16:39:27.000Z
@EmilJeřábek Sorry, that was of course a typo. Fixed!
Noah Schweber
CC BY-SA 4.0
2023-09-15T17:32:32.997Z
Thanks! My intended interpretation of the question was exactly this, that $\mathcal{M}$ has property $X$ iff some extension of $\mathcal{M}$ satisfies $\phi_1$. But in your argument above you seem to assume that there is also a formula for characterizing the failure to have the property ($\phi_2$), which I think is a stronger assumption, isn't it?
Nicola Gigante
CC BY-SA 4.0
2023-09-15T17:39:29.537Z
I've added an example that I think I've found after posting the question. Is it correct?
Nicola Gigante
CC BY-SA 4.0
2023-09-15T17:39:43.127Z
@gigabytes If you assume this interpretation, and do not require the same for complement, then the answer is simply that a property can be characterized like this if and only if it is $\Sigma^1_1$-definable (this is more or less just restating the definition). In the realm of of finite models, a property invariant under isomorphism  is $\Sigma^1_1$ iff it is in NP. An example of such a property that isn't FO-definable is non-connectedness.
Emil Jeřábek
CC BY-SA 4.0
2023-09-15T17:41:50.250Z
Yes, that's the sort of characterization I was looking for
Nicola Gigante
CC BY-SA 4.0
2023-09-15T18:18:08.767Z
@gigabytes I've edited my answer to align with your clarified question.
Noah Schweber
CC BY-SA 4.0
2023-09-15T18:23:00.763Z
Thanks! That is what I was looking for! I don't know who downvoted it!
Nicola Gigante
CC BY-SA 4.0
2023-09-15T16:17:06.117Z
2023-09-15T18:24:18.920Z
2023-09-15T18:24:18.920Z
Noah Schweber
<p>First, a terminological note: an <em>extension</em> of a model is a model in the same signature obtained by adding elements into the domain. What you are talking about is called an <em>expansion</em> (new relations are added to the signature, but the domain and old relations are preserved).</p>
<p>A property can be characterized as stipulated in the question if and only if it is <span class="math-container">$\Sigma^1_1$</span>-definable (i.e., expressible in existential second-order logic). This is pretty much just by definition.</p>
<p>In the realm of finite models, Fagin’s theorem states that a property is <span class="math-container">$\Sigma^1_1$</span>-definable if and only if it is in NP and invariant under isomorphism.</p>
<p>As meanwhile added to the question, a simple example that’s not first-order definable is the property that <span class="math-container">$d$</span> is <em>not</em> reachable from <span class="math-container">$s$</span>.</p>
<p>The property that <span class="math-container">$d$</span> <em>is</em> reachable from <span class="math-container">$s$</span> is also expressible in this way, as it is computable in NP (or indeed, NL). The following formula should work:</p>
<p><span class="math-container">$$\begin{align*}
\forall x\,x\nless x&amp;\land\forall x,y,x\,(x&lt;y\land y&lt;z\to x&lt;z)\\
&amp;\land\forall x,y\,(P(x,y)\leftrightarrow(x=s\lor\exists u,v\,(P(u,v)\land R(u,x)\land v&lt;y)))\\
&amp;\land\exists y\,P(d,y).
\end{align*}$$</span></p>
<p>This expresses the construction of the set of elements reachable from <span class="math-container">$s$</span> by induction along a partial order <span class="math-container">$&lt;$</span> (which you can think of simply as a linear order, but it only matters for soundness that is well-founded).</p>

CC BY-SA 4.0
2023-09-15T19:31:40.650Z
Thanks! Also for the terminological clarification. I've changed extension to expansion in the question.
Nicola Gigante
CC BY-SA 4.0
2023-09-15T18:26:39.927Z
2023-09-15T18:26:39.927Z
Emil Jeřábek
<p>Think of the classical inexpressivity results that one studies in early courses about first-order logic, <em>e.g.</em> that on a signature with a binary predicate <span class="math-container">$R$</span> one cannot express that <span class="math-container">$R$</span> is connected. Or, that one cannot express <span class="math-container">$R$</span>-reachability between two points <span class="math-container">$x$</span> and <span class="math-container">$y$</span>.</p>
<p>Now I'm wondering what happens if I extend the language. Does any such property become expressible? For example, in a signature with <span class="math-container">$R$</span> and <em>something else</em>, can I express connectivity of <span class="math-container">$R$</span>?</p>
<p>Are there examples of properties not FO-expressible in a signature but expressible in an extended signature?</p>
<p>I'm not considering here extending the theory as well. So if you have <span class="math-container">$&gt;$</span> and extend the signature with an interpreted <span class="math-container">$+$</span>, that's not what I'm looking for.</p>
<p><strong>Edit</strong>: I'll add an example that I've found after posting the question.</p>
<p>Take the signature <span class="math-container">$\Sigma$</span> with a binary predicate <span class="math-container">$R$</span> and two constants <span class="math-container">$s$</span> and <span class="math-container">$d$</span>. Let <span class="math-container">$X$</span> be the property of <span class="math-container">$d$</span> being <em>not</em> <span class="math-container">$R$</span>-reachable from <span class="math-container">$s$</span>. <span class="math-container">$X$</span> is not expressible in FO. But if I consider <span class="math-container">$\Sigma'$</span> which adds a unary predicate <span class="math-container">$P$</span>, I can write:</p>
<p><span class="math-container">$$
  \psi\equiv P(s) \land \forall xy ((P(x) \land R(x,y)) \to P(y)) \land \neg P(d)
$$</span></p>
<p>Is it correct that a structure <span class="math-container">$\mathcal{M}$</span> has property <span class="math-container">$X$</span> iff <span class="math-container">$\psi$</span> is satisfied in <em>some</em> expansion of <span class="math-container">$\mathcal{M}$</span>? This extension would be the one where <span class="math-container">$P$</span> is interpreted as the fixpoint of <span class="math-container">$R$</span>.</p>
<p>Is all of this correct?</p>

CC BY-SA 4.0
2023-09-15T14:50:11.287Z
The question is ambiguous as to what expansions of the original models you consider. E.g., *any* property becomes expressible if you expand the signature with a nullary predicate that is true in a given model iff the original property holds.
Emil Jeřábek
CC BY-SA 4.0
2023-09-15T14:53:15.433Z
But if you want a sentence that expresses the property in *exery* expansion of the original model to the new signature, then this is equivalent to first-order expressivity, as you can always define some such expansion in the original model itself (e.g., make all new predicates empty).
Emil Jeřábek
CC BY-SA 4.0
2023-09-15T16:07:12.347Z
What does it mean to extend the signature, but not the theory? If you add a new symbol $\phi$ but no axioms for it, you won't be able to do much with $\phi$.
Martin Berger
CC BY-SA 4.0
2023-09-15T17:58:30.340Z
I don’t think the formula $\psi$ in the edit does what you think it does, as it is logically equivalent to $\forall x\,P(x)\land\forall x\,\forall y\,R(x,y)$.
Emil Jeřábek
CC BY-SA 4.0
2023-09-15T18:20:46.507Z
Yes, that was wrong. I should have looked for expressing *non*-reachability, and the "iff" was wrong. Now it should be ok.
Nicola Gigante
<first-order-logic>
Inexpressibility results for first-order logic that fail extending the language
Nicola Gigante
# Inexpressibility results for first-order logic that fail extending the language

(Asked by: username_0 on 2023-09-15)

Think of the classical inexpressivity results that one studies in early courses about first-order logic, *e.g.* that on a signature with a binary predicate $R$ one cannot express that $R$ is connected. Or, that one cannot express $R$-reachability between two points $x$ and $y$.

Now I'm wondering what happens if I extend the language. Does any such property become expressible? For example, in a signature with $R$ and *something else*, can I express connectivity of $R$?

Are there examples of properties not FO-expressible in a signature but expressible in an extended signature?

I'm not considering here extending the theory as well. So if you have $>$ and extend the signature with an interpreted $+$, that's not what I'm looking for.

**Edit**: I'll add an example that I've found after posting the question.

Take the signature $\Sigma$ with a binary predicate $R$ and two constants $s$ and $d$. Let $X$ be the property of $d$ being *not* $R$-reachable from $s$. $X$ is not expressible in FO. But if I consider $\Sigma'$ which adds a unary predicate $P$, I can write:

$$
\psi\equiv P(s) \land \forall xy ((P(x) \land R(x,y)) \to P(y)) \land \neg P(d)
$$

Is it correct that a structure $\mathcal{M}$ has property $X$ iff $\psi$ is satisfied in *some* expansion of $\mathcal{M}$? This extension would be the one where $P$ is interpreted as the fixpoint of $R$.

Is all of this correct?

**Tags:** first-order-logic

> **Comments:**
> **username_1**: The question is ambiguous as to what expansions of the original models you consider. E.g., *any* property becomes expressible if you expand the signature with a nullary predicate that is true in a given model iff the original property holds.  
> **username_1**: But if you want a sentence that expresses the property in *exery* expansion of the original model to the new signature, then this is equivalent to first-order expressivity, as you can always define some such expansion in the original model itself (e.g., make all new predicates empty).  
> **username_2**: What does it mean to extend the signature, but not the theory? If you add a new symbol $\phi$ but no axioms for it, you won't be able to do much with $\phi$.  
> **username_1**: I don’t think the formula $\psi$ in the edit does what you think it does, as it is logically equivalent to $\forall x\,P(x)\land\forall x\,\forall y\,R(x,y)$.  
> **username_0**: Yes, that was wrong. I should have looked for expressing *non*-reachability, and the "iff" was wrong. Now it should be ok.  

---

## 2 answers

### Answer by username_3 on 2023-09-15. Score: 1 | Accepted answer

As noted in the comments it takes some care to phrase this question in a nontrivial way. However, this can be done in at least a couple ways, one yielding a positive answer and the other yielding a negative answer.

---

As clarified in your edit, you have in mind the following question: is there a non-first-order property $X$ of structures which is *existentially second-order* (= $\Sigma^1\_1$ or $\mathsf{ESO}$) characterizable? Here $\mathsf{ESO}$ is the logic which allows expressions of the form "Some expansion of the universe satisfies $\varphi$" for $\varphi\in\mathsf{FOL}$. Note that $\mathsf{ESO}$ is quite a nice logic in many respects - e.g. it is fully compact and has downward Lowenheim-Skolem - but it is not closed under negation (so we don't contradict [Lindstrom's theorem](https://en.wikipedia.org/wiki/Lindstr%C3%B6m%27s_theorem), and in fact [Shelah/Vaananen](https://arxiv.org/abs/2008.01145) showed that there is no direct analogue of Lindstrom's theorem for logics without negation). Broadly speaking, a good rule of thumb is that existential second-order logic is "tame" in a way that its dual (universal second-order logic) isn't; for example, the latter but not the former can characterize well-foundedness, which turns out to be a very strong anti-tameness property.

The answer to this question is **yes**. There is a vast literature on the topic, and the term "existential second-order" will be a useful search term. One easy example is that a structure is infinite iff it can be expanded to a model of (say) Robinson's arithmetic $\mathsf{Q}$ in a fresh signature. Note that this leans heavily on the lack of negation in $\mathsf{ESO}$: the reason infinitude is not $\mathsf{FOL}$-expressible is roughly that if it were then finiteness would also be $\mathsf{FOL}$-expressible and that would contradict compactness, but this relies on $\mathsf{FOL}$ having negation.

---

Interestingly, if we ask for the stronger property of both $X$ and $\neg X$ being "detectable" in this way (and this was how I originally interpreted your question), we get a **negative** answer.

Let $\Sigma$ be a fixed language and suppose $X$ is a property of $\Sigma$-structures of interest. Suppose $R\_1, R\_2$ are relation symbols not in $\Sigma$ and there are sentences $\varphi\_1,\varphi\_2$ in $\Sigma\sqcup\{R\_1\},\Sigma\sqcup\{R\_2\}$ respectively which "detect $X$-ness" in the sense that for every $\Sigma$-structure $\mathcal{M}$ we have

* $\mathcal{M}$ has property $X$ iff **some** expansion of $\mathcal{M}$ satisfies $\varphi\_1$, and
* $\mathcal{M}$ fails property $X$ iff **some** expansion of $\mathcal{M}$ satisfies $\varphi\_2$.

In this case, the pair $\varphi\_1\wedge\varphi\_2$ is inconsistent (given a putative model of $\varphi\_1\wedge\varphi\_2$, does the reduct to $\Sigma$ satisfy $X$ or not?). This means $\vdash\varphi\_1\rightarrow\neg\varphi\_2$. Applying [Craig's interpolation theorem](https://en.wikipedia.org/wiki/Craig_interpolation), we get a $\Sigma$-sentence $\theta$ entailed by $\varphi\_1$ and entailing $\neg\varphi\_2$. This $\theta$, then, exactly characterizes $X$.

---

At this point, it's worth seeing an example of a logic (necessarily not first-order logic $\mathsf{FOL}$) for which Craig interpolation *fails*. The two most common extensions of $\mathsf{FOL}$, namely the "small" infinitary logic $\mathcal{L}\_{\omega\_1,\omega}$ and second-order logic $\mathsf{SOL}$, each do have the interpolation property (interestingly and trivially, respectively), so we have to go into the weeds a bit.

My personal favorite example is $\mathsf{FOL}(Q\_\mathit{fin})$, where we add to first-order logic the quantifier "For finitely many." The point is that $(i)$ **unlike** $\mathsf{FOL}$ this logic we can pin down the standard model of arithmetic $\mathcal{N}=(\mathbb{N};+,\times)$ up to isomorphism, but $(ii)$ **like** $\mathsf{FOL}$ this logic can in $\mathcal{N}$ give an inductive definition of its own full theory of $\mathcal{N}$. These facts, combined with (the proof of) [Tarski's undefinability theorem](https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem), give us the failure of Beth definability (a corollary of Craig interpolation) for $\mathsf{FOL}(Q\_\mathit{fin})$.

Vaananen's article [*The Craig interpolation theorem in abstract model theory*](https://link.springer.com/article/10.1007/s11229-008-9357-z) contains a lot of good information about this topic, albeit at a high level.

> **Comments:**
> **username_1**: As noted in the comments, the question is unclear. But under the “for every expansion” reading that you seem to have adopted, you don’t need anything as heavy-handed as Craig’s interpolation (which fails for finite model theory, anyway); it follows trivially by interpreting $R$ as $\varnothing$, as also noted in the comments.  
> **username_3**: @EmilJeřábek Sorry, that was of course a typo. Fixed!  
> **username_0**: Thanks! My intended interpretation of the question was exactly this, that $\mathcal{M}$ has property $X$ iff some extension of $\mathcal{M}$ satisfies $\phi_1$. But in your argument above you seem to assume that there is also a formula for characterizing the failure to have the property ($\phi_2$), which I think is a stronger assumption, isn't it?  
> **username_0**: I've added an example that I think I've found after posting the question. Is it correct?  
> **username_1**: @gigabytes If you assume this interpretation, and do not require the same for complement, then the answer is simply that a property can be characterized like this if and only if it is $\Sigma^1_1$-definable (this is more or less just restating the definition). In the realm of of finite models, a property invariant under isomorphism  is $\Sigma^1_1$ iff it is in NP. An example of such a property that isn't FO-definable is non-connectedness.  
> **username_0**: Yes, that's the sort of characterization I was looking for  
> **username_3**: @gigabytes I've edited my answer to align with your clarified question.  
> **username_0**: Thanks! That is what I was looking for! I don't know who downvoted it!  

---

### Answer by username_1 on 2023-09-15. Score: 1

First, a terminological note: an *extension* of a model is a model in the same signature obtained by adding elements into the domain. What you are talking about is called an *expansion* (new relations are added to the signature, but the domain and old relations are preserved).

A property can be characterized as stipulated in the question if and only if it is $\Sigma^1\_1$-definable (i.e., expressible in existential second-order logic). This is pretty much just by definition.

In the realm of finite models, Fagin’s theorem states that a property is $\Sigma^1\_1$-definable if and only if it is in NP and invariant under isomorphism.

As meanwhile added to the question, a simple example that’s not first-order definable is the property that $d$ is *not* reachable from $s$.

The property that $d$ *is* reachable from $s$ is also expressible in this way, as it is computable in NP (or indeed, NL). The following formula should work:

$$\begin{align\*}
\forall x\,x\nless x&\land\forall x,y,x\,(x

This expresses the construction of the set of elements reachable from $s$ by induction along a partial order $<$ (which you can think of simply as a linear order, but it only matters for soundness that is well-founded).

> **Comments:**
> **username_0**: Thanks! Also for the terminological clarification. I've changed extension to expansion in the question.  

---

