Provability in Second-Order Arithmetic without the Successor Axiom

Question

Consider second-order Peano Arithmetic Z2, i.e. the two-sorted first-order theory with induction and comprehension. Remove the assumption about the totality of the successor relationship (the Successor Axiom), i.e. the assumption that every number is successored by a number. Call this theory FPA. FPA has as models the standard model (if it exists) and all the initial segments. FPA is "downward": if a natural number exists, it can prove all numbers less than that number exists, but none that are greater. So it cannot prove the infinity of the primes, but then this assertion isn't even true in all its models, e.g. {0,1,2,3} has two primes, and 2 is a member of the set, so the set of primes is finite in this model. FPA can, however, prove Bertrand's Postulate.

Are there any simple mathematical examples of assertions true in all models of FPA, provable in Z2, but not provable in FPA?

EDIT: On François' advice, I am adding here some clarifications which appear in comments.

Full comprehension is used.

Successoring is considered to be a 2-ary relationship, addition and multiplication to be 3-ary relationships. The usual axioms can be easily restated in these terms.

The logic is supposed to include variable n-ary relationships, for n = 1 but also for n > 1, which can be quantified over and whose existence can be proved using comprehension. So for instance, FPA is able to define size equivalence in the straightfoward fashion: A ~ B if and only if (there exists R)(R is a 1-1 function from A onto B). (In fact, given this apparatus, addition and multiplication can be defined from successoring, so one doesn't even need axioms about addition and multiplication, although this is a detail which should not affect the question asked.)

Induction can be considered to be: (P)(P0 & (n)(m)(Pn & Nn & Sn,m => Pm) => (n)(Nn => Pn)), where "N" is "is natural number" and "S" is successoring.

There are many ways to assert the infinity of primes. One way would be to define "a < b" as

(there exists x)(x > 0 & +(a,x,b)) and

"MP,n" (P has size n) as

P ~ {x : x < n}. Then

(not there exists n)(Nn & M{p : p is prime},n)

asserts the infinity of primes. Or one can state in via unboundedness: (n)(Nn => (there exists p)(p > n and p is prime)).

Answer 1

As I already mentioned in another thread for a slightly different theory, it is possible to give a complete description of models of FPA (I mean all models, giving a complete semantics for the many-sorted first-order theory, not just proper second-order models, which abo lists in the question and which I will henceforth call “standard”) in terms of more familiar theories:

• Models where successor is total are exactly the models of $Z_2$.

• Models where successor is not total. If $M\models I\Delta_0+\Omega_1$ and $0< a\in M$ is such that $M\models{}$ “$2^a$ exists”, we can form the following model $A_{M,a}$: its “first-order” sort consists of the submodel $[0,a)_M$ of $M$ (where successor, addition, and multiplication are considered as relations, not functions), and for every $n$, its “second-order” universe of $n$ary relations consists of $[0,2^{a^n})_M$, where $r< 2^{a^n}$ represents the relation $$\{\langle u_0,\dots,u_{n-1}\rangle\in[0,a)^n:M\models\mathrm{bit}(r,a^{n-1}u_{n-1}+\dots+au_1+u_0)=1\},$$ where $\mathrm{bit}(x,u)$ is the $u$th bit in the binary representation of $x$. (Note that the existence of $2^a$ implies the existence of $2^{a^n}$ by $\Omega_1$.) Then $A_{M,a}\models\mathrm{FPA}$: the main thing is that the validity of any (second-order) formula in $A_{M,a}$ translates to a formula in $M$ whose all quantifiers are bounded by some $2^{a^n}$, and $I\Delta_0+\Omega_1$ proves bit-comprehension for $\Delta_0$-definable subsets of logarithmically small intervals, which implies full comprehension in $A_{M,a}$.

  Conversely, every model $A\models\mathrm{FPA}$ where successor is not total is isomorphic to $A_{M,a}$ for some $M,a$ as above. I will sketch the argument below. FPA proves that $A$ has a largest element, and satisfies full first-order induction; this first-order theory is called $\mathrm{PA^{top}}$, and it is well-known that every its model $A$ can be extended into a model $B$ of $I\Delta_0$ so that $A$ is its submodel of the form $[0,a)$, and the standard powers $\{a^n:n\in\omega\}$ are cofinal in $B$ (unless $a=1$). The construction works as follows: for every $n$, elements of the interval $[0,a^n)$ in $B$ can be represented by $n$tuples of elements of $A$; one can define in $\mathrm{PA^{top}}$ the arithmetic operations on such $n$tuples in such a way that these $[0,a^n)$ form an increasing chain of models whose union is taken as $B$. In our case, we also have the second-order universes of $n$-ary relations, and these can be used to represent exponentially larger numbers: an $n$-ary relation from $A$ (i.e., a subset of $[0,a^n)$) will represent a number below $2^{a^n}$ in binary. In this way, we can extend $B$ into a model $M$ such that $B=\{x\in M:M\models2^x\text{ exists}\}$. Since any bounded formula in $M$ translates into a second-order formula in $A$, $M$ will satisfy $\Delta_0$ induction up to logarithmically small numbers (this is called length induction), which implies $I\Delta_0$. $M\models\Omega_1$ follow from the fact that $\{2^{a^n}:n\in\omega\}$ is cofinal in $M$. By the construction, $A\simeq A_{M,a}$.

  (The second part of the argument, viz. a correspondence of “second-order” models of arithmetic with bounded sets to “first-order” models with exponentially larger numbers is known as the RSUV isomorphism.)

This gives a characterization of provability in FPA: for any (second-order) sentence $\phi$, the construction above implicitly gives a first-order formula $\phi^*$ such that

$\mathrm{FPA}\vdash\phi$ iff $Z_2\vdash\phi$ and $I\Delta_0+\Omega_1\vdash\phi^*$.

Note that $\phi^*$ is a $\Pi^0_1$-sentence; conversely, every $\Pi^0_1$-sentence is equivalent to one of this form. Note that the standard models of FPA with non-total successor are $A_{\mathbb N,n}$ for some $n\in\mathbb N$, hence the question reduces to: find sentence $\phi$ such that $Z_2\vdash\phi$, $\mathbb N\models\phi^*$, but $I\Delta_0+\Omega_1\nvdash\phi^*$.

An example of such a statement is $\mathrm{Con}_Q$ (the formal consistency of Robinson arithmetic), formulated as a $\Pi^0_1$-formula of the form $\forall x\,\theta(x)$, where $\theta(x)$ is a formula whose all quantifiers are bounded to $x$, and atomic formulas are reformulated in such a way that they do not refer to any numbers above $x$. The translation $\phi^*$ is then essentially equivalent to $\forall x\,\theta(|x|)$, where $|x|$ is the length function, that is, the statement that $Q$ has no logarithmically short proofs of contradiction. This is not provable in $I\Delta_0+\Omega_1$. Thus, $\mathrm{Con}_Q$ is not provable in FPA, but it holds in all its standard models, and it is provable in $Z_2$.

Independent $\Pi^0_1$ statements (for weak or strong arithmetic) in the literature are mostly variants of consistency statements. While this is not a precise question, it is a sort of an open problem to find natural combinatorial $\Pi^0_1$ statements independent of particular fragments of arithmetic. Let me mention two principles which are conjectured to be unprovable in $I\Delta_0+\Omega_1$, and therefore would give the wanted example for FPA:

• $\Delta_0$-$\mathrm{PHP}$: the pigeonhole principle. In the language of FPA, it is the following schema: for every formula $\phi(u,X,Y)$ (possibly with other parameters not shown), $$\begin{align}\forall u\,\neg[&\forall X\subseteq[0,u]\,\exists Y\subsetneq[0,u]\,\phi(u,X,Y)\\&{}\land\forall X_0,X_1,Y\subseteq[0,u]\,\neg(\phi(u,X_0,Y)\land\phi(u,X_1,Y))].\end{align}$$ (I.e., $\phi$ does not define an injective (multi-)function from $\mathcal P([0,u])$ into itself minus one set.)

• $\mathrm{Count}_2(\Delta_0)$: the counting principle modulo $2$. In the language of FPA, it is the schema $$\begin{align}\forall u\,\neg[&\forall X\subsetneq[0,u]\,\exists!Y\subsetneq[0,u]\,\phi(u,X,Y)\\&{}\land\forall X,Y\subsetneq[0,u]\,(\phi(u,X,Y)\to X\ne Y\land\phi(u,Y,X))]\end{align}$$ for every formula $\phi(u,X,Y)$. (I.e., $\phi$ does not define a fixpoint-free involution on $\mathcal P([0,u])$ minus one set. In general, the mod $k$ counting principle would state that some canonical class of finite cardinality not divisible by $k$ cannot be partitioned into $k$-element subclasses, but it’s easier to state it just for $k=2$.)

Answer 2

Since FPA is a first-order theory, from the completeness theorem, if something is true in all its models, then it is provable in the theory. That can't really be what you're asking.

Answer 3

This is not an answer, just an attempt at explicitly writing down my interpretation of the question. Too long for a comment.

Z2 and FPA are many-sorted FIRST ORDER theories, with one "lowercase" sort (for numbers) and infinitely many "uppercase" sorts (the n-th sort is for n-ary relations. There are predicates $Succ(x,y)$, $Add(x,y,z)$, $Mult(x,y,z)$ and $Element_n(x_1,\ldots, x_n,Y)$ (one for each $n$). However, we write $S(x)\sim y$ instead of $Succ(x,y)$; similarly $x+y\sim z$ instead of $Add(x,y,z)$, etc. Also we write $Y(x_1,\ldots, x_n)$ instead of $Element_n(x_1,\ldots, x_n,y)$. There is also a relation $\le$.

There are several groups of axioms. The first group says that successor, addition and multiplication are partial functions. The second group says that they satisfy the usual properties from Peano arithmetic whenever defined, e.g.

• if $x+y\sim z$ and $S(z)\sim z'$ and $S(y)\sim y'$, then $x+y'\sim z'$.

I am not sure about the axioms for $\le$: Perhaps $0\le x$, and $S(y)\sim y' \to (x\le y' \leftrightarrow x\le y \vee x=y')$? Perhaps an axiom demanding that $\le$ is a total order? A discrete total order? (Feel free to edit.) And: "the domain of $S$ is downward closed".

In addition, Z2 (but not FPA) says that all functions are total.

The third group are the comprehension axioms: For every formula $\varphi(x_1,\ldots, x_n,\bar p)$ (where the parameters $\bar p$ may use come from all sorts), the universal quantification of $$\exists Y \ \forall x_1,\ldots, x_n \ [ Y(x_1,\ldots, x_n) \leftrightarrow \varphi(x_1,\ldots, x_n,\bar p)]$$

The fourth group is the induction axiom: $$ \forall Z: \quad [Z(0)\wedge \forall x \forall y\ ((Z(x)\wedge S(x)\sim y )\to Z(y))]\quad \to \quad \forall x \ Z(x) $$

The question is (correct me if I am wrong):

Assume that $\varphi$ is a formula (using any sorts) which is first order provable from Z2, and true in all standard models of FPA. Is $\varphi$ then first order provable from FPA?

(The standard models of FPA are: the natural numbers, and all truncated models. In all standard models, the uppercase sorts are interpreted as the respective power sets.)