First-order arithmetic is fairly weak, as measured for example by its consistency strength. When a stronger theory is desired, it is common to work with (fragments of) second-order arithmetic or set theory. However, such theories might fail to meet certain "strong" constructive criteria. (Examples below involve classical theories only because those are the ones I'm aware of.)

For example, the subsystem ACA_{0} of second-order arithmetic is equiconsistent with PA, but its axioms say that for every arithmetic formula there is a well-defined set of numbers which satisfy it, which could be considered to lack a constructive justification. (Here, "well-defined" means roughly that the set consists of a fixed collection of elements, and nothing else, in line with the law of excluded middle.)

Meanwhile, set theories often include an axiom that every set has a well-defined powerset, or at least an axiom asserting the existence of a well-defined set which is "actually" (as opposed to "potentially") infinite. Simply removing such axioms can lead to very weak theories: for instance, ZF - infinity + (not infinity) is bi-interpretable with PA.

On the other hand, the strengths of theories can often be quantified in terms of (notations for) recursive ordinals, and there are notations for some quite large ordinals which arguably satisfy stringent constructive principles; see for example the "ordinal systems" of Anton Setzer, which are "built from below" specifically for this purpose.

There are also theories of arithmetic (e.g. PRA) which, while weak, seem to me like they could be extended using such ordinal notations to considerably greater strength without any features that might be constructively objectionable in the above sense.

My question then is:

Can such ordinal notations indeed be used to bypass the aforementioned obstacles (in second-order arithmetic or set theory) to building "strongly constructive" theories beyond the strength of PA?

Could such theories have practical uses, e.g. in relation to the Curry-Howard correspondence?

Has any work already been done on this?

relevantto their work. And the latter ones will tell you thatrecursion principlesin type theory are the applicable and useful constructive replacement of ordinals. $\endgroup$ – Andrej Bauer Sep 3 '18 at 6:531more comments