Can every first-order theory be conservatively “second-order-ized”

first-order-logiclogicmodel-theorypredicate-logicsolution-verification

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.

Best Answer

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.

Related Question