Reverse Mathematics (RM for short) generally takes place in the language of second-order arithmetic. Thus, higher-order objects need to be "coded" or "represented" indirectly. The coding of third-order continuous functions as (what amounts to) second-order Kleene associates is well-known (see [9, II.6.1]). I am interested in the second-order coding of fourth-order mappings. I have found the following examples and am looking for more.
a) Functional analysis in RM involves mappings on e.g. $C ([0, 1])$ and other separable Banach spaces (see [1-3,9]). These are (the most) explicit examples of second-order codes for fourth-order objects.
b) Mummert-Simpson’s study of the RM of topology involves (codes for) homeomorphisms between (coded) spaces (see [6–8]); instances of these would be codes for fourth-order or higher objects.
c) The notion of ‘effectively finding’ as in e.g. [9, II.7] or [4] amounts to a second-order representation of a fourth-order mapping on second-order representations of third-order continuous functions or similar objects.
d) Notions like locatedness are fourth-order in nature; in the associated second- order RM, one essentially builds second-order codes for the associated fourth-order objects, often using fourth-order notation (see e.g. [5, §7]).
A set $Y$ is located if the distance function $d(x, Y)=\inf_{y\in Y}d(x, y)$ is given by (a code for) a continuous function ([6,9]).
References
[1] Jeremy Avigad and Ksenija Simic, Fundamental notions of analysis in subsystems of second-order arithmetic, Ann. Pure Appl. Logic 139 (2006), no. 1-3, 138–184.
[2] Douglas K. Brown, Notions of closed subsets of a complete separable metric space in weak subsystems of second-order arithmetic, Logic and computation (Pittsburgh, PA, 1987), Con- temp. Math., vol. 106, Amer. Math. Soc., Providence, RI, 1990, pp. 39–50.
[3] ____, Notions of compactness in weak subsystems of second order arithmetic, Reverse mathematics 2001, Lect. Notes Log., vol. 21, Assoc. Symbol. Logic, 2005, pp. 47–66.
[4] Mariagnese Giusto and Stephen G. Simpson, Located sets and reverse mathematics, J. Sym- bolic Logic 65 (2000), no. 3, 1451–1480.
[5] Mariagnese Giusto and Alberto Marcone, Lebesgue numbers and Atsuji spaces in subsystems of second-order arithmetic, Arch. Math. Logic 37 (1998), no. 5-6, 343–362.
[6] Carl Mummert and Stephen G. Simpson, Reverse mathematics and $\Pi_2^1$-comprehension, Bull. Symbolic Logic 11 (2005), no. 4, 526–533.
[7] Carl Mummert, On the reverse mathematics of general topology, ProQuest LLC, Ann Arbor, MI, 2005. Thesis (Ph.D.)–The Pennsylvania State University.
[8] ___, Reverse mathematics of MF spaces, J. Math. Log. 6 (2006), no. 2, 203–232.
[9] Stephen G. Simpson, Subsystems of second order arithmetic, 2nd ed., Perspectives in Logic, CUP, 2009.
