
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 manysorted firstorder theory, not just proper secondorder 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 “firstorder” 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 “secondorder” 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_{n1}\rangle\in[0,a)^n:M\models\mathrm{bit}(r,a^{n1}u_{n1}+\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 (secondorder) 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 bitcomprehension 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 firstorder induction; this firstorder theory is called $\mathrm{PA^{top}}$, and it is wellknown 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 secondorder 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 secondorder 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 “secondorder” models of arithmetic with bounded sets to “firstorder” models with exponentially larger numbers is known as the RSUV isomorphism.)
This gives a characterization of provability in FPA: for any (secondorder) sentence $\phi$, the construction above implicitly gives a firstorder 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 nontotal 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 fixpointfree 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$.)


answered Jan 28 '13 at 13:20

