How special is first-order $\mathsf{PA}$?

Question

This is a modified version of a question which was asked and bountied at MSE without success.

---

Below, "$\mathsf{PA}$" refers to first-order Peano arithmetic.

There are various "schematic" theories out there, like $\mathsf{PA}$ and $\mathsf{ZFC}$, which basically consist of three components: a "base" set of axioms which are more-or-less taken for granted (e.g. the discrete nonnegative ordered semiring axioms for $\mathsf{PA}$, and Pairing-Union-Extensionality-Foundation-Powerset-Infinity-Choice for $\mathsf{ZFC}$), an informal idea(s) for a further set of rules indexed by formulas (e.g. induction for $\mathsf{PA}$, and separation/replacement for $\mathsf{ZFC}$), and a choice of logic for implementing the latter (first-order logic for $\mathsf{PA}$ and $\mathsf{ZFC}$, and indeed in general). For any such theory we can hope to produce interesting variants by fixing the first two parts and varying the third - see e.g. here for a question about the case of $\mathsf{ZFC}$.

However, $\mathsf{PA}$ seems remarkably stubborn here: every natural logic (= regular logic possibly without negation) I can think of lands in one of two extremes. To be precise, given a logic $\mathcal{L}$ let $\mathfrak{PA}(\mathcal{L})$ be the class of models of $\mathsf{PA}$ with no $\mathcal{L}$-definable nontrivial proper cuts, and say that $\mathcal{L}$ is:

• strong for induction if $\mathfrak{PA}(\mathcal{L})$ consists of just $\mathbb{N}$ up to isomorphism;

• weak for induction if every complete first-order extension of $\mathsf{PA}$ is satisfied by some element of $\mathfrak{PA}(\mathcal{L})$; and

• intermediate for induction if neither of the above cases holds.

My question is:

Is there any natural logic which is intermediate for induction? (Here, by "natural" I mean "has appeared in at least two different papers whose respective authorsets are $\subseteq$-incomparable.")

In the MSE version I asked for an even stronger property, namely not pinning down $\mathbb{N}$ even up to elementary equivalence, but that seems overly optimistic in retrospect.

---

Here are some quick negative observations:

• Uniformly across models of $\mathsf{PA}$, standardness is definable by a $\Pi^1_1$ formula or by a very simple infinitary formula. So neither $\Pi^1_1$ nor any reasonable infinitary logic will be intermediate for induction; in fact, they'll pin down $\mathbb{N}$ up to isomorphism, not just up to first-order-elementary-equivalence.

• $\Sigma^1_1$ also pins down $\mathbb{N}$ up to isomorphism, although parameters now appear necessary; see here. For the same reason, first-order logic + the equicardinality quantifier pins down $\mathbb{N}$ up to isomorphism.

• On the opposite end of things, $\Delta^1_1$ is weak for induction. (OK, $\Delta^1_1$ may not look like a logic since the $\Delta^1_1$-ness of a $\Sigma^1_1$ formula is structure-dependent, but we can handwave past this: define an abstract logic with a formula $\hat{\varphi}$ for each $\Sigma^1_1$ formula $\varphi$, where $\hat{\varphi}$ is interpreted in $\mathcal{M}$ as $\varphi$ if $\neg\varphi^\mathcal{M}$ is $\Sigma^1_1$ over $\mathcal{M}$ and as $\top$ otherwise.)

• Similarly, $\mathsf{FOL}$ + the quantifier "At least as many $x$ satisfy $\varphi$ as satisfy $\neg\varphi$" is weak for induction, although its model class contains no countable nonstandard models; to see weakness, consider the $\omega_1$-like models of $\mathsf{PA}$.

The most promising approach to me at the moment is to look for fragments of second-order logic between $\Delta^1_1$ and $\Sigma^1_1$, since we see a genuinely interesting and nontrivial change in behavior there. However, I can't at the moment think of a good candidate fragment.

(I've added the set theory tag since, while set theory isn't built into the question a priori, it seems relevant to all the ideas I've had so far.)

Answer 1

This argument has a couple of iffy points, but I believe it does work.

In this paper, Shelah introduced a logic $\mathcal{L}(Q_{\mathrm{Brch}})$ which is fully compact, has the property that any countable theory with infinite models has models of every uncountable cardinality, and is strictly stronger than FOL for countable models. That paper is pretty awful to try to read. There's a slightly better exposition of this logic in this paper of Mekler and Shelah's, but it's still not great. (Technically I have not verified that this logic is natural under your amusingly precise definition of naturalness, but it probably is, and I think you'd probably accept this as an answer anyways.)

To specify the logic, we need some preliminaries. A tuple of formulas (possibly with parameters) $(\varphi_t(x),\varphi_r(x),\psi_t(x,y),\psi_r(x,y),\rho(x,y))$ defines a level tree if

• $\psi_i(x,y)$ defines a partial orded on $\varphi_i(x)$ for $i \in \{t,r\}$, which I will now write as $<_t$ and $<_r$,
• for every $a$ satisfying $\varphi_t$, the set of $<_t$-predecessors of $a$ is linearly ordered by $<_t$,
• $<_r$ is a directed partial order on $\varphi_r$ with no largest element, and
• $\rho(x,y)$ defines a function from $\varphi_t$ to $\varphi_r$ which is strictly order-preserving.

So basically, the idea is that this is the first-order version of a tree with a rank function. (By the way, there seems to be a typo in the published version of this paper. They have $\rho$ as a formula with three variables. There's also what seems to be an incorrect statement in the remark after Subclaim 3.6: They say that every countable level tree has a branch (which I will define in a second, but you can guess what it means). This seems to contradict the existence of countable well-founded trees.)

A branch of a level tree is a maximal linearly ordered subset of $\varphi_t$ whose image under $\rho$ is unbounded in $\varphi_r$. The logic $\mathcal{L}(Q_{\mathrm{Brch}})$ allows monadic second order variables and has this quantifier $$Q_{\mathrm{Brch}}b(\varphi_t(x),\varphi_r(x),\psi_t(x,y),\psi_r(x,y),\rho(x,y))\Theta(b),$$ which is interpreted as saying that if $(\varphi_t(x),\varphi_r(x),\psi_t(x,y),\psi_r(x,y),\rho(x,y))$ defines a level tree, then there is a branch $b$ of the level tree such that $\Theta(b)$ holds (and $\Theta(b)$ is any $\mathcal{L}(Q_{\mathrm{Brch}})$-formula). We are allowed to freely form formulas using this quantifier and standard quantifiers and connectives.

I'll call the version of $\mathsf{PA}$ that has induction for $\mathcal{L}(Q_{\mathrm{Brch}})$-formulas, $\mathsf{PA}(Q_{\mathrm{Brch}})$. By full compactness, we immediately get that $\mathsf{PA}(Q_{\mathrm{Brch}})$ has models other than $\mathbb{N}$. (Although, I do not know whether it has any non-standard countable models.)

Now we come to the point where if I knew more computability theory or reverse mathematics, I could probably have done this proof in a shorter way.

Proposition. $\mathsf{PA}(Q_{\mathrm{Brch}})\vdash \mathrm{Con}(\mathsf{PA})$, so in particular $\mathcal{L}(Q_{\mathrm{Brch}})$ is intermediate for induction.

Proof. I will prove this by showing that if $M \models \mathsf{PA}(Q_{\mathrm{Brch}})$, then $(M,\mathrm{Def}(M,\mathcal{L}(Q_{\mathrm{Brch})}))$ is a model of $\mathsf{ATR}_0$, where $\mathrm{Def}(M,\mathcal{L}(Q_{\mathrm{Brch}}))$ is the collection of all $\mathcal{L}(Q_{\mathrm{Brch}})$-definable-with-parameters subsets of $M$. I will call the induced second-order structure $M_2$ to avoid having to type that out again. Since models of $\mathsf{ATR}_0$ always satisfy $\mathrm{Con}(\mathsf{PA})$, the result clearly follows.

First note that it's pretty easy to see that $M_2$ is a model of $\mathsf{RCA}_0$. (More than this is also easy, but this is enough.) Now we will use the fact that $\mathsf{ATR}_0$ is equivalent to the comparability of any two well-orderings (over $\mathsf{RCA}_0$).

Claim 1. If $T$ is an $\mathcal{L}(Q_{\mathrm{Brch}})$-definable tree in $M^{<M}$ (i.e., $M$'s version of $\omega^{<\omega}$) with a branch, then it has an $\mathcal{L}(Q_{\mathrm{Brch}})$-definable branch.

Proof of claim 1. We can define a branch inductively. For each $n$, given $\sigma \in T$ of length $n$, with the property that there exists a branch in $T$ extending $\sigma$, find the smallest $m$ such that there exists a branch in $T$ extending $\sigma \frown m$. Having such a branch is an $\mathcal{L}(Q_{\mathrm{Brch}})$-definable property, so a smallest such $m$ must exist and by induction we can build a path this way. This branch is definable since a $\sigma$ is an initial segment of it if and only if every initial segment of it satisfies this inductive definition. $\square_{\text{claim 1}}$

Claim 2. If $\varphi(x,y)$ is an $\mathcal{L}(Q_{\mathrm{Brch}})$-formula (possibly with parameters) that defines an internal well-ordering on $M$ (in the sense that the tree of internally finite descending sequences in $M$ has no branch), then for any $\mathcal{L}(Q_{\mathrm{Brch}})$-formula $\psi(x)$ (possibly with parameters), either $\psi(x)$ does not hold for any elements of $M$ or there is a $\varphi$-least element of $M$ satisfying $\psi(x)$.

Proof of claim 2. We will prove the contrapositive. Assume that $\varphi(x,y)$ defines a linear order on $M$ and suppose that $\psi(x)$ is a formula that defines a non-empty set with no $\varphi$-least element. Then we can inductively build a descending sequence by choosing the $<$-least element that is $\varphi$-less than whatever we have chosen so far, where $<$ is the standard order on $M$. $\square_{\text{claim 2}}$

Now fix two formulas (possibly with parameters) $\varphi(x,y)$ and $\psi(x,y)$ which define internal well-orderings (i.e., linear orders with no definable-with-parameters infinite descending sequences). For notational simplicity, call the linear orders defined by $\varphi(x,y)$ and $\psi(x,y)$, $(A,<)$ and $(B,<)$. (They both have universe $M$, but it's easier to state things this way.)

Let $T$ be the tree of all (internally) finite strictly order-preserving maps from $(A,<)$ to $(B,<)$. Let $\chi(x,y)$ be a formula (which we're thinking of as a relation between $A$ and $B$) that holds if and only if there exists a branch on $T$ whose domain is an initial segment of $A$ and whose range is an initial segment of $B$ and which maps $x$ to $y$.

Claim 3. $\chi(x,y)$ is a maximal order isomorphism between initial segments of $A$ and $B$. That is to say, it is either an isomorphism between $A$ and $B$, a mapping of $A$ onto an initial segment of $B$, or the inverse of a mapping of $B$ onto an initial segment of $A$.

Proof of claim 3. (This is pretty much the standard argument for the comparability of well-orders. Mostly we're just checking that it all goes through in $\mathsf{PA}(Q_{\mathrm{Brch}})$.) First note that $\chi(x,y)$ must be a one-to-one relation. If there were some $a\in A$ and $b_0,b_1 \in B$ such that $\chi(a,b_0)$ and $\chi(a,b_1)$ both hold, then by composing some maps we'd get a definable strictly order-preserving map of an initial segment of $B$ onto a smaller initial segment $B$, whence we could get a definable infinite descending sequence of elements of $B$. (Take the first element of $B$ not in the range of this map and iterate, which we can do by Claim 2.) Also it's fairly clear that $\chi(x,y)$ must actually be a bijection between initial segments of $A$ and $B$. Assume that the domain of $\chi(x,y)$ is not all of $A$ and the range of $\chi(x,y)$ is not all of $B$. By Claim 2, there is a smallest $a \in A$ not in the domain of $\chi(x,y)$ and a smallest $b \in B$ not in the range of $\chi(x,y)$, so we can build a branch in $T$ witnessing a bijection extending $\chi(x,y)$ to $a$ and $b$, which is a contradiction. $\square_{\text{claim 3}}$.

So since we can do this for any two definable internal well-orderings in $M$, we have that well-orderings are comparable in $M_2$, so since it satisfies $\mathrm{RCA}_0$, it is a model of $\mathrm{ATR}_0$. Therefore every model of $\mathsf{PA}(Q_{\mathrm{Brch}})$ satisfies $\mathrm{Con}(\mathsf{PA})$. $\square$

Answer 2

There are several notable papers, starting with a key paper of Angus Macintyre (Ramsey quantifiers in arithmetic, Model theory of algebra and arithmetic, Lecture Notes in Math., 834, Springer, 1980), which explore natural extensions of Peano Arithmetic formulated in "well-behaved" logics extending first order logic. The most well-known of these extensions are obtained by adding the so-called Ramsey quantifiers $Q^{n}$ (where $n\in \omega,~n>0$) to first order logic; these quantifiers are also known as Magidor-Malitz quantifiers.

The extension of PA formulated using Ramsey quantifiers is usually referred to as $PA(Q^{<\omega})$. Given a model $\mathcal{M}$ of PA, the semantics of $Q^{n}$ is guided by:

$\mathcal{M}\models Q^{n}x_1,...,x_n~ \varphi(x_1,...,x_n)$ iff there is an unbounded subset $H$ of $\mathcal{M}$ such that $\mathcal{M}\models \varphi(h_1,...,h_n)$ for every increasing sequence $h_1,...,h_n$ from $H$.

Macintyre proved various interesting results in his paper, including a completeness theorem (with the help of the combinatorial principle $\diamond_{\omega_1}$). This allowed him to show that $PA(Q^{<\omega})$ has an $\omega_1$-like model (an uncountable model every proper initial segment of which is countable). As also noted by Macintyre, the Paris-Harrington extension of the finite form of Ramsey's theorem is provable in $PA(Q^{<\omega})$, thus the 1-consistency of PA is provable in $PA(Q^{<\omega})$ [indeed proving the Paris-Harrington principle in a natural extension of PA is what led Macintyre to introduce $PA(Q^{<\omega})$].

Schmerl and Simpson refined Macintyre's work by eliminating the need for $\diamond_{\omega_1}$ in the results of Macintyre in the aforementioned paper (On the role of Ramsey quantifiers in first order arithmetic, Journal of Symbolic Logic, Vol.47, 1982). Their refinement allowed them to calibrate the arithmetical strength of $PA(Q^{<\omega})$ by proving the following theorem:

Theorem (Schmerl and Simpson). The following statements are equivalent for an arithmetical statement $\varphi$:

(a) $PA(Q^{<\omega}) \vdash \varphi$.

(b) $PA(Q^{2}) \vdash \varphi$.

(c) $\Pi^1_1-\mathrm{CA_0} \vdash \varphi$.

In a later paper by Schmerl, entitled PA(aa), in Notre Dame Journal of Formal Logic, Vol. 36, 1982, Schmerl studied the extension of PA with stationary quantifiers (originally introduced and studied in a landmark 1978 paper of Barwise, Kaufmann, and Mekler) and established that the purely arithmetical consequences of PA(aa) + Det [where Det is the so-called scheme of finite determinateness of stationary logic] coincides with the purely arithmetical consequences of second order arithmetic $Z_2$ (the first order theory whose subsystems are studied in reverse mathematics, as opposed to PA formulated in full second logic, which is a much stronger theory which only has one model up to isomorphism).

Another important paper of Schmerl (Peano arithmetic and hyper-Ramsey logic, Trans. Amer. Math. Soc., 1986) connects PA formulated in so-called hyper-Ramsey logic with subsystems of second order arithmetic.