2 more examples

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$.)

• 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$.