At the very bottom of logical strength, there is the following example.

Julian Hook's PhD thesis under Ed Nelson (available from ProQuest) explores the development of weak arithmetic/analysis assuming the negation of the axiom

the exponentiation function is total on the natural numbers. (*)

Of course, the negation of (*) is consistent with e.g. bounded arithmetic.

I believe people later showed that the same results can be obtained without assuming the negation of (*). This is discussed in Buss' book on Ed Nelson's research, if memory serves.

My experience in reverse math is the same: Dag Normann and I have shown that fairly strong systems are consistent with

there is an injection from the real numbers to the naturals. (**)

However, the axiom (**) does not yield any interesting results/alternative development of math/faster proofs, et cetera, as far as I know.

At the very bottom of logical strength, there is the following example.

Julian Hook's PhD thesis with title A Many-Sorted Approach to Predicative Mathematics, written under the supervision of Ed Nelson (and available from ProQuest) explores the development of weak arithmetic/analysis assuming the negation of the axiom

the exponentiation function is total on the natural numbers. (*)

Of course, the negation of (*) is consistent with e.g. bounded arithmetic.

I believe people later showed that the same results can be obtained without assuming the negation of (*). This is discussed in Buss' book on Ed Nelson's research, if memory serves.

My experience in reverse math is the same: Dag Normann and I have shown that fairly strong systems are consistent with

there is an injection from the real numbers to the naturals. (**)

However, the axiom (**) does not yield any interesting results/alternative development of math/faster proofs, et cetera, as far as I know.