0
$\begingroup$

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?

$\endgroup$
5
  • 1
    $\begingroup$ 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. $\endgroup$ Commented Sep 15, 2023 at 14:50
  • 1
    $\begingroup$ 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). $\endgroup$ Commented Sep 15, 2023 at 14:53
  • $\begingroup$ 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$. $\endgroup$ Commented Sep 15, 2023 at 16:07
  • $\begingroup$ 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)$. $\endgroup$ Commented Sep 15, 2023 at 17:58
  • $\begingroup$ Yes, that was wrong. I should have looked for expressing non-reachability, and the "iff" was wrong. Now it should be ok. $\endgroup$ Commented Sep 15, 2023 at 18:20

2 Answers 2

1
$\begingroup$

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, and in fact Shelah/Vaananen 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, 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, 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 contains a lot of good information about this topic, albeit at a high level.

$\endgroup$
8
  • $\begingroup$ 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. $\endgroup$ Commented Sep 15, 2023 at 16:21
  • $\begingroup$ @EmilJeřábek Sorry, that was of course a typo. Fixed! $\endgroup$ Commented Sep 15, 2023 at 16:39
  • 1
    $\begingroup$ 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? $\endgroup$ Commented Sep 15, 2023 at 17:32
  • $\begingroup$ I've added an example that I think I've found after posting the question. Is it correct? $\endgroup$ Commented Sep 15, 2023 at 17:39
  • 1
    $\begingroup$ @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. $\endgroup$ Commented Sep 15, 2023 at 17:39
1
$\begingroup$

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<y\land y<z\to x<z)\\ &\land\forall x,y\,(P(x,y)\leftrightarrow(x=s\lor\exists u,v\,(P(u,v)\land R(u,x)\land v<y)))\\ &\land\exists y\,P(d,y). \end{align*}$$

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).

$\endgroup$
1
  • $\begingroup$ Thanks! Also for the terminological clarification. I've changed extension to expansion in the question. $\endgroup$ Commented Sep 15, 2023 at 19:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.