Coding in Reverse Mathematics

[Sam Sanders]

Dear All,

The use of coding in Reverse Mathematics (RM) is well-known.  I have gathered some example theorems for which the logical strength changes considerably 
if we change “second-order code for continuous function” to “third-order function that is also continuous”.   I am thinking of e.g. the Heine, Weierstrass, and Tietze 
theorems on separably closed sets, but also more recent results on the Ekeland variational principle.   The problem seems to be that certain second-order codes 
do not give rise to third-order functions in e.g. Kohlenbach’s base theory of higher-order RM, i.e. there are “too many” codes. 

The associated paper is here:

https://arxiv.org/abs/1910.07913

Can anyone think of more theorems of this kind?

Best,

Sam

PS: I should not have to say, but I will, lest I be misunderstood, that the above does not constitute a blanket judgement of coding as being “bad”. 
The only point made is that IF one is interested in the minimal axioms that prove a certain theorem of ordinary mathematics, THEN coding seems
like a bad idea, changing as it does the minimal axioms needed.