## Stream: general

### Topic: bijection with noncomputable inverse

#### Kevin Buzzard (Jun 11 2019 at 07:13):

There are some concepts which are obvious to computer scientists who have learnt some constructive logic but which are alien to mathematicians, and I am interested in explaining them to mathematicians.

One of these concepts is the idea that there are types which don't have decidable equality. I think I've cracked this one. One can argue that the real numbers on either side of the equality at, say, this answer are clearly "well-defined" or "computable to arbitrary accuracy" or however mathematicians would like to think of it, but mathematicians can just as easily see that there is no "one method" which will answer all questions of this nature (as evidenced by the fact that apparently there is no known method which will answer that one).

I want to do the same for bijections. Mathematicians still find it jarring that the concept of "bijection" and "map with a two-sided inverse" are not "the same" in Lean. I'd like to give an example of a bijection from the reals to the reals which is defined by an algorithm but for which there is no obvious algorithm to define the inverse. I'm assuming such a function exists -- does it? I'm also assuming that this question can be made precise (where "real number" becomes something like "for all n, a rational number within 1/n of the real numbers" or whatever; I'm hoping there are no issues here).

#### Mario Carneiro (Jun 11 2019 at 07:14):

an even simpler example of non-decidable equality is nat -> nat

#### Kevin Buzzard (Jun 11 2019 at 07:15):

I think mathematicians will prefer the real example. I'm not sure they understand what a Turing machine is.

#### Mario Carneiro (Jun 11 2019 at 07:15):

I am not talking about turing machines, I mean functions

#### Kevin Buzzard (Jun 11 2019 at 07:16):

Mathematicians are typically not taught what a computable function is.

#### Mario Carneiro (Jun 11 2019 at 07:16):

just regular functions

#### Kevin Buzzard (Jun 11 2019 at 07:16):

Well fair enough.

#### Mario Carneiro (Jun 11 2019 at 07:16):

to properly talk about decidability you need some notion of computing though

#### Mario Carneiro (Jun 11 2019 at 07:16):

an informal sense is sufficient

#### Kevin Buzzard (Jun 11 2019 at 07:17):

I know but this is the hard part for mathematicians. The example with the reals I think gets the point across for decidability.

#### Kevin Buzzard (Jun 11 2019 at 07:17):

"if I can't decide it, how can a machine?"

#### Kevin Buzzard (Jun 11 2019 at 07:18):

Maybe nat -> nat is a place to look for computable bijections with a non-computable inverse?

#### Mario Carneiro (Jun 11 2019 at 07:18):

really? I find the idea that real numbers are not decidable at least a bit weird, given that we generally picture them as completed entities, where 1 = 2 in real is no different from 1 = 2 in nat

#### Mario Carneiro (Jun 11 2019 at 07:18):

plus I can ask my calculator if real numbers are equal no problem

#### Kevin Buzzard (Jun 11 2019 at 07:18):

All I'm saying is that a mathematician will not even flinch when you say "conjecture: some stupid sum of binomial coefficients is pi^7"

#### Kevin Buzzard (Jun 11 2019 at 07:19):

and then you can say "hah! But both sides are well-defined real numbers, and we can't figure out if they're equal."

#### Mario Carneiro (Jun 11 2019 at 07:19):

conjecture: the function that maps all goldbach counterexamples to 1 and other stuff to 0 is the constant 0 function

I believe you

#### Mario Carneiro (Jun 11 2019 at 07:20):

I think it's easier to draw the parallel between Pi1 statements and equality of functions than equality of reals, but maybe that's the logician in me

#### Kevin Buzzard (Jun 11 2019 at 07:20):

and I can use this to give noncomputable bijections with noncomputable inverses

#### Kevin Buzzard (Jun 11 2019 at 07:21):

does Goldbach help with the noncomputable inverse thing?

#### Mario Carneiro (Jun 11 2019 at 07:21):

I don't know whether I have a convincing example for the bijection problem

#### Kevin Buzzard (Jun 11 2019 at 07:21):

Mathematicians don't know what a Pi1 statement is either.

#### Mario Carneiro (Jun 11 2019 at 07:21):

obviously don't say that

#### Mario Carneiro (Jun 11 2019 at 07:21):

say goldbach or RH or something

#### Kevin Buzzard (Jun 11 2019 at 07:21):

We're so ignorant. Only the logicians know, and they're retiring and not being replaced.

#### Kevin Buzzard (Jun 11 2019 at 07:21):

At least in the UK.

#### Mario Carneiro (Jun 11 2019 at 07:22):

I mentioned the bijection between option and roption before, but I don't want to explain that one

#### Kevin Buzzard (Jun 11 2019 at 07:22):

Yes, I looked at that comment and even wrote the code constructing the equiv afterwards

#### Kevin Buzzard (Jun 11 2019 at 07:22):

I used your trick of subst to avoid heqs, IIRC

#### Mario Carneiro (Jun 11 2019 at 07:23):

The problem is that you can't just use some simple type like nat -> nat because you usually get obvious bijections, even if weird ones also exist

#### Mario Carneiro (Jun 11 2019 at 07:23):

you have to put some strange subtype on the thing

#### Mario Carneiro (Jun 11 2019 at 07:23):

you can embed roption nat in nat -> bool as monotone sequences

#### Mario Carneiro (Jun 11 2019 at 07:24):

and of course option nat is isomorphic to nat

#### Mario Carneiro (Jun 11 2019 at 07:24):

so perhaps that's a solution

#### Kevin Buzzard (Jun 11 2019 at 07:25):

Thanks for these comments; I'll think more.

#### Mario Carneiro (Jun 11 2019 at 07:28):

def enat := {f : nat → bool // ∀ n, f n = tt → f (n+1) = tt}

def f : nat → enat
| 0 := ⟨λ _, ff, λ n h, h⟩
| (n+1) := ⟨λ i, n ≤ i, λ i h,
(to_bool_iff _).2 $nat.le_succ_of_le$ (to_bool_iff _).1 h⟩


the inverse to f is noncomputable

Oh I like that!

#### Kevin Buzzard (Jun 11 2019 at 07:32):

With the reals I was going round in circles thinking "I need to have some sort of discontinuity, where a and b are a long way apart but f(a) and f(b) are close -- and yet aren't all computable functions continuous or some such nonsense?"

#### Kevin Buzzard (Jun 11 2019 at 07:33):

Here we have the discontinuity with f(1000000000000) and f(0) looking very close for the first gazillion entries, and yet f is still computable.

#### Kevin Buzzard (Jun 11 2019 at 07:36):

I am quite good at "silly little maths puzzles" but I am much less good at these ones, because I have been brought up resolutely classical, so it's hard for me to tell the difference between option and roption. But because these are different things to you, you can tell which is which; they all just look like "some countable set" to me.

#### Kevin Buzzard (Jun 11 2019 at 07:37):

This feels a bit like that embedding of nat into f : nat -> nat from yesterday. These are somehow all implementation issues, computationally equivalent (but with different running times). I've never thought about these sorts of problems before in my life.

#### Kevin Buzzard (Jun 11 2019 at 07:37):

I've spent 25 years living in a world where "computable" = "terminates instantly" and I had noncomputable theory at the top of the file anyway.

#### Mario Carneiro (Jun 11 2019 at 07:38):

I think of it topologically - roption looks like the set {1/n...} \cup {0}

#### Kevin Buzzard (Jun 11 2019 at 07:38):

It certainly does now.

#### Mario Carneiro (Jun 11 2019 at 07:39):

so while there is an additional element, it isn't "apart" from the others, unlike option where it's a disjoint union

#### Mario Carneiro (Jun 11 2019 at 07:40):

The dint example is actually computably isomorphic to int, because the constraint is that the functions are basically translations, so you don't get any of this "almost the same" business - you can just evaluate the function at any point to find out what it translates 0 to

#### Kevin Buzzard (Jun 11 2019 at 07:42):

Right. My point is that given dint you know where to put it -- "it's the same as int". But your notion of "the same" is more refined than mine -- for me, option and roption are the same, and for things like enat you know whether it's option nat or roption nat. For me, they're just all nat, because I've never been asked to think in this way.

#### Mario Carneiro (Jun 11 2019 at 07:42):

surely you have a notion of topological distinctness though

#### Kevin Buzzard (Jun 11 2019 at 07:43):

Oh definitely. I can certainly see that topologically they're not the same. I thought this was just an analogy though.

#### Mario Carneiro (Jun 11 2019 at 07:43):

like there are different topologies on the same underlying points

Sure.

#### Mario Carneiro (Jun 11 2019 at 07:43):

it's not an analogy at all, there is literally a topological structure

#### Kevin Buzzard (Jun 11 2019 at 07:43):

If you'd asked me to give you a continuous bijection with a discontinuous inverse, between two countable sets, I would have given you this instantly.

#### Kevin Buzzard (Jun 11 2019 at 07:44):

I could well have given you that exact example in fact. But I don't see what this has to do with computability.

#### Mario Carneiro (Jun 11 2019 at 07:44):

Domain theory is the branch of computer science that deals with putting topologies on all these types, such that the computable functions are continuous

#### Kevin Buzzard (Jun 11 2019 at 07:45):

So if I put the topology on nat so that the closed sets are nat and the finite sets, what does domain theory tell me about that?

#### Kevin Buzzard (Jun 11 2019 at 07:45):

That horrible non-Hausdorff topology is called the Zariski topology.

(sort-of)

#### Mario Carneiro (Jun 11 2019 at 07:48):

I don't think you can obtain all topologies via domain theory; it's usually phrased in terms of monotone functions on a chain complete partial order

#### Kevin Buzzard (Jun 11 2019 at 07:50):

So just these "orderish" ones like 0 union 1/n maybe.

#### Mario Carneiro (Jun 11 2019 at 07:50):

that said I can believe that your zariski example is representable

#### Kevin Buzzard (Jun 11 2019 at 07:51):

It's what the topology on Spec(Z) is.

#### Kevin Buzzard (Jun 11 2019 at 07:52):

What about if I say every even number is less than every odd number, but on even numbers and on odd numbers it's the usual <=?

#### Kevin Buzzard (Jun 11 2019 at 07:52):

the disjoint union of nat and nat

omega+omega

#### Kevin Buzzard (Jun 11 2019 at 07:52):

with the order topology.

#### Mario Carneiro (Jun 11 2019 at 07:55):

aha, you can do zariski

#### Mario Carneiro (Jun 11 2019 at 07:56):

you can take the representative of n to be a function which has 1 at a, a+n, a+2n, ... quotient over all choices of a

#### Mario Carneiro (Jun 11 2019 at 07:58):

the constraint is you should not ever be able to tell, given such a function, whether you actually have a representative of n or something else, but you can determine in finite time that two distinct elements are distinct

#### Mario Carneiro (Jun 11 2019 at 08:00):

The epistemological interpretation is that the open sets represent your knowledge of the function at some point in time; you can knock off finitely many natural numbers as not being the represented value so the open sets are cofinite

#### Mario Carneiro (Jun 11 2019 at 08:02):

It is possible to come up with arbitrary orders and interpret programming languages into those domains to get a funny model, but given a standard model you may not find your order represented

#### Kevin Buzzard (Jun 11 2019 at 08:02):

The "Furstenburg topology" is the topology on Z induced from the profinite topology on the completion of Z; the closed sets are the arithmetic progressions.

#### Kevin Buzzard (Jun 11 2019 at 08:03):

Anyway, this is just my mind wandering. Thanks for the roption example!

#### Mario Carneiro (Jun 11 2019 at 08:04):

it kind of reminds me of some quantum computations... you can calculate the period of a periodic function efficiently without being able to get particular values

#### Kevin Buzzard (Jun 11 2019 at 08:06):

That's how they factor large integers!

#### Mario Carneiro (Jun 11 2019 at 08:07):

right, I'm thinking of shor's algorithm

#### Mario Carneiro (Jun 11 2019 at 08:07):

maybe you can find a furstenburg topology in there

#### Mario Carneiro (Jun 11 2019 at 08:12):

Oh, the zariski example doesn't quite work, because you can determine n if you find a and then search for the next set value. But permuting the values is actually a much more effective approach. You let the representative of n be a bijection between nat and nat - {n} (quotient over all such). Then given any such function you can never find n, you can only eliminate possible candidates for n by enumerating the members

#### Mario Carneiro (Jun 11 2019 at 08:21):

Oh! I'm thinking too hard about this. The easy solution is to say that a representative is a monotone sequence of finsets whose union is nat - {n}

#### Mario Carneiro (Jun 11 2019 at 08:22):

and you can do the same trick to get the Furstenburg topology - a representative of n is a sequence of pairs (ai,di) such that ai = n (mod di) for all i, and such that n is uniquely determined by the full sequence

#### Reid Barton (Jun 11 2019 at 09:32):

The epistemological interpretation is that the open sets represent your knowledge of the function at some point in time; you can knock off finitely many natural numbers as not being the represented value so the open sets are cofinite

Exercise for Kevin: What familiar topology do you get appllying this to the entire type nat -> bool?

#### Kevin Buzzard (Jun 11 2019 at 09:53):

I've been busy writing https://xenaproject.wordpress.com/2019/06/11/the-inverse-of-a-bijection/

#### Kevin Buzzard (Jun 11 2019 at 09:54):

I'm going to guess that it's just the profinite topology on $2^\mathbb{N}$.

#### Kevin Buzzard (Jun 11 2019 at 09:55):

The dumb algorithms will only end up evaluating functions at finitely many places

#### Kevin Buzzard (Jun 11 2019 at 09:56):

So the issue seems to be whether there can be an algorithm which can end up evaluating functions at an arbitrarily large set of places and yet always be guaranteed to terminate.

#### Reid Barton (Jun 11 2019 at 09:59):

I think you can rule that out with a compactness argument

Or Konig's lemma

#### Reid Barton (Jun 11 2019 at 10:07):

So, in particular, pretty much any reasonable encoding of the p-adics will be assigned their usual profinite topology

#### David Michael Roberts (Jun 11 2019 at 12:53):

I'm not sure if someone raised this above, but the space of infinite bit strings is the Cantor space 2^\mathbb{N} with the product topology (which probably coincides with the profinite topology). This is a metric space, and you should think of computable things as being uniformly continuous functions. IIRC there is no uniformly continuous function that picks out the streams that eventually have a 1, as opposed to the ones that don't (or at least, this is the fable I tell myself in my head)

#### Kevin Buzzard (Jun 11 2019 at 13:08):

I'd just come back to this thread with some more questions and perhaps David has answered one.

So yes by the profinite topology I meant the product topology. I am a bit confused about the metric space claim. sure I can put a metric space structure on it -- but I am equally sure that I can put two different metric space structures on it such that the uniformly continuous functions on one do not coincide with the uniformly continuous functions on the other. Is a product of uniform spaces a uniform space? Isn't a continuous function from a compact space automatically uniformly continuous anyway?

Reid, I am a bit confused about the logic of things here. I don't want to start using compactness arguments or Konig's lemma yet -- they are mathsy things so they don't see the notion of computability; they might see the notion of continuity, but I thought that's what we were trying to prove.

The claim washing around here seems to be that computable functions from nat -> bool are continuous (or now we have this rival bid of uniformly continuous). So what about computable functions (nat -> bool) -> nat? What topology am I supposed to be putting on nat here? If the discrete topology, then continuous image of compact is compact so all continuous functions have finite image. Do all computable functions (nat -> bool) -> nathave finite image?

The general theorem can't be that the target always has the discrete topology though, becuase the identity function is a continuous function from nat -> bool which has infinite image.

What is going on here?

#### David Michael Roberts (Jun 11 2019 at 13:11):

In computable land, things are not so easy: https://link.springer.com/chapter/10.1007/11494645_3

#### David Michael Roberts (Jun 11 2019 at 13:13):

Also, it might be something like not functions from Cantor space but functions from functionals on Cantor space. It's a bit too late here for me, so I should look up some references tomorrow. Certainly work of Andrej Bauer and of Martin Escardo is relevant here.

#### David Michael Roberts (Jun 11 2019 at 13:14):

One more potentially relevant reference and I may come back to this tomorrow: https://www.jstor.org/stable/27590306?seq=1#page_scan_tab_contents

#### Reid Barton (Jun 11 2019 at 13:21):

So you asked whether every computable (total) function from nat -> bool to bool can only depend on the value of its argument at finitely many natural numbers.

#### Kevin Buzzard (Jun 11 2019 at 13:24):

Oh yes, that was a question I meant to flag up again. If I have a computable function (nat -> bool) -> nat then is there some B such that the computable function does not depend on the values of the function which are greater than B? Note that this is not true for (nat -> bool) -> (nat -> bool) so I am a bit bewildered about what's going on here.

#### Reid Barton (Jun 11 2019 at 13:25):

The argument is going to go something like this. Suppose F : (nat -> bool) -> bool is not of this form, that is, there is no N such that F is determined by the restriction of its argument f to numbers less than N. The only thing that F can do with f is evaluate it at various values. So suppose F starts out by evaluating f at some value i.

#### Kevin Buzzard (Jun 11 2019 at 13:25):

Aah, so the target is now bool? Is that always the target for these questions?

#### Reid Barton (Jun 11 2019 at 13:26):

f is going to return either tt or ff. Now in at least one of these two cases, F must still have the property that the result depends on infinitely many more values of f. (Otherwise, we could get a bound for the maximum index that F depends on.)

#### Reid Barton (Jun 11 2019 at 13:28):

Let's say it's tt, and then mentally set f i = tt and continue running the algorithm. It has to next check the value of f at a new index j.

#### Reid Barton (Jun 11 2019 at 13:29):

and again we can partially specify f in a way to ensure that F depends on infinitely many more of its values. (This is basically the proof of Konig's lemma happening here.)

#### Reid Barton (Jun 11 2019 at 13:30):

Furthermore we may as well assume j is different from i since evaluating f at i again doesn't help F.

#### Reid Barton (Jun 11 2019 at 13:31):

In this way we get an infinite sequence of constraints f i0 = b0, f i1 = b1, f i2 = b2 ...
Now choose a function f which satisfies all these constraints (this is a form of compactness), and run the algorithm for F on this f--it has to run forever, a contradiction because we assumed that the algorithm was total.

#### Reid Barton (Jun 11 2019 at 13:32):

If we removed random bits of the space nat -> bool, we might not be able to do the step where we picked f. For example, nat can be embedded within nat -> bool and then the argument would break down at that step

#### Kevin Buzzard (Jun 11 2019 at 13:33):

So if we stick to functions to bool we can guarantee they only query finitely many values, so they're continuous.

#### Reid Barton (Jun 11 2019 at 13:37):

If you have a semidecidable subset of nat -> bool then it's the union of the sets accepted by countably many functions (nat -> bool) -> bool (given by "run the semidecision procedure for $T$ steps, and return true if it accepts, otherwise false") and so it's an open subset.

#### Mario Carneiro (Jun 11 2019 at 20:02):

This proof still works for (nat -> bool) -> nat, without any changes. It doesn't work for (nat -> bool) -> (nat -> bool) because the values are now functions, which can delay the computation of f while still depending on infinitely many parts of it

#### Mario Carneiro (Jun 11 2019 at 20:03):

what you can say is that in any case, finitely many evaluations of f are performed before a value is produced

#### Kevin Buzzard (Jun 11 2019 at 20:16):

Sure in any run only finitely many evaluations occur. The question is whether there is a uniform bound independent of the function. Reid proved that this was true for functions to bool. What about functions to nat?

#### François G. Dorais (Jun 11 2019 at 20:22):

def enat := {f : nat → bool // ∀ n, f n = tt → f (n+1) = tt}

def f : nat → enat
| 0 := ⟨λ _, ff, λ n h, h⟩
| (n+1) := ⟨λ i, n ≤ i, λ i h,
(to_bool_iff _).2 $nat.le_succ_of_le$ (to_bool_iff _).1 h⟩


the inverse to f is noncomputable

Except that this is not a bijection! The statement function.surjective f is equivalent to ∀ (p : nat → bool), (∃ n, p n = tt) ∨ (∀ n, p n = ff) (provably in plain Lean) but the latter is a non-provable instance of the law of excluded middle. In fact, the inverse becomes definable in Lean with the (somewhat stronger) assumption [decidable (∃ n, p n = tt)].

To return to @Kevin Buzzard's original question, what is missing from lean to prove that every bijection is invertible is the _Principle of Definite Description_, which is also known as the _Principle of Unique Choice_. In Lean, the Axiom of Choice is formulated as:

axiom choice {α : Sort u} : nonempty α → α


The Axiom of Unique Choice can be formulated as follows:

axiom unique_choice {α : Sort u} [subsingleton α] : nonempty α → α


Given a function f : α → β, function.injective f yields Π (y : β), subsingleton { x : α // f x = y } and function.surjective f yields Π (y : β), nonempty { x : α // f x = y } and thus unique_choice can be used to define the inverse.

Unlike choice, which gives classical logic by Diaconescu's Theorem and hence many noncomputable functions nat → nat, unique_choice has no consequence on the logic of Prop and cannot be used to prove the existence of a noncomputable function nat → nat in Lean. It does have interesting properties on the type structure of Lean. The main consequence is that unique_choice allows Prop to eliminate into Type and since Prop is impredicative, this makes the whole hierarchy of types impredicative as well. So the real problem for inverting bijections is with predicativity rather than computability. Assuming unique_choice every bijection has an inverse, but @Mario Carneiro's example is still not invertible since it is not provably bijective.

#### Reid Barton (Jun 11 2019 at 20:23):

You can first prove that a computable function (nat -> bool) -> nat is bounded by the same kind of argument (otherwise we can construct an input for which the output exceeds N for every N).

#### Reid Barton (Jun 11 2019 at 20:27):

Or since we already proved that computable functions to bool are continuous, consider the open cover by the sets {f | F f = i} and take a finite subcover.

#### Kevin Buzzard (Jun 11 2019 at 20:38):

Except that this is not a bijection!

I can switch on some maths settings and then prove that it is, which surely means that it can't "not [be] a bijection" before -- it was just not provably a bijection or something.

#### François G. Dorais (Jun 11 2019 at 20:42):

But, for most of these settings, if you switch on those settings you can also prove that every bijection has an inverse!

#### Chris Hughes (Jun 11 2019 at 20:52):

em is weaker than full choice.

#### Chris Hughes (Jun 11 2019 at 20:52):

I don't think em implies bijections have an inverse.

#### Kevin Buzzard (Jun 11 2019 at 20:54):

Maths settings FTW

#### Mario Carneiro (Jun 11 2019 at 20:54):

My claim has always been in the context of assume all classical axioms but not noncomputable

#### Kevin Buzzard (Jun 11 2019 at 20:55):

It's interesting. I always regard all of this non-maths stuff (computability, classicality) as just "non-maths stuff", but I am slowly beginning to be able to distinguish these various bogs from one another.

#### Mario Carneiro (Jun 11 2019 at 20:55):

In constructive maths it is probably not possible, because a constructive proof that it is a bijection is basically an equiv

#### Kevin Buzzard (Jun 11 2019 at 20:56):

I liked David Roberts' comment on my blog post -- if you think of functions as relations then one can prove that the inverse is a "functional relation" -- and yet it still doesn't arise from a function.

#### Mario Carneiro (Jun 11 2019 at 20:56):

right, that's a good way to think about it

#### Kevin Buzzard (Jun 11 2019 at 20:56):

In ZFC and classical first order logic is there a notion of computability?

#### Kevin Buzzard (Jun 11 2019 at 20:56):

[indicating my still huge level of ignorance]

#### Kevin Buzzard (Jun 11 2019 at 20:57):

because I thought that in ZFC a function was the same as a functional relation.

#### Mario Carneiro (Jun 11 2019 at 20:58):

what you can say is that in any case, finitely many evaluations of f are performed before a value is produced

Sure in any run only finitely many evaluations occur. The question is whether there is a uniform bound independent of the function. Reid proved that this was true for functions to bool. What about functions to nat?

I mean that statement uniformly. For any computable closed term of (nat -> bool) -> A, there exists n such that the argument will be evaluated at most n times before the result becomes a value

#### Kevin Buzzard (Jun 11 2019 at 20:59):

I see. But the value itself can depend on other arguments (e.g. id evaluates nothing and depends on everything)

#### Mario Carneiro (Jun 11 2019 at 21:00):

id : (nat -> bool) -> (nat -> bool) does not evaluate the function f at all before returning f

#### Mario Carneiro (Jun 11 2019 at 21:00):

f is assumed to already be a value here (i.e. a lambda) since it was passed to id

#### Mario Carneiro (Jun 11 2019 at 21:01):

the difference is that the meaning of "value" depends on the type in question

#### Mario Carneiro (Jun 11 2019 at 21:01):

for nat -> bool, a value is something of the form \lam x : nat, e

#### Mario Carneiro (Jun 11 2019 at 21:01):

for bool, a value is either tt or ff, and for nat a value is succ $...$ succ 0

#### François G. Dorais (Jun 11 2019 at 21:02):

@Kevin Buzzard To be more precise with this last comment, it's totally fine to assume the full law of excluded middle in Prop. Since Prop can't eliminate into Type, you won't get any noncomputable functions out of that. But then you get into this awful scenario where you can prove the _existence_ of noncomputable functions nat → nat but you can't produce a single one: every closed term nat → nat is still computable. I find that scenario rather bizarre but I also like bizarre stuff... By the way, for the same reason, your question has a different answer if you ask for the _existence_ of an inverse rather than an actual term for the inverse.

#### Mario Carneiro (Jun 11 2019 at 21:03):

there are noncomputable closed terms, e.g. unguarded use of choice

#### François G. Dorais (Jun 11 2019 at 21:04):

@Mario Carneiro: Yes, that's my point. With choice every bijection has an inverse.

#### Mario Carneiro (Jun 11 2019 at 21:04):

I'm talking about classical + computable though, where you are allowed to use choice but only to prove a proposition

#### Mario Carneiro (Jun 11 2019 at 21:05):

in particular that means that if you only ask for existence of an inverse it's easy since you just use choice to construct a noncomputable function, and then the exists shields the noncomputability

#### François G. Dorais (Jun 11 2019 at 21:05):

Yes, then you can prove the _existence_ of an inverse but you can't get to the inverse without eliminating the proposition.

#### Mario Carneiro (Jun 11 2019 at 21:07):

In ZFC and classical first order logic is there a notion of computability?

No, except of course for the deep embedding, a.k.a the usual notion of computability by math/cs using turing machines or whatever

#### Kevin Buzzard (Jun 11 2019 at 21:08):

example (X Y : Type) (f : X → Y) (hf : function.bijective f) : ∃ g : Y → X, true :=
begin
sorry
end


I don't know how to prove this constructively :-(

#### Kevin Buzzard (Jun 11 2019 at 21:08):

The only constructor I know for exists is "just show me the function" and that's exactly what I can't do.

#### Mario Carneiro (Jun 11 2019 at 21:08):

the proof uses choice

#### Mario Carneiro (Jun 11 2019 at 21:09):

or at least unique_choice

#### Kevin Buzzard (Jun 11 2019 at 21:09):

oh I see, but it's still computable probably [goes to check]

#### Kevin Buzzard (Jun 11 2019 at 21:19):

import tactic.interactive

def equiv_thing (X Y : Type) (f : X → Y) (hf : function.bijective f) : ∃ g : Y → X, (∀ x, g (f x) = x) ∧ (∀ y, f (g y) = y) :=
begin
choose g hg using (λ y, hf.2 y),
use g,
split, swap, exact hg,
intro x, apply hf.1, exact hg _,
end


I love that choose tactic; it makes that argument so much easier than it used to be.

#### Kenny Lau (Jun 11 2019 at 21:20):

you can eta-reduce fun y, hf.2 y

#### Kevin Buzzard (Jun 11 2019 at 21:27):

Eta reduction is defeq for pi types but not for inductive tires

#### Mario Carneiro (Jun 11 2019 at 21:27):

did autocorrect change tyre to tire there?

#### Kevin Buzzard (Jun 11 2019 at 21:28):

Maybe it's bed time, I seem to have spent all day thinking about type theory

#### Mario Carneiro (Jun 11 2019 at 21:29):

eta reduction is defeq for inductive types, although sometimes lean gets confused

#### Mario Carneiro (Jun 11 2019 at 21:35):

hey, a reasonable application of axiom_of_choice:

def equiv_thing (X Y : Type) (f : X → Y) (hf : function.bijective f) : ∃ g : Y → X, (∀ x, g (f x) = x) ∧ (∀ y, f (g y) = y) :=
let ⟨g, hg⟩ := classical.axiom_of_choice hf.2 in
⟨g, λ x, hf.1 (hg _), hg⟩


#### Reid Barton (Jun 11 2019 at 21:38):

Personally I've always found choice philosophically dubious, and I'd much prefer to stick to axiom_of_choice plus unique_choice wherever possible

#### Kevin Buzzard (Jun 11 2019 at 21:39):

Personally I've always found choice philosophically dubious, and I'd much prefer to stick to axiom_of_choice plus unique_choice wherever possible

I put that sort of comment in the same box as "personally I find castling philosophically dubious in chess". Isn't it all a game?

#### Reid Barton (Jun 11 2019 at 21:41):

It's another part of the "mathematicians' rules of conduct" I guess. We don't make definitions that depend on which element choiceproduces.

#### Kevin Buzzard (Jun 11 2019 at 21:41):

eta reduction is defeq for inductive types, although sometimes lean gets confused

The proof of complex.eta is not rfl, it's cases, rfl

#### Reid Barton (Jun 11 2019 at 21:42):

If you replace choice by axiom_of_choice+unique_choice then you're forced to prove, for example, that the dimension of a vector space does not depend on the choice of basis

#### Mario Carneiro (Jun 11 2019 at 21:52):

oh, right there are multiple things called eta

#### Mario Carneiro (Jun 11 2019 at 21:52):

I'm not sure what I thought you meant

#### Mario Carneiro (Jun 11 2019 at 21:53):

axiom_of_choice + unique_choice makes type theory look basically like ZFC

#### Mario Carneiro (Jun 11 2019 at 22:05):

However, it doesn't really affect proofs very much, you can just have a long lived hypothesis variable [has_choice] and do this:

universe u
class has_choice : Type u := (f : ∀ α : Sort u, nonempty α → α)

theorem unchoice {p : Prop} (H : ∀ [has_choice.{u}], p) : p :=
let ⟨F, _⟩ := classical.axiom_of_choice (λ α : Sort u,
show ∃ f : nonempty α → α, true, from
let ⟨f, hf⟩ := classical.axiom_of_choice (λ h : nonempty α,
exists_true_iff_nonempty.2 h) in ⟨f, trivial⟩) in
@H ⟨F⟩


#### Mario Carneiro (Jun 11 2019 at 22:07):

I think choice is the idea that since doing this is needless boilerplate we may as well just pick a global choice function

#### Reid Barton (Jun 11 2019 at 22:18):

It's harmless for proofs but not for definitions

#### Mario Carneiro (Jun 11 2019 at 22:24):

for definitions, you can just put [has_choice] in the arguments to the definition

#### François G. Dorais (Jun 11 2019 at 23:03):

em is weaker than full choice.

Sorry @Chris Hughes, I think an earlier reply was partly mistakenly written to Kevin instead of you. You are totally right that EM for Prop is very weak and almost harmless. However, it becomes dangerous in combination with unique_choice, even locally!

section
parameter unique_choice {α : Type} [subsingleton α] : nonempty α → α
variables {p : Prop} (h : p ∨ ¬ p)

def nonempty_decidable_of_em : nonempty (decidable p) :=
or.elim h
(λ h, nonempty.intro (decidable.is_true h))
(λ h, nonempty.intro (decidable.is_false h))

#print decidable.subsingleton -- show instance

def decidable_of_em : decidable p := unique_choice (nonempty_decidable_of_em h)

end


#### Mario Carneiro (Jun 11 2019 at 23:23):

what's wrong with that? A mathematician would think that's fine

#### Mario Carneiro (Jun 11 2019 at 23:23):

it's basically saying that if p then 1 else 0 exists

#### Mario Carneiro (Jun 11 2019 at 23:25):

which is a perfectly fine ZFC-ish thing to do

#### Mario Carneiro (Jun 11 2019 at 23:25):

it's just not computable

#### François G. Dorais (Jun 11 2019 at 23:28):

Yes, 100% of mathematicians (including me!) believe in Unique Choice. But this is not about mathematics, it's about the type theory of Lean. The problem is that it systematically breaks predicativity, even locally. So if Lean insists on predicativity of Type, Unique Choice is not an option.

#### François G. Dorais (Jun 11 2019 at 23:33):

For what it's worth, I think Lean should have an "impredicative mode" where Unique Choice is true (but not full choice). This mode would make a lot of universe issues wash away, but it may have other consequences where ignoring props would trickle up to ignoring some types... This option needs a deeper look but it would match better with mathematics where types are also occasionally ignored.

#### François G. Dorais (Jun 11 2019 at 23:44):

This trickling, combined with simpler universe constraint calculations, might make typing undecidable. That's the main implementation issue.

#### Mario Carneiro (Jun 11 2019 at 23:49):

Do you still want computability in your impredicative mode?

#### Mario Carneiro (Jun 11 2019 at 23:49):

because that basically means you can't erase anything

#### Mario Carneiro (Jun 11 2019 at 23:50):

so you lose the ability to have "programs with assertions"

#### Mario Carneiro (Jun 11 2019 at 23:50):

This is what actually happens in most HoTT libraries, but I don't think it's particularly practical for computation

#### Mario Carneiro (Jun 11 2019 at 23:52):

unique_choice on its own doesn't make anything undecidable. But perhaps you want a computation rule such as unique_choice _ _ <a> ~> a

#### Mario Carneiro (Jun 11 2019 at 23:53):

I don't see it fixing any universe issues, although computation may end up doing weird things with universes

#### François G. Dorais (Jun 12 2019 at 00:04):

Yes, that mode is for mathematics only. To obtain a computation, we would need to remove the mode and resolve the predicativity issues manually. In theory, this is possible but with the impredicative mode, Lean could accept things that are actually beyond what plain Lean can handle, so there is no choice but to do this process manually.

#### Mario Carneiro (Jun 12 2019 at 00:05):

what are the impredicative constructions you envision?

#### Mario Carneiro (Jun 12 2019 at 00:06):

lean can already do impredicative stuff with Prop

#### Mario Carneiro (Jun 12 2019 at 00:07):

if you don't care about computation, then it seems like you can just have choicein Type and just ignore noncomputable

#### François G. Dorais (Jun 12 2019 at 00:19):

That doesn't work because noncomputable can't be eliminated, any derived term in Type* is noncomputable as well and must be marked that way. This can be mitigated by using type classes, but that only covers standardized ways of eliminating noncomputable axioms whereas the full process requires some creativity.

#### François G. Dorais (Jun 12 2019 at 00:25):

The larger issue is that Math Computable and Lean Computable mean different things. In mathematics, computable is a computation that _happens_ to always terminate, but plain Lean requires more. The mode I'm proposing is an in-between, where some principles such as unique choice are accepted as rules (because they are admissible) but not necessarily as axioms. Then the admissible rules could be eliminated manually, if needed, to get a plain term.

#### Mario Carneiro (Jun 12 2019 at 00:32):

noncomputable can't be eliminated but it can be ignored

#### Mario Carneiro (Jun 12 2019 at 00:33):

actually you can trivially make noncomputable types computable

#### Mario Carneiro (Jun 12 2019 at 00:35):

axiom foo : Type
def foo' : Type := id foo


#### Mario Carneiro (Jun 12 2019 at 00:39):

The larger issue is that Math Computable and Lean Computable mean different things. In mathematics, computable is a computation that _happens_ to always terminate, but plain Lean requires more.

Actually, I would argue that lean's (non)noncomputable + classical axioms matches math computable pretty well. Here "happens to terminate" is expressed as "classically proven to terminate", which is not exactly the same because of the gap between provability and truth, but it's indistinguishable from within the system

#### Mario Carneiro (Jun 12 2019 at 00:43):

unique_choice is not admissible as a computable axiom, without changing the interpretation of Prop, but it is admissible as a noncomputable axiom if you think ZF is reasonable. Even choice is admissible as a noncomputable axiom if you think ZFC + some universes is reasonable

#### François G. Dorais (Jun 12 2019 at 00:52):

I think unique_choice might still be admissible as a _rule_. I still don't know how it plays with inductive construction, which is just another bunch of rules (if you want to think about them that way) but rules aren't necessarily compatible.

#### Mario Carneiro (Jun 12 2019 at 00:53):

what do you mean by "as a rule"?

#### François G. Dorais (Jun 12 2019 at 00:56):

A deduction rule rather than as an axiom (an actual constant).

#### Mario Carneiro (Jun 12 2019 at 00:56):

I don't see any way that a term constructor could end up differing in any essential way from a constant given all the other stuff in DTT

#### Mario Carneiro (Jun 12 2019 at 00:57):

If you allow a context in your rule, then I will just lambda abstract and build the constant

#### François G. Dorais (Jun 12 2019 at 00:58):

Proofs are finite. Axioms are more powerful than rules.

#### Mario Carneiro (Jun 12 2019 at 00:58):

Unless you put an unusual constraint on the rule, it's equivalent

#### Mario Carneiro (Jun 12 2019 at 00:59):

so I'm asking what the constraint is

#### Mario Carneiro (Jun 12 2019 at 01:00):

like usually stuff like and.left and or.elim are done as rules, but because DTT has lambda and app it makes no difference to introduce them as constants instead

#### François G. Dorais (Jun 12 2019 at 01:36):

The actual rule for Unique Choice would require a new subsingleton judgment and the obvious accompanying rules (e.g. two elements of a subsingleton are definitionally equal, Pi's of subsingletons are subsingletons, and the unique choice rule). In plain Lean, these subsingletons could be universe ranked and all props would be automatic subsingletons. In the impredicative case, there could be a single subsingleton judgment, which would make unique choice work. I don't know if this is actually sound for Lean type theory. I think it would definitely make Lean less lean.

#### Mario Carneiro (Jun 12 2019 at 01:42):

oh, you want an assumption of defeq?

#### François G. Dorais (Jun 12 2019 at 01:43):

Yes, as it should be for mathematics...

#### Mario Carneiro (Jun 12 2019 at 01:43):

Is it possible to prove something is a subsingleton, or is it a syntactic judgment?

#### Mario Carneiro (Jun 12 2019 at 01:43):

because if you can prove it then this makes the whole theory extensional

#### François G. Dorais (Jun 12 2019 at 01:44):

It's just syntactic, that's the whole point. That way it could be eliminated from proof terms with some creative work.

#### Mario Carneiro (Jun 12 2019 at 01:44):

so then what is a subsingleton that isn't already a prop?

#### François G. Dorais (Jun 12 2019 at 01:56):

Well, this is going into speculation since I haven't worked out whether any of this makes sense for lean type theory. From the front end point of view, in the impredicative case, the subsingleton judgment would take the place of Prop and (hopefully) universe levels of subsingletons would simply wash away entirely. That would make the Lean front end essentially the same except that Props would eliminate into Type automatically.

#### François G. Dorais (Jun 12 2019 at 01:58):

The predicative case is more complicated, it would probably need a hierarchy of Prop* that parallels Type* and what eliminates where would be complicated. This is probably not worth it, but unique choice might still work.

#### François G. Dorais (Jun 12 2019 at 02:05):

Because subsingletons (aka props) are judgments, they can be tracked much better even in the impredicative case, which makes it plausible to undo this addition and "manually" work out a plain Lean term from an extended one. It's plain that adding this is sound because of the set theoretic model. Computational soundness is less clear but not bad. The one thing that worries me a lot is quotients, which can be used to produce subsingletons out of nowhere...

#### François G. Dorais (Jun 12 2019 at 02:07):

Then again, subsingleton judgments might give a better way of defining quotients...
This all needs deeper thinking...

#### Mario Carneiro (Jun 12 2019 at 02:35):

I'm still confused how (in the impredicative case) you have done anything different from renaming Prop to subsingleton

#### Mario Carneiro (Jun 12 2019 at 02:36):

Lean's subsingleton would still have to exist as a separate thing, since there are things that are only proven to be subsingletons, and AFAICT this doesn't make that part any different

#### François G. Dorais (Jun 12 2019 at 02:37):

Except for universe level computations and elimination into type?

#### Mario Carneiro (Jun 12 2019 at 02:37):

universe level computation meaning what

#### Mario Carneiro (Jun 12 2019 at 02:38):

I see, elimination into type meaning it's proof relevant?

#### François G. Dorais (Jun 12 2019 at 02:38):

They disappear into subsingletons, which makes impredicativity happen and unique choice trivial.

#### Mario Carneiro (Jun 12 2019 at 02:41):

Do you still expect em or axiom_of_choice?

#### Mario Carneiro (Jun 12 2019 at 02:43):

as you have pointed out this lets you build a decidable p, which breaks canonicity (to be fair, it's already broken but this makes it even easier)

#### Mario Carneiro (Jun 12 2019 at 02:49):

And actually this does break decidability of the typing relation as well, because if you have something like X := if RH then 1 else 0 then if RH is provable we have prop_decidable RH == of_true proof_of_RH (defeq because decidable is a subsingleton, and we can set to be syntactically so) and hence X == 1 definitionally

#### François G. Dorais (Jun 12 2019 at 02:49):

No, I don't. I expect terms that I can use but that other people can prove. If other people want AC, that's fine but I can't use their stuff for my work. Same goes for RH.

#### Mario Carneiro (Jun 12 2019 at 02:51):

My point being that whether this term X is defeq to 1 or not actually depends on whether a proof of RH exists

#### Mario Carneiro (Jun 12 2019 at 02:51):

I could write theorem proof_of_RH : X = 1 := rfl and lean has to go find me a proof of RH

#### Mario Carneiro (Jun 12 2019 at 02:55):

yeah, I'm becoming increasingly convinced that unique_choice + definitional subsingleton will totally break the type system

#### Mario Carneiro (Jun 12 2019 at 02:56):

unless you go full extensional, but lean needs more interaction modes for that

#### François G. Dorais (Jun 12 2019 at 02:56):

Yes, that's the issue: at some point typeability becomes undecidable. This is almost unavoidable in an impredicative system. However, this is where the creativity I mentioned earlier comes into play. To make this into a computable term, I have to decide RH...
But the main point is that with a closed term in this impredicative system, I can isolate a finite number of proofs to resolve (with zero implication that I can).

#### François G. Dorais (Jun 12 2019 at 02:59):

It's quite possible that my proposal goes too far close to extensional type theory. My main goal is to go as far as possible in that direction without breaking anything significant.

#### Mario Carneiro (Jun 12 2019 at 02:59):

The problem isn't merely that there are noncomputable things, it's the part where noncomputable things "infect" defeq so that you can't decide types

#### Mario Carneiro (Jun 12 2019 at 03:00):

it means that axiom is not safe in this system

Exactly.

#### François G. Dorais (Jun 12 2019 at 03:01):

Definitely. (But non-propositional constants are already unsafe.)

#### Mario Carneiro (Jun 12 2019 at 03:01):

To be fair, that's kind of a weird requirement; most mathematicians would not be surprised that you can get garbage if you add arbitrary axioms, but you can't break defeq in lean even then

#### Mario Carneiro (Jun 12 2019 at 03:02):

I think it's important for unique_choice to work that the proof of nonempty is proof relevant

#### Mario Carneiro (Jun 12 2019 at 03:03):

being able to defeq change "proofs" around leads to lots of defeq things in Type, which is bad

#### François G. Dorais (Jun 12 2019 at 03:03):

A proof relevant version of nonempty would make unque choice trivial.

#### Mario Carneiro (Jun 12 2019 at 03:04):

not exactly trivial; it might be a proof relevant subsingleton

#### Mario Carneiro (Jun 12 2019 at 03:04):

I mean it's basically trunc at that point

#### François G. Dorais (Jun 12 2019 at 03:04):

It is, which makes it trivial.

#### Mario Carneiro (Jun 12 2019 at 03:05):

I mean it implies the existence of quotient types and so on

#### Mario Carneiro (Jun 12 2019 at 03:05):

but that's all in lean already so maybe it's not impressive

#### François G. Dorais (Jun 12 2019 at 03:06):

I'm always assuming quotients. That's 99% of why Lean is the best.

#### Mario Carneiro (Jun 12 2019 at 03:06):

Part of my masters thesis was the discovery that even the very limited form of large elimination allowed in lean (to support acc and eq) causes problems

#### Mario Carneiro (Jun 12 2019 at 03:07):

the large elimination rule is all about reasoning that an inductive type is "basically a subsingleton"

#### Mario Carneiro (Jun 12 2019 at 03:07):

https://github.com/digama0/lean-type-theory/releases

#### Mario Carneiro (Jun 12 2019 at 03:09):

section 3.1 is about how acc causes undecidability of the typing relation

#### François G. Dorais (Jun 12 2019 at 03:09):

I see. I had read an earlier version but I see that there are new pieces I need to read. Thanks!

#### David Michael Roberts (Jun 12 2019 at 09:26):

OK, so here's a good discussion about the Cantor space and the property I was trying to think of, called 'searchability'

https://mathoverflow.net/a/330699/4177

This is 'inside the effective topos', but you can think of it as being in 'computable land' (or, apparently, 'Type I computability'). Essentially, there is no computable function 2^N \to 2 = {0,1} that on input f:N\to 2 outputs 1 if \exists n with f(n)=1 and outputs 0 otherwise.

#### David Michael Roberts (Jun 12 2019 at 09:27):

Perhaps ironically, I'm examining a thesis where the author would have done well to mention this stuff, but is coming from a rather different background, so seems unaware of it, so it's been on my mind, and I'm glad I needed to look up a good discussion on this stuff.

#### Mario Carneiro (Jun 12 2019 at 12:00):

I don't think this summary is correct. It is all very confusing to me, but I think Andrej's argument only shows that in the internal logic of the effective topos there is no function which provably has the desired property. But in the original article http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ (on Andrej's own blog), there is demonstrated a program that does exactly that! I think the caveat is that one cannot prove that this program actually works from within the system.

#### Reid Barton (Jun 12 2019 at 12:24):

It's not really clear to me in what sense the functions in that blog post are functions except that you can program them in Haskell and they work

#### Mario Carneiro (Jun 12 2019 at 12:28):

That seems to be strong evidence that they are computable functions

#### Mario Carneiro (Jun 12 2019 at 12:29):

what's not clear is whether they are total, but I can believe that as long as the input functions are computable, a modulus of continuity exists so it should halt

#### Reid Barton (Jun 12 2019 at 12:30):

Right, the question is what happens when the input function is not computable, but it's not clear that this question is even meaningful

#### Mario Carneiro (Jun 12 2019 at 12:33):

of course, these functions are not allowed

#### Mario Carneiro (Jun 12 2019 at 12:34):

Obviously we can't assert this property, but we can observe that the function always halts from the meta level

#### Mario Carneiro (Jun 12 2019 at 12:34):

but that does mean that lean can't prove that it halts

Last updated: May 18 2021 at 16:25 UTC