Is there a natural intermediate version of PA

logicmodel-theorypeano-axiomsset-theory

Below, "logic" means "regular logic containing first-order logic" in the sense of Ebbinghaus/Flum/Thomas.

Setup

For a logic $\mathcal{L}$, let $\mathcal{PA}(\mathcal{L})$ be the set of $\mathcal{L}$-sentences in the language of arithmetic consisting of:

  • the ordered semiring axioms, and

  • for each $\mathcal{L}$-formula $\varphi(x,y_1,…,y_n)$ the induction instance $$\forall y_1,…,y_n[[\varphi(0,y_1,…,y_n)\wedge\forall x(\varphi(x,y_1,…,y_n)\rightarrow\varphi(x+1,y_1,…,y_n))]\rightarrow\forall x\varphi(x,y_1,…,y_n)].$$

(Note that even if the new logic $\mathcal{L}$ has additional types of variable – e.g. "set" variables – the corresponding induction instances will only allow "number" variables $y_1,…,y_n$ for the parameters.)

For example, $\mathcal{PA}(FOL)$ is just the usual (first-order) PA, and $\mathcal{PA}(SOL)$ characterizes the standard model $\mathbb{N}$ up to isomorphism. Also, we always have $\mathbb{N}\models_\mathcal{L}\mathcal{PA}(\mathcal{L})$.

  • Note that it's not quite true that $\mathcal{PA}(SOL)$ "is" second-order PA as usually phrased – induction-wise, we still have a scheme as opposed to a single sentence. However, induction applied to "has finitely many predecessors" gets the job done. (If we run the analogous construction with ZFC in place of PA, though, things seem more interesting ….)

Question

Say that a logic $\mathcal{L}$ is PA-intermediate if we have $PA<\mathcal{PA}(\mathcal{L})<Th_{FOL}(\mathbb{N})$ in the following sense:

  • There is a first-order sentence $\varphi$ such that $PA\not\models\varphi$ but $\mathcal{PA}(\mathcal{L})\models\varphi$.

  • There is a first-order sentence $\theta$ such that $\mathbb{N}\models\theta$ but $\mathcal{PA}(\mathcal{L})\not\models\theta$.

Is there a "natural" PA-intermediate logic?

(This is obviously fuzzy; for precision, I'll interpret "natural" as "has appeared in at least two different papers whose respective authorsets are incomparable.")

Partial progress

  • A couple non-examples:

    • Infinitary logic $\mathcal{L}_{\omega_1,\omega}$ is not PA-intermediate, since in fact $\mathcal{PA}(\mathcal{L}_{\omega_1,\omega})$ pins down $\mathbb{N}$ up to isomorphism (consider $\forall x(\bigvee_{i\in\omega}x=1+…+1\mbox{ ($i$ times)}$). So both second-order and infinitary logic bring in too much extra power.

    • Adding an equicardinality quantifier ($Ix(\varphi(x);\psi(x))$ = "As many $x$ satisfy $\varphi$ as $\psi$") also results in pinning down $\mathbb{N}$ up to isomorphism (consider "$\neg$ As many $x$ are $<k$ as are $<k+1$"). If we add the weak equicardinality quantifer $Qx\varphi(x) = Ix(\varphi(x);\neg\varphi(x))$, on the other hand, we wind up with a conservative extension of $PA$. That said, the latter is stronger semantically: no countable nonstandard model of $PA$ satisfies $\mathcal{PA}(FOL[Q])$ (to prove conservativity over $PA$ we look at the $\omega_1$-like models).

    • Fragments of second-order logic don't seem to help either: both $\mathcal{PA}(\Pi^1_1)$ and $\mathcal{PA}(\Sigma^1_1)$ pin down $\mathbb{N}$ (see here).

  • The proof of Lindstrom's theorem yields a weak negative result: if $\mathcal{L}$ is a logic strictly stronger than first-order logic with the downward Lowenheim-Skolem property, then we can whip up an $\mathcal{L}$-sentence $\varphi$ and an appropriate tuple of formulas $\Theta$ such that $\varphi$ is satisfiable and $\Theta^M\cong\mathbb{N}$ in every $M\models\varphi$. So an example for the above question would have to either allow nasty implicit definability shenanigans or lack the downward Lowenheim-Skolem property. This rules out a whole additional slew of candidates. That said, there is a surprising amount of variety among logics without the downward Lowenheim-Skolem property even in relatively concrete contexts – e.g. there is a compact logic strictly stronger than FOL on countable structures.

Best Answer

This is a continuation of my answer to your easier version of this question on MathOverflow. As I wrote out this argument, I realized that it's not quite as easy as I thought when I originally wrote my comment on the other post, and I can now only claim a weaker result, but it is still sufficient to answer this question.

In the MO answer, we already established that $\mathrm{Con}(\mathsf{PA})$ is a first-order sentence that $\mathsf{PA}(Q_{\mathrm{Brch}})$ entails but which is not entailed by $\mathsf{PA}$.

I will show that there is a c.e. extension $\mathsf{Z}_2^{US}$ of $\mathsf{Z}_2$ (in a bigger language) with the property that if $(M,S)$ is a model of $\mathsf{Z}_2^{US}$, then there is a (first-order) elementary extension $(M',S') \succeq (M,S)$ such that $M' \models \mathsf{PA}(Q_{\mathrm{Brch}})$. By Gödel, this establishes that $\mathsf{PA}(Q_{\mathrm{Brch}}) \not \models \mathrm{Con}(\mathsf{Z}_2^{US})$. (I will denote models of second-order arithmetic like $(M,S)$, with $M$ the numbers sort and $S$ the set sort.)

This argument is partially based on the proof of compactness for $\mathcal{L}(Q_{\mathrm{Brch}})$ in Section 3.1 of this paper of Mekler and Shelah. Although this argument is actually easier, because we can lean on the coding structure of arithmetic.

Let $\mathcal{L}^U$ be the language of second order arithmetic augmented with a single new unary predicate on the set sort. Let $\mathcal{L}^{US}$ be this language enriched with Skolem functions in both sorts. Let $\mathsf{Z}_2^{US}$ be the $\mathcal{L}^{US}$ theory which consists of

  • $\mathsf{Z}_2$ with comprehension extended to all $\mathcal{L}^{US}$-formulas,
  • the assertion that $U$ is an (internal) non-principal ultrafilter on the number sort (i.e., any set of the form $[a,\infty)$ satisfies $U$; if $X$ satisfies $U$, then any superset of $X$ satisfies $U$; and if $X$ and $Y$ satisfy $U$, then $X\cap Y$ satisfies $U$), and
  • the assertion that the Skolem functions in $\mathcal{L}^{US}$ are Skolem functions.

By taking the standard model of $\mathsf{Z}_2$ and appending a non-principal ultrafilter and Skolem functions, we can see that $\mathsf{Z}_2^{US}$ is consistent. It is clearly a c.e. theory, and by Gödel we have that $\mathsf{Z}_2^{US}\not \vdash \mathrm{Con}(\mathsf{Z}_2^{US})$.

Note that for any $(M,S) \models \mathsf{Z}_2^{US}$, the predicate $U$ defines a complete type over $MS$ in the number sort. Call this type $p|_{MS}$. Note furthermore that if $a$ realizes this type, then every element of the Skolem hull of $MSa$ realizes an $MS$-definable type over $MS$.

Fix $(M,S)\models \mathsf{Z}_2^{US}$. Fix an uncountable regular cardinal $\kappa > |MS|$. Let $(M_0,S_0) = (M,S)$. For each positive ordinal $\alpha < \kappa$, given $(M_\beta,S_\beta)$ for $\beta < \alpha$,

  • if $\alpha = \gamma +1$, then let $(M_\alpha,S_\alpha)$ be the Skolem hull of $M_\gamma S_\gamma a$, where $a$ is a realization of $p|_{M_\gamma S_\gamma}$ and
  • if $\alpha$ is a limit ordinal, let $(M_\alpha,S_\alpha) = \bigcup_{\beta < \alpha} (M_\beta,S_\beta)$.

Finally, let $(M',S') = \bigcup_{\alpha < \kappa} (M_\alpha,S_\alpha)$. By a not-too-difficult induction argument, one can show that for any $\alpha$, and any $c \in (M',S')$, the type of $c$ over $M_\alpha S_\alpha$ is $M_\alpha S_\alpha$-definable. Note also that for each $\alpha < \kappa$, $|M_\alpha S_\alpha| < \kappa$.

Fact. For any formula $\varphi(x,y,\bar{z})$, there is a formula $\psi(x,y,\bar{z})$ such that for any $\bar{a}$, if $\varphi(x,y,\bar{a})$ defines a directed partial order on the number sort with no largest element, then $\psi(x,y,\bar{a})$ defines a function from the number sort to itself which is strictly order preserving (from the ordinary order to $\varphi(x,y,\bar{a})$) and which is cofinal in the partial order.

Proof. Easy induction argument. $\square$

This implies that in each $(M_{\alpha+1},S_{\alpha+1})$, for any directed $M_{\alpha}S_\alpha$-definable partial order $<$ on $M_\alpha$, there is some $a \in M_{\alpha+1}$ such is $<$-greater than every element of $M_{\alpha}$.

Lemma. If $(<_1,<_2,r)$ are a pair of $M'S'$-definable partial orders and an $M'S'$-definable function on the number sort that form a level tree and if $B \subseteq M'$ is a branch of this tree, then $B \in S'$ (in the sense that there is some element of $S'$ with the same members as $B$.

Proof. First note that since this is a level tree, definable initial segments of $B$ are cofinal in $B$ (consider sets of the form $x <_1 a$). For any $M_\alpha$, we can find $b \in B$ such that the rank $r(b)$ is greater than any of the ranks of elements of $M_\alpha \cap B$. This implies that $M_\alpha \cap B = M_\alpha \cap (-\infty, b]$ (since branches are linearly ordered). By one of the above comments, the type of $b$ over $M_\alpha S_\alpha$ is $M_\alpha S_\alpha$-definable. This implies that the set $M_\alpha \cap (-\infty,b]$ (and therefore $M_\alpha \cap B$) is actually definable in $(M_\alpha,S_\alpha)$. Since formulas only use finitely many parameters, this implies that for each limit ordinal $\alpha<\kappa$, there is a strictly smaller ordinal $\beta_\alpha$ such that $M_\alpha \cap B$ is definable in $M_\alpha$ with parameters from $M_{\beta_\alpha} S_{\beta_\alpha}$. By Fodor's lemma, there is a single $\delta <\kappa$ such that $M_\alpha \cap B$ is definable with parameters from $M_\delta S_\delta$ for a stationary (and therefore unbounded) set of $\alpha$'s. By the pigeonhole principle, there must be a single formula $\varphi(x,\bar{b})$ with $\bar{b} \in M_\delta S_\delta$ such that for an unbounded set of $\alpha$'s, $\varphi(M_\alpha, \bar{b}) = M_\alpha\cap B$. Therefore, by elementarity, $\varphi(x,\bar{b})$ actually defines $B$ in $(M',S')$. $\square$

For any formula $\varphi(x,\bar{y})$, we have that for any $\bar{b}$, there is a set $X \in S'$ such that $X = \varphi(M',\bar{b})$. (This is just comprehension.) This implies that given any $\mathcal{L}(Q_{\mathrm{Brch}})$ formula $\psi(\bar{x})$ and any $\bar{a} \in M'$, $M' \models \psi(\bar{a})$ if and only if $(M',S')$ satisfies the internal interpretation of it. Therefore, since no $M'S'$-definable subset of $M'$ is a cut, we have that $M' \models \mathsf{PA}(Q_{\mathrm{Brch}})$. If we start with a model $(M,S)$ of $\mathsf{Z}_2^{SU} + \neg \mathrm{Con}(\mathsf{Z}_2^{SU})$, then we get an $M' \models \mathsf{PA}(Q_{\mathrm{Brch}})$ which does not satisfy true arithmetic, establishing that $\mathcal{L}(Q_{\mathrm{Brch}})$ is $\mathsf{PA}$-intermediate.

I vaguely seem to recall that there is actually a forcing-style reduction of of 'second-order arithmetic + an ultrafilter predicate' to $\mathsf{Z}_2$ which gives a relative consistency argument, but that doesn't seem to be enough to get consistency of $\mathsf{Z}_2^{SU}$ from consistency of $\mathsf{Z}_2$.

Related Question