Makoto Fujiwara: Constructive provability versus uniform provability in classical computable mathematics

So-called elementary analysis EL is two-sorted intuitionistic arithmetic, which serves as system to formalize constructive mathematics. In this talk, we show that for any Pi^{^1}_2 formula T of some syntactical form, T is provable in EL if and only of T is uniformly provable in classical variant RCA of EL. It is remarkable that all of our proofs are constructive, namely, they are just explicit syntactic translations. Since a large number of existence theorems are formalized as Pi^{^1}_2 formula T of the form, under the agreement that constructive provability is identical with provability in EL, it suggests the constructive equivalence (from a meta-perspective) between constructive provability and classical uniform provability in RCA for practical existence theorems.