Two systems in which the successor operation is altered are Sazonov's arithmetic over a finite row, in "A logical approach to the problem 'P=NP?'" http://www.csc.liv.ac.uk/~sazonov/papers.html and Boucher's "Arithmetic without the Successor Axiom", http://www.andrewboucher.com/papers/.
In Sazonov's system, there is a total successor operation that is explicitly assumed to stop at the last number $\square+1 = \square$, whereas in Boucher's system the successor relation is just not assumed to be total.
Then there are ways to designate numbers up to $2^\square$ via binary strings or second-order variables. Because of course even though we can't feasibly reach, say, $2^{1000}$ starting from zero and repeatedly adding one, computers manipulate binary representations of numbers of that order and larger all the time, and we should be able to prove theorems about these representations.
But if you don't like restrictions on induction, there's a problem. With unrestricted induction even up to $\square$, it seems we just define a second-order zero and successor, and derive unrestricted induction up to $2^\square$. Now if, from $P(0)$ and $\forall n . P(n) \to P(n+1)$, you conclude, $P(2^{1000})$, then you're admitting that, in principle, you can reach $2^{1000}$ from zero by repeatedly adding one.
Which lets me segue to an idea that I had. Caveat lector.
Start with cyclic induction: if $\exists n. P(n)$ and $\forall n . P(n) \to P(S(n))$ then $\forall n. P(n)$. If $X$ and $Y$ are types with unrestricted cyclic induction, then $X^Y$ (the type of all functions from $Y$ to $X$) has unrestricted cyclic induction. And of course unrestricted cyclic induction is valid for a two-element domain. So this suggests the theory of finite-order types over 2 (something like $\mathbf{HA}^\omega$, the constructive theory of finite-order types over $\mathbb{N}$.)
One way this may be of interest is that, as Theo Johnson-Freyd mentions, computers generally work with a cyclic domain like $2^{32} = (2^{2^{2^2}})^2$. They can also work with larger integer size. And in fact there are "big integer" implementations which are sometimes said to work with arbitrary integers. And I notice someone claims above that the C programming model has infinite memory! But that's sort of an insult to $\mathbb{N}$. If they are implemented with, say, 32-bit pointers, then your big integer type really has a size approximately $2^{2^{32}}$ - even if your computer has more than 4GB of memory you can't use it. Taking this even further, if you can imagine a computer with a truly vast address space, which has to be accessed using "big pointers" made from small 32-bit pointers, and then defining "really big integers" over that, well, that's still just a finite type of something like $2^{2^{2^{32}}}$.
From the other side, you can accept a truly arbitrary integer with an interactive spefication, but you're really dealing with something like the one-point compactification of $\mathbb{N}$. There doesn't seem to be a way to express the specification that the input stream must terminate "eventually" without cutting it off at a large but finite bound, or circularly referring to $\mathbb{N}$.
Another way this may be of interest is that instead of talking of the "finite" types over 2 in terms of a meta-theory involving $\mathbb{N}$, we can then use it as its own meta-theory, so we're dealing with a large but finite set of formulas. That should be a viable proof theory.
Of course this alternative arithmetic may suit a finitist, but you're an ultrafinitist and this is not what you really want. I think what you really want doesn't exist: as I've ranted elsewhere it seems we need induction up to infeasible numbers to prove theorems about feasible computations.
