Suppose T is a theorem of mathematics formalised in the language of second-order arithmetic.
Experience (e.g. Reverse Mathematics) suggests that there is a certain ‘duality’ between the proof theoretic and computability theoretic properties of T, as follows
If T is hard to prove (i.e. requires strong axioms), then T involves objects that are hard to compute, and vice versa.
Are there (natural) examples of exceptions to this duality?