Can every first-order theory be conservatively "second-order-ized"?

Question

Basically the idea is to define comprehension over first-order formulas in $T$. I give complete details below, but as a preview

Questions:

1. Starting from an arbitrary (single-sorted $O$) first-order theory $T$ over language $\mathcal{L} = (O, \dots)$, is the resulting many-sorted first-order theory $\tilde{T}$ over the extended language $\tilde{L}=(O,S, \tilde{\in}, \dots)$ always a conservative extension of $T$?

2. Is it true that $(\mathfrak{M}, \mathfrak{F}) \models \tilde{T}$ if and only if $\mathfrak{M} \models T$, $\mathfrak{F} \subseteq \mathcal{P}(\mathfrak{M})$, and $\mathsf{Def}_{\mathcal{L}}(\mathfrak{M}) \subseteq \mathfrak{F}$?

   In particular, among models of $\tilde{T}$ whose "first-order part" is $\mathfrak{M}$, is it true that $(\mathfrak{M}, \mathsf{Def}_{\mathcal{L}}(\mathfrak{M}))$ is always minimal?

Note: The first part of this unanswered question is similar to, but both less general and much less specific than, this question.

I've posted an attempt at answering these questions as a community wiki answer.

Details:
Let $T$ be an arbitrary first-order theory, assumed (without loss of generality) to be single-sorted, over the language $\mathcal{L}$.
(Call the original/first sort "$O$" for "objects" for the sake of concreteness.)

Define a new language $\tilde{\mathcal{L}}$ that extends $\mathcal{L}$ by adding a new / second sort (called "$C$" for "collections" for the sake of concreteness), and a binary predicate / relation $\tilde{\in}$ which takes terms of the first sort ("objects") for its first argument and terms of the second sort ("collections") for its second sort.

Finally define the new (many-sorted) first-order theory $\tilde{T}$ over the language $\tilde{\mathcal{L}}$ which has all of the same axioms as $T$ (i.e. over the sub-language $\mathcal{L} \subseteq \tilde{\mathcal{L}}$) along with the following axiom schema:

• For every well-formed formula $\psi(o, \bar{\omega})$ in the language $\mathcal{L}$ (NOT $\tilde{\mathcal{L}}$ - this is extremely important) with "argument free variable" $o$ and "parameter free variables" $\bar{\omega}$, the following is an axiom: $$ \forall^O \bar{\omega} \left( \exists^C c_{\psi, \bar{\omega}} \left( \forall^O o ( \psi(o, \bar{\omega}) \leftrightarrow o \tilde{\in} c_{\psi, \bar{\omega}} \right) \right) $$

Here $\bar{\omega}$ is shorthand for a (metalanguage) tuple $(\omega_1, \dots, \omega_n)$ of ($O$-sort, "object") variables, where $n$ is some definite but unspecified (metalanguage) natural number that in general depends on the specific well-formed formula $\psi$. Similarly, $\forall^O \bar{\omega}$ is just shorthand for $\forall^O \omega_1 \forall^O \omega_2 \dots \forall^O \omega_n$.

$\mathsf{Def}_{\mathcal{L}}(\mathfrak{M})$ is intended to denote the collection of all subsets of $\mathfrak{M}$ that are definable over the language $\mathcal{L}$ with arbitrary parameters from $\mathfrak{M}$.

E.g. assuming $T$ is a first-order theory with equality, all singleton subsets $\{m\}$ would be included for $m \in \mathfrak{M}$ e.g. by using the formula $x = y$ and the valuation sending the variable $y$ to the element $m$.

Comment: Technically this only defines comprehension for "monadic" or "unary" formulas, rather than arbitrary arity formulas, as arguably a "true second-order-ization" would do. Basically I'm assuming here that the same arguments would go through in that case (as it would for functions, to the extent those can be defined in terms of relations in first-order-logic-with-equality). Also the examples I'm interested in only need / use "monadic / unary comprehension" anyway.

Answer 1

To expand a first-order theory to a second-order theory conservatively (i.e. without adding new first-order definable sets) you have to add a sort for every "definition-scheme". I.e. a sort for every partitioned formula $\varphi(x;y)$.

The canonical expansion of a first-order structure $M$ has, beside the domain of the home sort $M$, a domain for each sort $\varphi(x;y)$ that contains (as elements) the sets $\varphi(U;b)$ where $U$ is a large saturated extension of $M$ and $b∈ M^y$.

In the language of of $M$ is expanded with the membership relations.

---

You find the construction above, with all the gory details, in the Section 13.2 (The eq-expansion) of these notes. In the notes a second-order expansion is used to construct (a version of) Shelah's $T^{\rm eq}$.

If I understand it well, this comes close to the expansion you are proposing, only much tamer form the model-theoretic point of view.

Answer 2

Attempt (community wiki):

Note that for 2. I've been sloppy in declaring that $\mathfrak{F} \subseteq \mathcal{P}(\mathfrak{M})$ because the Tarskian semantics for multi-sorted logic don't require that. In general $\mathfrak{F}$ could be any set.

However, my understanding is that one can assume without loss of generality that $\mathfrak{F} \subseteq \mathcal{P}(\mathcal{M})$, in the following way.

Let's say we have some structure $\tilde{\mathfrak{F}}$ for the collections (that may or may not consist of subsets of $\mathfrak{M}$). Then we can define a (possibly new) structure $\mathfrak{F} \subseteq \mathcal{P}(\mathfrak{M})$ via the map $\tilde{\mathfrak{F}} \to \mathfrak{F}$ with rule of assignment $$ \tilde{f} \mapsto \{ m \in \mathfrak{M}: \tilde{E}(m, \tilde{f}) \} ,$$ where $\tilde{E}$ is the interpretation of $\tilde{\in}$ in $\tilde{\mathfrak{F}}$. (I guess I also left it implicit in the question that the interpretation of $\tilde{\in}$ in any $\mathfrak{F} \subseteq \mathcal{P}(\mathfrak{M})$ would be the restriction of $\in$ of the ambient set theory.)

Anyway, regarding 1., I am not sure at all how one would prove it via proof-theoretic means, although presumably there is a way. My understanding though is that if one can prove that the answer to 2. is correct, then the combination of the soundness and completeness theorem would mean that the model-theoretic result also implicitly proves the proof-theoretic result 1.

Specifically, I am asserting that if it is true that all models of $\tilde{T}$ have as their first-order part a model of $T$, and that for every model of $T$ there is at least one corresponding model of $\tilde{T}$ with that as its first-order part, then by the Godel completeness theorem this means that the only things $\tilde{T}$ can prove about statements restricted to $\mathcal{L}$ are those that can be proved by $T$, i.e. $\tilde{T}$ is conservative over $T$. I'm not really certain whether that's correct or precise enough.

So for proving 2., the general idea would be that presumably the only new atomic formulas that are introduced by augmenting $\mathcal{L}$ to $\tilde{\mathcal{L}}$ are of the form $o \tilde{\in} c$. But (1) I'm not sure whether it's really true that those are the only new atomic formulas, or whether others are "sneaking in" that I'm not noticing, and (2) if they are the only ones, how to prove that that's the case.

If it's true, then basically the proof strategy would be to try to show that all such atomic formulas $o \tilde{\in} c$ can be "eliminated", or replaced with statements entirely in $\mathcal{L}$ which are proven by $T$.

This seems to divide into three cases: (1) $c$ corresponds to a (explicitly defined) wff. $\psi$ via the axiom schema, (2a) $c$ does not correspond to a wff. but does correspond to an implicitly defined formula, (2b) $c$ does not correspond to any sort of formula.

This is where I start to have a lot of confusion, which seems to be related to that expressed in this other related question. Specifically regarding (2b), which I can only think of how to potentially address model-theoretically. Because even though our intended models for the collections sort $C$ is always $\mathsf{Def}_{\mathcal{L}}(\mathfrak{M})$, that doesn't mean we can't have models for $C$ that are strict supersets of $\mathsf{Def}_{\mathcal{L}}(\mathfrak{M})$ (i.e. even when using the trick to force the interpretation of $C$ to be a subset of $\mathcal{P}(\mathfrak{M})$). And for those possible valuations of $C$-sort variables $c$ corresponding to elements $\mathfrak{F} \setminus \mathsf{Def}_{\mathcal{L}}(\mathfrak{M})$, I am very unsure how, if at all one could reason about them proof-theoretically.

For case (1), the proof seems to be easy, i.e. we basically have a definitorial expansion, because we can replacement the statement $o \in c_{\psi,\bar{\omega}}$ with the $\mathcal{L}$-sentence $\forall^O \bar{\omega} \psi(o, \bar{\omega})$ (basically the axiom schema was rigged to accomplish this).

For case (2a), apparently the Beth definability theorem says that in fact it is the same as case (1), i.e. "no new / nonstandard formulas sneak in the back door". (But I seriously doubt I actually understand the statement of the Beth definability theorem, much less whether I am applying it correctly. I certainly don't understand its generalization, the Craig interpolation theorem.)

So again that would seem to only leave (2b) which I can only think to handle model theoretically. But basically because in that case the variable $c$ doesn't even implicitly define a predicate, that seems to mean it would "correspond to a parameter present in the "second-order part" $\mathfrak{F}$ part of some models of $\tilde{T}$ but not present in other models of $\tilde{T}$". (I know that statement doesn't actually make sense.) So then basically we would conclude by the Godel completeness theorem that $\tilde{T}$ can not prove anything about statements involving it, in particular the one we care about $o \tilde{\in} c$? And because apparently $\tilde{T}$ can't prove anything about $o \tilde{\in} c$ in that case, it would follow that $\tilde{T}$ can't use it to prove anything over the sublanguage $\mathcal{L} \subseteq \tilde{\mathcal{L}}$. So in this case too the collection of true sentences over $\mathcal{L}$ is not expanded by $\tilde{T}$?

So assuming the argument for (2b) is actually correct, we would get a proof that no additional statements in the language $\mathcal{L}$ are proved by $\tilde{T}$, and thus that $\tilde{T}$ is conservative over $T$?