I can offer a computational perspective. In computable mathematics we are interested in "computing with mathematical objects" such as integers, finite sets, real numbers, infinite-dimensional Banach spaces, compact subsets of $\mathbb{R}^n$, and many other "infinite" things. Some of these are pretty complicated, so the question arises how to represent them as a data structures, in other words, we face a coding problem, just like in Reverse Mathematics.

In computability theory we normally code everything with natural numbers. Another possibility is to code things with "reals", by which computability theorists mean infinite binary sequences. In actual implementations we code by elements of datatypes available to us in a programming language. But we always face the same question, namely what does it mean to correctly encode a given mathematical object.

To properly answer such a question we have to take a very important step: we must turn encodings themselves into honest mathematical objects and collect them all (even the allegedly sensless ones) into a manageable mathematical structure, say a category. We should be able to use the structure of the resulting category to bring some order and sense to the black art of "choosing appropriate codings".

When this is done in computable mathematics, the result is a realizability topos. This is great, as we can interpret higher-order (intuitionistic) logic in it, and that suffices to develop mathematics. To see how this works, consider an easy example, the natural numbers. Nobody ever questions encodings of natural numbers, but nevertheless it is possible to come up with some bad ones. Encodings are objects of a realizability topos. Thus, a candidate encoding for natural numbers lives inside the topos as an object $N$. If in the topos the object $N$ satisfies Peano axioms, then it correctly encodes natural numbers, otherwise it does not.

Our correctness criterion then is this: an encoding is correct when, seen as an object of the realizability topos, it corresponds to the expected mathematical object. Other examples are easy to come by:

• An encoding of real numbers is correct if the corresponding object in the topos is a Cauchy-complete archimedean ordered field.
• An encoding of c.e. sets is correct if in the corresponding object in the topos is the object of countable subsets of $\mathbb{N}$.
• An encoding of functions $X \to Y$ is correct if in the topos it is the exponential object of $X$ and $Y$.
• An encoding of a group is correct if in the topos it corresponds to a group.
• etc.

As toposes and intuitionistic mathematics make snaicititamehtam queasy, and reverse mathematics happens in the context of classical logic anyway, realizaiblity toposes are not going to be the right answer for Reverse Mathematics. Nevertheless, we have a plan: what category, or (non-standard) model of (weak) set-theory captures the idea of coding in Recursive Mathematics? If you can find it, and it has good enough properties, it should give some answers. This sounds like somebody's PhD.

I can offer a computational perspective. In computable mathematics we are interested in "computing with mathematical objects" such as integers, finite sets, real numbers, infinite-dimensional Banach spaces, compact subsets of $\mathbb{R}^n$, and many other "infinite" things. Some of these are pretty complicated, so the question arises how to represent them as a data structures, in other words, we face a coding problem, just like in Reverse Mathematics.

In computability theory we normally code everything with natural numbers. Another possibility is to code things with "reals", by which computability theorists mean infinite binary sequences. In actual implementations we code by elements of datatypes available to us in a programming language. But we always face the same question, namely what does it mean to correctly encode a given mathematical object.

To properly answer such a question we have to take a very important step: we must turn encodings themselves into honest mathematical objects and collect them all (even the allegedly senseless ones) into a manageable mathematical structure, say a category. We should be able to use the structure of the resulting category to bring some order and sense to the black art of "choosing appropriate codings".

When this is done in computable mathematics, the result is a realizability topos. This is great, as we can interpret higher-order (intuitionistic) logic in it, and that suffices to develop mathematics. To see how this works, consider an easy example, the natural numbers. Nobody ever questions encodings of natural numbers, but nevertheless it is possible to come up with some bad ones. Encodings are objects of a realizability topos. Thus, a candidate encoding for natural numbers lives inside the topos as an object $N$. If in the topos the object $N$ satisfies Peano axioms, then it correctly encodes natural numbers, otherwise it does not.

Our correctness criterion then is this: an encoding is correct when, seen as an object of the realizability topos, it corresponds to the expected mathematical object. Other examples are easy to come by:

• An encoding of real numbers is correct if the corresponding object in the topos is a Cauchy-complete Archimedean ordered field.
• An encoding of c.e. sets is correct if in the corresponding object in the topos is the object of countable subsets of $\mathbb{N}$.
• An encoding of functions $X \to Y$ is correct if in the topos it is the exponential object of $X$ and $Y$.
• An encoding of a group is correct if in the topos it corresponds to a group.
• etc.

As toposes and intuitionistic mathematics are often unfamiliar to mathematicians, and reverse mathematics happens in the context of classical logic anyway, realizability toposes are not going to be the right answer for Reverse Mathematics. Nevertheless, we have a plan: what category, or (non-standard) model of (weak) set-theory captures the idea of coding in Recursive Mathematics? If you can find it, and it has good enough properties, it should give some answers. This sounds like somebody's PhD.

I can offer a computational perspective. In computable mathematics we are interested in "computing with mathematical objects" such as integers, finite sets, real numbers, infinite-dimensional Banach spaces, compact subsets of $\mathbb{R}^n$, and many other "infinite" things. Some of these are pretty complicated, so the question arises how to represent them as a data structures, in other words, we face a coding problem, just like in Reverse Mathematics.

In computability theory we normally code everything with natural numbers. Another possibility is to code things with "reals", by which computability theorists mean infinite binary sequences. In actual implementations we code by elements of datatypes available to us in a programming language. But we always face the same question, namely what does it mean to correctly encode a given mathematical object.

To properly answer such a question we have to take a very important step: we must turn encodings themselves into honest mathematical objects and collect them all (even the allegedly sensless ones) into a manageable mathematical structure, say a category. We should be able to use the structure of the resulting category to bring some order and sense to the black art of "choosing appropriate codings".

When this is done in computable mathematics, the result is a realizability topos. This is great, as we can interpret higher-order (intuitionistic) logic in it, and that suffices to develop mathematics. To see how this works, consider an easy example, the natural numbers. Nobody ever questions encodings of natural numbers, but nevertheless it is possible to come up with some bad ones. Encodings are objects of a realizability topos. Thus, a candidate encoding for natural numbers lives inside the topos as an object $N$. If in the topos the object $N$ satisfies Peano axioms, then it correctly encodes natural numbers, otherwise it does not.

Our correctness criterion then is this: an encoding is correct when, seen as an object of the realizability topos, it corresponds to the expected mathematical object. Other examples are easy to come by:

• An encoding of real numbers is correct if the corresponding object in the topos is a Cauchy-complete archimedean ordered field.
• An encoding of functions $X \to Y$ is correct if in the topos it is the exponential object of $X$ and $Y$.
• An encoding of a group is correct if in the topos it corresponds to a group.
• etc.

As toposes and intuitionistic mathematics make snaicititamehtam queasy, and reverse mathematics happens in the context of classical logic anyway, realizaiblity toposes are not going to be the right answer. Nevertheless, we have a plan: what category or (non-standard) model of (weak) set-theory captures the idea of coding in Recursive Mathematics? If you can find it, and it has good enough properties, it should give some answers.

I can offer a computational perspective. In computable mathematics we are interested in "computing with mathematical objects" such as integers, finite sets, real numbers, infinite-dimensional Banach spaces, compact subsets of $\mathbb{R}^n$, and many other "infinite" things. Some of these are pretty complicated, so the question arises how to represent them as a data structures, in other words, we face a coding problem, just like in Reverse Mathematics.

In computability theory we normally code everything with natural numbers. Another possibility is to code things with "reals", by which computability theorists mean infinite binary sequences. In actual implementations we code by elements of datatypes available to us in a programming language. But we always face the same question, namely what does it mean to correctly encode a given mathematical object.

To properly answer such a question we have to take a very important step: we must turn encodings themselves into honest mathematical objects and collect them all (even the allegedly sensless ones) into a manageable mathematical structure, say a category. We should be able to use the structure of the resulting category to bring some order and sense to the black art of "choosing appropriate codings".

When this is done in computable mathematics, the result is a realizability topos. This is great, as we can interpret higher-order (intuitionistic) logic in it, and that suffices to develop mathematics. To see how this works, consider an easy example, the natural numbers. Nobody ever questions encodings of natural numbers, but nevertheless it is possible to come up with some bad ones. Encodings are objects of a realizability topos. Thus, a candidate encoding for natural numbers lives inside the topos as an object $N$. If in the topos the object $N$ satisfies Peano axioms, then it correctly encodes natural numbers, otherwise it does not.

Our correctness criterion then is this: an encoding is correct when, seen as an object of the realizability topos, it corresponds to the expected mathematical object. Other examples are easy to come by:

• An encoding of real numbers is correct if the corresponding object in the topos is a Cauchy-complete archimedean ordered field.
• An encoding of c.e. sets is correct if in the corresponding object in the topos is the object of countable subsets of $\mathbb{N}$.
• An encoding of functions $X \to Y$ is correct if in the topos it is the exponential object of $X$ and $Y$.
• An encoding of a group is correct if in the topos it corresponds to a group.
• etc.

As toposes and intuitionistic mathematics make snaicititamehtam queasy, and reverse mathematics happens in the context of classical logic anyway, realizaiblity toposes are not going to be the right answer for Reverse Mathematics. Nevertheless, we have a plan: what category, or (non-standard) model of (weak) set-theory captures the idea of coding in Recursive Mathematics? If you can find it, and it has good enough properties, it should give some answers. This sounds like somebody's PhD.