Interesting examples of first-order, one-sorted proper extensions of PA Are there any interesting nontrivial examples of first-order, one-sorted theories of natural numbers (i.e. theories whose quantifiers range over natural numbers only and not, say, sets of natural numbers) that are stronger than first-order Peano arithmetic (PA)?
PA is usually strengthened by introducing sets of natural numbers (e.g. second-order arithmetic and its subsystems) or working with sets of sets (e.g. various set theories).
Simply adding lengthy, complex Diophantine equations that express the consistency of PA or stronger theories is an example of what I'm not looking for, since it fails the interestingness criterion and is aesthetically ad-hoc from an axiomatic standpoint.
 A: There are now several examples known of interesting arithmetical sentences independent of $\mathsf{PA}$ (e.g. Paris-Harrington), and any of these - when added to $\mathsf{PA}$ as an axiom - gives of course a proper strengthening of $\mathsf{PA}$ in the same language. However, even if we're totally convinced of the interestingness of such axioms, the fact remains that such extensions may feel ad hoc.
Another approach we could take is to take an existing theory $T$ of interest in a richer language, and look at the theory $T'$ consisting of $T$'s arithmetical consequences. For example, the set of arithmetical consequences of $\mathsf{ZFC}$ is a computably axiomatizable first-order theory in the language of arithmetic which properly extends $\mathsf{PA}$. However, this may still feel like a cheat; moreover, we often lack a good way to describe the resulting $T'$ "on its own terms" (e.g. see here).
Ultimately, it's difficult to get away from the conclusion that $\mathsf{PA}$ is a fairly natural "stopping point." I find this fascinating, and am interested in any results supporting or attacking this (admittedly extremely informal) idea. For now, the only thing that comes to mind is, interestingly enough, a positive result - that is, attacking the idea of $\mathsf{PA}$-uniqueness - which came as a surprise to me: we can produce proper first-order extensions of $\mathsf{PA}$ in the language of arithmetic using the same "core idea" that motivated $\mathsf{PA}$ itself by bringing strong-but-not-too-strong natural logics into play.
Specifically, suppose I have a logic $\mathcal{L}$ (e.g. first-order logic, second-order logic, etc.). We can define a first-order theory $\mathsf{PA}[\mathcal{L}]$ as follows: it consists of all first-order consequences of the $\mathcal{L}$-theory gotten from $\mathsf{PA}$ by extending the induction scheme to range over $\mathcal{L}$-formulas. Note that although we're going through a non-first-order logic $\mathcal{L}$, we do wind up with a first-order theory in the end: $\mathsf{PA}[\mathcal{L}]$ is the "first-order part" of an $\mathcal{L}$-theory.
A quick perusal of the abstract model theory literature may suggest - or at least it suggested to me at one point - that the situation is uninteresting: that for every "natural" logic $\mathcal{L}$ extending first-order logic, we either have $\mathsf{PA}[\mathcal{L}]=\mathsf{PA}$ or $\mathsf{PA}[\mathcal{L}]=Th(\mathbb{N})$. However, this turns out not to be the case as the answers to this MathOverflow question of mine showed.
Of particular note is what I'll call $\mathsf{PA}[\mathit{Ramsey}]$; this is what we get when we apply the above idea to the extension of $\mathsf{FOL}$ gotten by adding Ramsey (or Magidor-Malitz) quantifiers. The resulting theory turns out to be ... precisely the arithmetical fragment of the first-order theory $\Pi^1_1$-$\mathsf{CA_0}$! So not only do we have a proper first-order strengthening of $\mathsf{PA}$ in the same language which is computably axiomatizable and motivated by a coherent "core idea" (the same as $\mathsf{PA}$ itself, together with the basic motivation for generalized quantifiers), but we also have a connection with an existing theory of interest in a different setting. And this in turn should make us more interested in the $T\leadsto T'$-construction I dismissed a few paragraphs prior:

Maybe the arithmetical parts of strong first-order theories correspond, at least sometimes, to "$\mathsf{PA}$-analogues" for logics extending $\mathsf{FOL}$.

