Dedekind-Peano axioms, but numbers have at most one successor One can consider a variant of the Dedekind-Peano axioms
in which one replaces the assumption that every number
has exactly one successor by the assumption that every
number has at most one successor, leaving the other
axioms the same (and in particular retaining the
second-order induction axiom). The models of this theory
are then the initial segments of the natural numbers.
Call it a "size-neutral" version of the second-order
Dedekind-Peano theory.  My question is, to what extent
can one prove analogues of standard theorems about the
natural numbers in this theory?
For instance, what would serve as a size-neutral analogue
of the proposition that the set of primes is infinite?  Ideally it would be some proposition P with the property that if
you assume that P is true, and you assume that every
number has a successor, then the standard claim about
the set of primes being infinite would follow without
too much trouble (where "too much trouble" means "going back to the beginning and proving the infinitude of the primes in the usual way without invoking P at all").
I'm aware that even defining "prime" is problematic.
To begin with, in a size-neutral theory, one cannot
define addition or multiplication in the usual recursive
way, or rather, if one does, the operations are not
provably total; if one's model cuts off at n, then
sums and products that exceed this bound are undefined.
One could choose to remedy this with a definition that
basically says "If a number has no successor, define it
to be its own successor; now proceed using this new,
enlarged notion of succession instead of the old one",
and then sums and products that in ordinary arithmetic
exceed n would now equal n -- though I'm not sure this is
a good way to go.
This can't be a new line of thought, so I'd be happy
with answers of the form "Go read X".
 A: As pointed out by Emil Jeřábek (in the comment to Joel Hamkins' answer), the system you are referring to is known as "Peano Arithmetic with a top". It has been studied for several decades. A good place to learn about it is the chapter written by Lawrence (Tin Lok) Wong, as part of his lecture notes for a course on models of arithmetic, available here.
Wong's chapter also includes the proof of the theorem (mentioned in Hamkins' answer) that connects models of this theory with models of $\mathrm{I}\Delta_0$, and credits this result to Jeff Paris (see Theorem 13.11 of the chapter).
A: Victoria Gitman and I recently looked at the first-order version of this theory, which we called fPA, to contrast it with the theory FPA, which Woodin has looked into, which is a possibly stronger version.
[Update As explained by Emil Jeřábek in the comments below and in Ali Enayat's answer, this theory has been well studied in models of arithmetic and is known as $\text{PA}^{\text{top}}$. The observations below about $I\Delta_0$ are evidently due originally to Jeff Paris.]
So the language of fPA is the same as the ordinary language of arithmetic, except that there is possibly a largest number (without a successor), and the operations of + and $\cdot$ are merely partial, but defined as far as they can be according to the usual recursive definitions. Meanwhile, we have the first-order induction scheme.
The main observation we made is that if you have a model of fPA with a largest number $N$, then there is some largest number $m$ whose square exists $m^2\leq N$, and using this number, we can interpret a larger model of fPA. Simply use quadruples of numbers $abcd$ to represent larger numbers in base $m$. We know how to add and multiply such numbers in that representation, and this requires only arithmetic for numbers less than $m$, which works fine. Using this method, we can build a larger model of fPA in which $N^2$ exists. Basically, every model of fPA interprets a larger model of fPA, in which any two numbers from the original model now have a product.
Answer to your question. The main point I want to make is that the base $m$ method provides a means to express primality etc. also in your context. Since the interpreted model is definable in the original model using quadruples, we can express those notions entirely in the original model simply by using the base $m$ representation. Any concept that could be expressed in the context of the larger models can also be expressed in the original model.
Iterating. The further observation is that we can simply iterate the interpretation construction $\omega$ many times, interpreting to larger and larger models of fPA. The union model is a model of $I\Delta_0$, since bounded induction amounts to unbounded induction in the individual models.
Conclusion. The models of fPA with a largest number all arise by chopping a model of $I\Delta_0$ at some number $N$.
For this reason, questions about what is or what is not provable in fPA amount to the corresponding questions about $I\Delta_0$, which is an intensely studied theory and there are many open questions.
FPA. Woodin had looked into the first-order theory FPA in which one adopts the pigeon-hole principle as a fundamental axiom scheme, rather than just the first-order induction scheme. PHP implies the induction scheme, but it is open whether they are equivalent.
A: I've looked at the system you've mentioned, where you assume these as mathematical axioms:
(1) Uniqueness of successoring
(2) Uniqueness of predecessoring
(3) 0 doesn't have a predecessor
(4) Induction
As Emil Jeřábek pointed out to me, the system has connections to certain well-known systems of weak arithmetics. (See the first MathOverflow question linked to below.)
In second-order logic, where one has access to predicates and relationships, there is no problem to define addition and multiplication relationships, although as you point out they will not be total. There is no problem in defining primality, as LSpice points out in comments.
In this system you can prove Quadratic Reciprocity and Bertand's Postulate and I imagine - although I have not checked in detail - the Prime Number Theorem.  You might want to check these out:
https://www.researchgate.net/publication/351561089_Arithmetic_Without_the_Successor_Axiom
https://www.researchgate.net/publication/352796035_Proving_Bertrand's_Postulate
This paper looks at what happens when you assume even less:
https://www.researchgate.net/publication/352795952_General_Arithmetic
Variants of this system have appeared in these MathOverflow questions:
Provability in Second-Order Arithmetic without the Successor Axiom
Can FPA really prove its consistency?
Is an ultrafinitist Hilbert's program doomed?
When we count the same set, must the number always be the same?
Can this weakish system of arithmetic express multiplication for second-sort numbers?
