<p>You are touching on some very interesting basic questions about mathematics in general. Do we construct mathematical objects and later discover their structure, or do we construct objects with a specific structure in mind? I think the answer is not simple. Sometimes we "design" structures to order, and sometimes we discover them. I believe the quarternions were discovered, but at the same time Hamilton knew what sort of structure to look for. So I think your observation that we discover the structure of the objects we constructed has a lot of merit. But why do we discover some objects and not others? What makes the ones we pay attention to important and interesting? Presumably their structure.</p>

<p>Let me clear up something about equality versus addition. They have exactly the same status. The reals are equipped with equality, which is a binary relation, and they are also equipped with addition, which is a binary operation. We make no assumptions about equality being decidable, or not decidable, and neither to we make any assumption about addition being computable. We just state the axioms for the reals: they form a structure consisting of such-and-such relations and operations, satisfying such-and-such axioms. Then we ask whether such a structure exists in our (realizability) model. If it does, then we have an implementation of its parts. Addition is implemented by a program which takes realizers for two reals and computes a realizer for their sum. But how is equality implemented?</p>

<p>Equality is a binary relation, which is just a predicate on a cartesian product. So we might as well think about how to implement a predicate on a set. Well, there are two views of predicates. The first one is that a predicate $P$ on a set $X$ is just a subset $P \subseteq X$. The second one is that it is a map $P : X \to \lbrace 0, 1 \rbrace$. In intuitionistic mathematics, we have to replace the booleans $\lbrace 0, 1 \rbrace$ with the set of all truth values $\Omega$, which is much larger. In fact $\Omega$ is so complicated that it does not exist in the simple realizability models (although it exists in a realizability topos), which is a fancy way of saying that it cannot be implemented (feel free to have a go: implement the initial complete Heyting algebra; mind you, it has to have suprema of families indexed by atbitrary datatypes). So in general we cannot implement predicates as maps into the subobject classfier. We can of course implement them as subobjects, but that is rather useless, e.g., equality on $\mathbb{R}$ would be implemented as the map $x \mapsto (x, x)$.</p>

<p>Fortunately, certain pieces of $\Omega$ still exist in realizability models. If a predicate $P : X \to \Omega$ happens to factor through such a piece of $\Omega$, then we get to implement its classifying map. Some examples:</p>

<ul>
<li><p>the booleans $2 = \lbrace p \in \Omega \mid p \lor \lnot p\rbrace$ are familiar to every programmer, and most programming languages have the corresponding type <code>bool</code>. A predicate $P : X \to 2$ is knows as <em>decidable</em> and can be implemented as a map into <code>bool</code>. All this is familiar.</p></li>
<li><p>the semidecidable truth values $\Sigma = \lbrace p \in \Omega \mid \exists f : \mathbb{N} \to 2 . p = (\exists n \in \mathbb{N} . f n = 1)\rbrace$ are those truth values that are equal to an existential quantification over $\mathbb{N}$ of a decidable predicate. They are around, not every programmer knows about them, but theoretical computer scientists are of course familiar with semidecidability. A <em>semidecidable</em> predicate $P : X \to \Sigma$ can be implemented as a map <code>P : X -&gt; (nat -&gt; bool)</code>: it takes a realizer <code>x</code> for $x \in X$ and returns a realizer <code>f : nat -&gt; bool</code> of some $f : \mathbb{N} \to 2$ such that $x \in P$ is equivalent to $\exists n . f n = 1$. This is less familiar and less useful.</p></li>
<li><p>the classical truth values $\Omega_{\lnot\lnot} = \lbrace p \in \Omega \mid \lnot\lnot p = p\rbrace$ exist in a category of assemblies but not in a category of modest sets. So we are reaching the limit of what can be implemented. The implementation of $\Omega_{\lnot\lnot}$ is silly, because it is implemented by the <code>unit</code> type. In other words, a classical predicate $P : X \to \Omega_{\lnot\lnot}$ is implemented by a function which always returns the unit <code>()</code>.
And I am not making this up. I am telling you what the realizability interpretation gives as a result.</p></li>
</ul>

<p>It just so happens that $=$ on reals is <em>not</em> classified by a map into $2$, but it is classified by a map into $\Omega_{\lnot\lnot}$. So in principle one could implement equality as a map which always returns the unit <code>()</code>. That's useless. Perhaps $=$ is classified by a map into a smaller part of $\Omega$? Yes, it is a <em>theorem</em> that <em>inequality</em> $\neq$ is classifed by a map into $\Sigma$, so we <em>can</em> do better and implement $\neq$ as a map <code>neq : real -&gt; real -&gt; (nat -&gt; bool)</code> which takes (realizers of) two reals $x$ and $y$, and returns a map <code>f : nat -&gt; bool</code> which attains <code>true</code> iff $x \neq y$. But this is actually a very sensible thing: <code>neq x y n</code> tests <code>x</code> and <code>y</code> for inequality "up to precision <code>n</code>". That's how people actually implement exact real arithmetic.</p>

<p>I think a lot of confusion arises from the fact that people speak about "computable" relations without telling us wha that means. And when they do, they usually end up defining decidable relations. But that's just a very limited view of relations. There are semidecidable relations, and $\Pi^0_2$ relations, and arithmetical relations, etc.</p>

CC BY-SA 3.0
2013-02-19T23:57:36.270Z
Thanks Andrej. I feel I have to think about your answer more and probably reread it a few more times to completely understand it. But I also feel I see where my confusion comes from. Here we are taking the algebraic/category theoretic perspective of mathematics and in that sense real numbers are defined by structure of objects satisfying some axioms. From that perspective, I can understand what you are saying but to get it completely I should probably read your thesis which has been on my reading list for sometime.
Kaveh
CC BY-SA 3.0
2013-02-20T00:00:31.710Z
When I personally think about real numbers (from the set theoretical perspective?), I am mostly used to think about each real number as a stand alone construction/object independent of any structure it belongs to, and structures and axioms satisfied by them come later. I feel that the emphasis put on structures is relatively new as I don't remember seeing it in older works of constructivists (e.g. Brouwer, Heyting, Beeson, etc.) or researchers in computable analysis ( IIRC there wasn't much emphasis on structures that objects belong to even in Weihrauch's book).
Kaveh
CC BY-SA 3.0
2013-02-20T06:06:29.427Z
I accept your answer for clarifying my misunderstanding: addition and equality are not treated differently.
Kaveh
CC BY-SA 3.0
2013-02-20T09:11:32.360Z
Thanks. In my opinion a mathematical object should never be studied in "isolation", but always in relation to the rest of the "universe". So yes, a real number is just a point of a space, but you cannot learn everything about the space if you think of it as just a collection of points. And neither can you learn everything about a space without thinking about how it relates to other spaces. And neither can you learn everything about a category of spaces without thinking about how it relates to other categories. Oh my god, this is Hegel talking through me! Devil be gone!
Andrej Bauer
CC BY-SA 3.0
2013-02-19T22:58:54.447Z
2013-02-19T23:09:53.197Z
2013-02-19T23:09:53.197Z
Andrej Bauer
<h3>Question</h3>
<blockquote>
<p>What is a reasonable representation of objects (for computability)?<br />
What is the criteria that we should apply to see if a representation is reasonable?</p>
</blockquote>
<p><a href="https://cstheory.stackexchange.com/a/16547/">This answer</a> by Andrej suggests that the representation should be <em>workable</em> and &quot;workable&quot; here means that the basic operations associated with those objects should be computable over those representations. More formally, as I understand it, he is saying that we are not representing objects alone but a structure of objects that comes with some operations, and a representation should allow us to compute the operations coming from that structure. After we pick a representation for that structure, we can start taking about computing other operations.</p>
<p>However I don't feel that answer is satisfying for two reasons:</p>
<ol>
<li><p>We already make a decision about what to be computable when deciding what operations are basic. For example, I feel that Andrej in <a href="https://cstheory.stackexchange.com/a/16547/">his answer</a> already decided that equality is not going to be decidable.</p>
</li>
<li><p>Objects don't really come with an associated structure. We think of the same objects as belonging to several different structures. Sometimes the model of computation cannot support all of the operations of the natural structure associated with objects, e.g. for real numbers one would probably want at least addition, multiplication, order, and equality. This has lead to models of computation like real-RAM and BSS though one can argue that they are not practical.</p>
</li>
</ol>
<p>I feel that from constructive perspective, what is important is how the objects are <em>constructed</em>. The structures and operations come later. A reasonable representation should allow us to obtain enough information about the way an object is constructed and the computability of any other operation should be based on computability of of them from this information.</p>
<p>So my main question:</p>
<blockquote>
<p>Why we need a reasonable representation of objects (e.g. real numbers) support anything more than a mechanism to give us information about the construction of those objects (arbitrary good enough approximations)? Why we need a reasonable representation to support the operations of a structure on those objects (e.g. addition on real numbers)? And how can we decide which operations are essential and which ones are not (e.g. why addition on real numbers and not equality of real numbers)?</p>
</blockquote>
<hr />
<h3>Background</h3>
<p>Many computational models usually deal with very basic data types. For example, a Turing machine works on a string of symbols from a fixed finite alphabet.</p>
<p>However, often we need to perform computation on other kind of objects, e.g. natural numbers,  rational numbers, graphs, Turing machines, real numbers, etc. We encode objects as objects of the basic data types that the machine is designed to work with. More formally, a representation is a function from a basic data type supported by the machine to the set of objects we want to talk about.</p>
<p>Examples:</p>
<ul>
<li><p>We can encode natural numbers as strings of bits of their binary representation: <span class="math-container">$\langle n \rangle = (n)_2 $</span>.</p>
</li>
<li><p>We can encode integers numbers using pairs of natural numbers and a pair like <span class="math-container">$\langle n,m\rangle$</span> represents the integer <span class="math-container">$n-m$</span>.</p>
</li>
<li><p>We can encode rationals using a pair of a natural number and an integer <span class="math-container">$\langle \frac{p}{q}\rangle = \langle p, q\rangle$</span>.</p>
</li>
</ul>
<p>Each object can have several names, and we can define the equality between these names, e.g. <span class="math-container">$\langle \frac{p}{q}\rangle = \langle \frac{p'}{q'}\rangle$</span> iff <span class="math-container">$pq'=p'q$</span> to say that two names refer to the same object.</p>
<p>More examples:</p>
<ul>
<li><p>We can represents a graph with vertices <span class="math-container">$\{1,\ldots, n\}$</span> by the number of vertices <span class="math-container">$n$</span> and its list of edges. Or we can represent it using its adjacency matrix.</p>
</li>
<li><p>We can represent a Turing machine as a labeled graph.</p>
</li>
</ul>
<p>The natural representations that one normally comes up with are equally good for computability (but not always for complexity) as we can convert any of them to other ones computably.</p>
<p>However one can also define more complicated representations: for example, we can represent a Turing machine as a labeled graph plus a proof in ZFC telling us if it is a halting when we have one. But we can also define a representation of Turing machines as a labeled graph plus one bit telling us if the machine halts on blank tape. This representation doesn't seem to be reasonable, e.g. it allows us to decide a Turing machine halts or not which is undecidable using usual representations, we also don't know how give an Turing machine as an input in practice as it would need us to know the answer to the halting problem on that machine. It give a sense of why this representation is not suitable, however it is still not easy to articulate why the representation is unreasonable (at least for me).</p>
<p>The explanation is usually along the lines that we take <em>a weakest workable representation</em>. Let me first explain what weakest means here: weakest means that any other workable representation can be computably converted to this representation. It seems a reasonable condition. However &quot;workable&quot; is bit vague and complicated here, for Turing machines one normally means something like the representation satisfies SMN and UTM theorems, however articulating why is not easy (at least it is not for me).</p>
<p>For computability on finite objects the problem is not big (and therefor the issue is completely avoided usually in introduction to computability and complexity): someone who is not familiar with these issues will normally use a representation which satisfies these conditions and is equivalent to other reasonable representations of the objects.</p>
<p>A similar issue comes up sometimes in complexity where it is not clear if there is a weakest workable representation: some algorithms work better with one representation, others work with other representation and all of these representations are considered reasonable (e.g. adjacency matrix, incidence matrix, etc. for graphs). Often the issue of representations and reasonable representations is avoided (one might say somewhat swept under the carpet) by saying that we define a problem not the objects but on a fixed representation of the objects. So a graph problem is not about graphs but about a particular representation of them.</p>
<p>However when we move to computability over objects that are inherently infinite, e.g. real numbers, the issue becomes more serious. If a person unfamiliar with computability over real numbers tries to come up with a representation the first representation is likely to be the decimal/binary expansion of the number which is not good for various reasons, e.g. even addition is not computable. Another representation might allow us to compute addition but not another function, or say equality with <span class="math-container">$0$</span>. Yet another representation might allow us to compute equality to <span class="math-container">$0$</span> but not addition. And it is not even as clear if there is a weakest &quot;workable&quot; representation and/or what does we mean by &quot;workable&quot;.</p>
<p>(There is also an issue of computability in what model which I will avoid for this question.)</p>

CC BY-SA 3.0
2013-02-19T21:11:52.567Z
I disagree with the comment about Andrej's decision in his answer. The decision is not that equality is undecidable, but that the decidability of equality is not apriori fixed. This is different because it may or may not be decidable. In a broad sense, this decision is no different from the way we deal with models of computation. Transition relations have computable representations but decidability of language inclusion is a property that follows and is not fixed by design.
Vijay D
CC BY-SA 3.0
2013-02-19T21:21:33.173Z
@VijayD, you can rephrase my question as follows: why addition is treated differently from equality? IIUC Andrej's answwer, it is because "real numbers" means *a particular structure of real numbers which has addition but not equality*. My questions are: why we need to consider structures in the first place? and if we need to which structure should we take as *the* structure real numbers?
Kaveh
CC BY-SA 3.0
2013-02-19T22:34:00.163Z
Andrej simply assumed that addition should be computable whereas equality does not have to be computable.  There is no inherent reason why other people have to make the same assumptions.  This is basically why we have to define encoding to define any computational problems, and we all do this every day.  I do not think that this is a research-level question in theoretical computer science.  I voted to close it as off topic.
Tsuyoshi Ito
CC BY-SA 3.0
2013-02-19T23:00:47.003Z
I did not assume *anything* about the computability of addition and equality, see my answer. They both have exactly the same status. I think we need to clear up what it means for a predicate to be "computable". You all seem to think that predicates are functions into booleans or some such. They are subobjects.
Andrej Bauer
CC BY-SA 3.0
2013-02-19T23:42:27.270Z
@Tsuyoshi, you can rephrase my question as follows: why does some experts in computable analysis make the assumption you mentioned? Considering that Andrej is an expert on the topic of computable analysis and constructive mathematics I think asking why he is making that assumption is a research-level question. I feel that either there is a misunderstanding on my side or there is a good reason why he is making that assumption which I am missing.
Kaveh
CC BY-SA 3.0
2013-02-20T00:11:04.270Z
+1 Nice question. Are you looking for a definition of  **natural** representation/encoding of objects?
Mohammad Al-Turkistany
CC BY-SA 3.0
2013-02-20T01:32:09.640Z
@Mohammad, natural is an overloaded word, I am looking for a definition for what would be considered a reasonable/acceptable representation.
Kaveh
CC BY-SA 3.0
2013-02-20T04:11:22.510Z
I don't think this is the appropriate forum for the debate that this question is designed to invite (or continue).  I'm voting to close the question, but I think it would make a great post for the community blog.
Jeffε
CC BY-SA 3.0
2013-02-20T04:55:13.830Z
@JɛﬀE, I understand, as you say this might be more suitable for a blog post/discussion. I will try to see if I can edit this so it does lead to a debate (which wasn't my intention for posting this question).
Kaveh
CC BY-SA 3.0
2013-02-20T06:03:07.443Z
I thought about how to modify the question but don't see a good way of asking the question right now. I am fine with closing this question as "not constructive".
Kaveh
CC BY-SA 3.0
2013-02-20T09:12:55.523Z
I agree that it would be better to have a discussion, and that this forum is not the best place for it. Where should we go?
Andrej Bauer
CC BY-SA 3.0
2013-02-21T01:12:21.777Z
@Andrej, we can continue the discussion in the [chat], we can also create a new room for the discussion if you prefer that.
Kaveh
CC BY-SA 3.0
2013-02-22T01:41:21.073Z
2nd the idea for _someone_ to update the [tcs blog](http://cstheory.blogoverflow.com/?blb=1) which is now nearly a _year_ without an update. see also meta question from last summer [what is the status of the community blog](http://meta.cstheory.stackexchange.com/questions/1583/status-of-our-community-blog) (now 7 votes)
vzn
<cc.complexity-theory><computability><computable-analysis>
What is a reasonable representation/encoding of objects?
Kaveh
# What is a reasonable representation/encoding of objects?

(Asked by: username_0 on 2013-02-19)

### Question

> What is a reasonable representation of objects (for computability)?  
> What is the criteria that we should apply to see if a representation is reasonable?

[This answer](https://cstheory.stackexchange.com/a/16547/) by Andrej suggests that the representation should be *workable* and "workable" here means that the basic operations associated with those objects should be computable over those representations. More formally, as I understand it, he is saying that we are not representing objects alone but a structure of objects that comes with some operations, and a representation should allow us to compute the operations coming from that structure. After we pick a representation for that structure, we can start taking about computing other operations.

However I don't feel that answer is satisfying for two reasons:

1. We already make a decision about what to be computable when deciding what operations are basic. For example, I feel that Andrej in [his answer](https://cstheory.stackexchange.com/a/16547/) already decided that equality is not going to be decidable.
2. Objects don't really come with an associated structure. We think of the same objects as belonging to several different structures. Sometimes the model of computation cannot support all of the operations of the natural structure associated with objects, e.g. for real numbers one would probably want at least addition, multiplication, order, and equality. This has lead to models of computation like real-RAM and BSS though one can argue that they are not practical.

I feel that from constructive perspective, what is important is how the objects are *constructed*. The structures and operations come later. A reasonable representation should allow us to obtain enough information about the way an object is constructed and the computability of any other operation should be based on computability of of them from this information.

So my main question:

> Why we need a reasonable representation of objects (e.g. real numbers) support anything more than a mechanism to give us information about the construction of those objects (arbitrary good enough approximations)? Why we need a reasonable representation to support the operations of a structure on those objects (e.g. addition on real numbers)? And how can we decide which operations are essential and which ones are not (e.g. why addition on real numbers and not equality of real numbers)?

---

### Background

Many computational models usually deal with very basic data types. For example, a Turing machine works on a string of symbols from a fixed finite alphabet.

However, often we need to perform computation on other kind of objects, e.g. natural numbers, rational numbers, graphs, Turing machines, real numbers, etc. We encode objects as objects of the basic data types that the machine is designed to work with. More formally, a representation is a function from a basic data type supported by the machine to the set of objects we want to talk about.

Examples:

* We can encode natural numbers as strings of bits of their binary representation: $\langle n \rangle = (n)\_2 $.
* We can encode integers numbers using pairs of natural numbers and a pair like $\langle n,m\rangle$ represents the integer $n-m$.
* We can encode rationals using a pair of a natural number and an integer $\langle \frac{p}{q}\rangle = \langle p, q\rangle$.

Each object can have several names, and we can define the equality between these names, e.g. $\langle \frac{p}{q}\rangle = \langle \frac{p'}{q'}\rangle$ iff $pq'=p'q$ to say that two names refer to the same object.

More examples:

* We can represents a graph with vertices $\{1,\ldots, n\}$ by the number of vertices $n$ and its list of edges. Or we can represent it using its adjacency matrix.
* We can represent a Turing machine as a labeled graph.

The natural representations that one normally comes up with are equally good for computability (but not always for complexity) as we can convert any of them to other ones computably.

However one can also define more complicated representations: for example, we can represent a Turing machine as a labeled graph plus a proof in ZFC telling us if it is a halting when we have one. But we can also define a representation of Turing machines as a labeled graph plus one bit telling us if the machine halts on blank tape. This representation doesn't seem to be reasonable, e.g. it allows us to decide a Turing machine halts or not which is undecidable using usual representations, we also don't know how give an Turing machine as an input in practice as it would need us to know the answer to the halting problem on that machine. It give a sense of why this representation is not suitable, however it is still not easy to articulate why the representation is unreasonable (at least for me).

The explanation is usually along the lines that we take *a weakest workable representation*. Let me first explain what weakest means here: weakest means that any other workable representation can be computably converted to this representation. It seems a reasonable condition. However "workable" is bit vague and complicated here, for Turing machines one normally means something like the representation satisfies SMN and UTM theorems, however articulating why is not easy (at least it is not for me).

For computability on finite objects the problem is not big (and therefor the issue is completely avoided usually in introduction to computability and complexity): someone who is not familiar with these issues will normally use a representation which satisfies these conditions and is equivalent to other reasonable representations of the objects.

A similar issue comes up sometimes in complexity where it is not clear if there is a weakest workable representation: some algorithms work better with one representation, others work with other representation and all of these representations are considered reasonable (e.g. adjacency matrix, incidence matrix, etc. for graphs). Often the issue of representations and reasonable representations is avoided (one might say somewhat swept under the carpet) by saying that we define a problem not the objects but on a fixed representation of the objects. So a graph problem is not about graphs but about a particular representation of them.

However when we move to computability over objects that are inherently infinite, e.g. real numbers, the issue becomes more serious. If a person unfamiliar with computability over real numbers tries to come up with a representation the first representation is likely to be the decimal/binary expansion of the number which is not good for various reasons, e.g. even addition is not computable. Another representation might allow us to compute addition but not another function, or say equality with $0$. Yet another representation might allow us to compute equality to $0$ but not addition. And it is not even as clear if there is a weakest "workable" representation and/or what does we mean by "workable".

(There is also an issue of computability in what model which I will avoid for this question.)

**Tags:** cc.complexity-theory, computability, computable-analysis
> **Comments:**
> **username_1**: I disagree with the comment about Andrej's decision in his answer. The decision is not that equality is undecidable, but that the decidability of equality is not apriori fixed. This is different because it may or may not be decidable. In a broad sense, this decision is no different from the way we deal with models of computation. Transition relations have computable representations but decidability of language inclusion is a property that follows and is not fixed by design.  
> **username_0**: @VijayD, you can rephrase my question as follows: why addition is treated differently from equality? IIUC Andrej's answwer, it is because "real numbers" means *a particular structure of real numbers which has addition but not equality*. My questions are: why we need to consider structures in the first place? and if we need to which structure should we take as *the* structure real numbers?  
> **username_2**: Andrej simply assumed that addition should be computable whereas equality does not have to be computable.  There is no inherent reason why other people have to make the same assumptions.  This is basically why we have to define encoding to define any computational problems, and we all do this every day.  I do not think that this is a research-level question in theoretical computer science.  I voted to close it as off topic.  
> **username_3**: I did not assume *anything* about the computability of addition and equality, see my answer. They both have exactly the same status. I think we need to clear up what it means for a predicate to be "computable". You all seem to think that predicates are functions into booleans or some such. They are subobjects.  
> **username_0**: @Tsuyoshi, you can rephrase my question as follows: why does some experts in computable analysis make the assumption you mentioned? Considering that Andrej is an expert on the topic of computable analysis and constructive mathematics I think asking why he is making that assumption is a research-level question. I feel that either there is a misunderstanding on my side or there is a good reason why he is making that assumption which I am missing.  
> **username_4**: +1 Nice question. Are you looking for a definition of  **natural** representation/encoding of objects?  
> **username_0**: @Mohammad, natural is an overloaded word, I am looking for a definition for what would be considered a reasonable/acceptable representation.  
> **username_5**: I don't think this is the appropriate forum for the debate that this question is designed to invite (or continue).  I'm voting to close the question, but I think it would make a great post for the community blog.  
> **username_0**: @JɛﬀE, I understand, as you say this might be more suitable for a blog post/discussion. I will try to see if I can edit this so it does lead to a debate (which wasn't my intention for posting this question).  
> **username_0**: I thought about how to modify the question but don't see a good way of asking the question right now. I am fine with closing this question as "not constructive".  
> **username_3**: I agree that it would be better to have a discussion, and that this forum is not the best place for it. Where should we go?  
> **username_0**: @Andrej, we can continue the discussion in the [chat], we can also create a new room for the discussion if you prefer that.  
> **username_6**: 2nd the idea for _someone_ to update the [tcs blog](http://cstheory.blogoverflow.com/?blb=1) which is now nearly a _year_ without an update. see also meta question from last summer [what is the status of the community blog](http://meta.cstheory.stackexchange.com/questions/1583/status-of-our-community-blog) (now 7 votes)  

---

## 1 answers

### Answer by username_3 on 2013-02-19. Score: 9 | Accepted answer

You are touching on some very interesting basic questions about mathematics in general. Do we construct mathematical objects and later discover their structure, or do we construct objects with a specific structure in mind? I think the answer is not simple. Sometimes we "design" structures to order, and sometimes we discover them. I believe the quarternions were discovered, but at the same time Hamilton knew what sort of structure to look for. So I think your observation that we discover the structure of the objects we constructed has a lot of merit. But why do we discover some objects and not others? What makes the ones we pay attention to important and interesting? Presumably their structure.

Let me clear up something about equality versus addition. They have exactly the same status. The reals are equipped with equality, which is a binary relation, and they are also equipped with addition, which is a binary operation. We make no assumptions about equality being decidable, or not decidable, and neither to we make any assumption about addition being computable. We just state the axioms for the reals: they form a structure consisting of such-and-such relations and operations, satisfying such-and-such axioms. Then we ask whether such a structure exists in our (realizability) model. If it does, then we have an implementation of its parts. Addition is implemented by a program which takes realizers for two reals and computes a realizer for their sum. But how is equality implemented?

Equality is a binary relation, which is just a predicate on a cartesian product. So we might as well think about how to implement a predicate on a set. Well, there are two views of predicates. The first one is that a predicate $P$ on a set $X$ is just a subset $P \subseteq X$. The second one is that it is a map $P : X \to \lbrace 0, 1 \rbrace$. In intuitionistic mathematics, we have to replace the booleans $\lbrace 0, 1 \rbrace$ with the set of all truth values $\Omega$, which is much larger. In fact $\Omega$ is so complicated that it does not exist in the simple realizability models (although it exists in a realizability topos), which is a fancy way of saying that it cannot be implemented (feel free to have a go: implement the initial complete Heyting algebra; mind you, it has to have suprema of families indexed by atbitrary datatypes). So in general we cannot implement predicates as maps into the subobject classfier. We can of course implement them as subobjects, but that is rather useless, e.g., equality on $\mathbb{R}$ would be implemented as the map $x \mapsto (x, x)$.

Fortunately, certain pieces of $\Omega$ still exist in realizability models. If a predicate $P : X \to \Omega$ happens to factor through such a piece of $\Omega$, then we get to implement its classifying map. Some examples:

* the booleans $2 = \lbrace p \in \Omega \mid p \lor \lnot p\rbrace$ are familiar to every programmer, and most programming languages have the corresponding type `bool`. A predicate $P : X \to 2$ is knows as *decidable* and can be implemented as a map into `bool`. All this is familiar.
* the semidecidable truth values $\Sigma = \lbrace p \in \Omega \mid \exists f : \mathbb{N} \to 2 . p = (\exists n \in \mathbb{N} . f n = 1)\rbrace$ are those truth values that are equal to an existential quantification over $\mathbb{N}$ of a decidable predicate. They are around, not every programmer knows about them, but theoretical computer scientists are of course familiar with semidecidability. A *semidecidable* predicate $P : X \to \Sigma$ can be implemented as a map `P : X -> (nat -> bool)`: it takes a realizer `x` for $x \in X$ and returns a realizer `f : nat -> bool` of some $f : \mathbb{N} \to 2$ such that $x \in P$ is equivalent to $\exists n . f n = 1$. This is less familiar and less useful.
* the classical truth values $\Omega\_{\lnot\lnot} = \lbrace p \in \Omega \mid \lnot\lnot p = p\rbrace$ exist in a category of assemblies but not in a category of modest sets. So we are reaching the limit of what can be implemented. The implementation of $\Omega\_{\lnot\lnot}$ is silly, because it is implemented by the `unit` type. In other words, a classical predicate $P : X \to \Omega\_{\lnot\lnot}$ is implemented by a function which always returns the unit `()`.
  And I am not making this up. I am telling you what the realizability interpretation gives as a result.

It just so happens that $=$ on reals is *not* classified by a map into $2$, but it is classified by a map into $\Omega\_{\lnot\lnot}$. So in principle one could implement equality as a map which always returns the unit `()`. That's useless. Perhaps $=$ is classified by a map into a smaller part of $\Omega$? Yes, it is a *theorem* that *inequality* $\neq$ is classifed by a map into $\Sigma$, so we *can* do better and implement $\neq$ as a map `neq : real -> real -> (nat -> bool)` which takes (realizers of) two reals $x$ and $y$, and returns a map `f : nat -> bool` which attains `true` iff $x \neq y$. But this is actually a very sensible thing: `neq x y n` tests `x` and `y` for inequality "up to precision `n`". That's how people actually implement exact real arithmetic.

I think a lot of confusion arises from the fact that people speak about "computable" relations without telling us wha that means. And when they do, they usually end up defining decidable relations. But that's just a very limited view of relations. There are semidecidable relations, and $\Pi^0\_2$ relations, and arithmetical relations, etc.

> **Comments:**
> **username_0**: Thanks Andrej. I feel I have to think about your answer more and probably reread it a few more times to completely understand it. But I also feel I see where my confusion comes from. Here we are taking the algebraic/category theoretic perspective of mathematics and in that sense real numbers are defined by structure of objects satisfying some axioms. From that perspective, I can understand what you are saying but to get it completely I should probably read your thesis which has been on my reading list for sometime.  
> **username_0**: When I personally think about real numbers (from the set theoretical perspective?), I am mostly used to think about each real number as a stand alone construction/object independent of any structure it belongs to, and structures and axioms satisfied by them come later. I feel that the emphasis put on structures is relatively new as I don't remember seeing it in older works of constructivists (e.g. Brouwer, Heyting, Beeson, etc.) or researchers in computable analysis ( IIRC there wasn't much emphasis on structures that objects belong to even in Weihrauch's book).  
> **username_0**: I accept your answer for clarifying my misunderstanding: addition and equality are not treated differently.  
> **username_3**: Thanks. In my opinion a mathematical object should never be studied in "isolation", but always in relation to the rest of the "universe". So yes, a real number is just a point of a space, but you cannot learn everything about the space if you think of it as just a collection of points. And neither can you learn everything about a space without thinking about how it relates to other spaces. And neither can you learn everything about a category of spaces without thinking about how it relates to other categories. Oh my god, this is Hegel talking through me! Devil be gone!  

---

