I think we're heading towards an era where "ordinary" mathematics includes logic, at least the parts of it that can be described as applied mathematics (used in practical problems of the real world). For example, the ML programming language is based on polymorphic lambda calculus. I'm no expert but I have the impression that the proof that polymorphic lambda calculus is strongly normalizing is equivalent to second order arithmetic. There are fancier languages based in even more powerful (?) theories, like Coq implements Martin-Lof type theory more or less directly. I'm just a programmer trying to learn these languages but people disigning them and writing compilers for them (e.g. implementing type inference) seem to me to often be up to their elbows in proof theory. I saw a thesis by someone about ordinal analysis of programs (after all, by the Curry-Howard correspondence, programs are proofs..). I wondered if software engineers (at least those in high-assurance programming) will someday use proof-theoretic ordinals in their daily work just like electrical engineers now use complex numbers.

In complexity theory, there are some proofs that P vs NP is independent of some sizeable fragments of PA, but maybe those fragments are weaker than EFA.

I think we're heading towards an era where "ordinary" mathematics includes logic, at least the parts of it that can be described as applied mathematics (used in practical problems of the real world). For example, the ML programming language is based on polymorphic lambda calculus. I'm no expert but I have the impression that the proof that polymorphic lambda calculus is strongly normalizing is equivalent to second order arithmetic. There are fancier languages based in even more powerful (?) theories, like Coq implements Martin-Löf type theory more or less directly. I'm just a programmer trying to learn these languages but people disigning them and writing compilers for them (e.g. implementing type inference) seem to me to often be up to their elbows in proof theory. I saw a thesis by someone about ordinal analysis of programs (after all, by the Curry–Howard correspondence, programs are proofs…). I wondered if software engineers (at least those in high-assurance programming) will someday use proof-theoretic ordinals in their daily work just like electrical engineers now use complex numbers.

In complexity theory, there are some proofs that P vs NP is independent of some sizeable fragments of PA, but maybe those fragments are weaker than EFA.