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