Zulip Chat Archive

Stream: new members

Topic: mathlib & constructivity


view this post on Zulip Scott Olson (Sep 25 2018 at 04:57):

is there a standard library structure for isomorphisms, like this type in Idris? https://github.com/idris-lang/Idris-dev/blob/bae730a7ffaeae09a835a35bac132c141f3b50b3/libs/base/Control/Isomorphism.idr#L10-L16

i'm not sure what name to search for

view this post on Zulip Simon Hudon (Sep 25 2018 at 04:58):

In mathlib, you may want data.equiv.basic

view this post on Zulip Simon Hudon (Sep 25 2018 at 04:58):

https://github.com/leanprover/mathlib/blob/master/data/equiv/basic.lean

view this post on Zulip Scott Olson (Sep 25 2018 at 05:15):

thanks, that looks like what i want

that brings me to another question, though... should i be using mathlib, in general? is it basically just expected that most people will be using it?

view this post on Zulip Simon Hudon (Sep 25 2018 at 05:19):

Most people use mathlib because it's the largest repository of definitions and theorems in Lean and it keeps growing. Most importantly it has a lot of useful stuff

view this post on Zulip Mario Carneiro (Sep 25 2018 at 05:19):

That is certainly the intent... it is like the standard library of most programming languages

view this post on Zulip Scott Olson (Sep 25 2018 at 06:59):

is mathlib generally constructive or classical? or at least, does it clearly delimit which things depend on classical axioms? curious if i'll have to "wary" and check with #print axioms

view this post on Zulip Simon Hudon (Sep 25 2018 at 07:02):

You'll have to be wary. An effort is made to label classical theorems but people still use them pretty loosely

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:02):

mathlib is mostly classical. In particular, we only worry about constructivity in so far as it avoids the noncomputable marking. In any props or theorems we use AC freely

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:04):

There really isn't any point in being "wary" with #print axioms, because all you will achieve by doing that is get yourself in a tizzy about the many unnecessary uses of AC. Suffice it to say it is used in many difficult to avoid places in the foundation, some of which are in lean core and so are not even accessible to mathlib

view this post on Zulip Scott Olson (Sep 25 2018 at 07:04):

is there a discussion somewhere on the pros and cons of being classical for something like mathlib or just Props in general?

view this post on Zulip Scott Olson (Sep 25 2018 at 07:05):

the mathlib docs i've found so far just don't mention it

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:05):

We've had the discussion off and on for a while. Lean 2 made a concerted effort to be both constructive and classical

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:06):

At the beginning I held out hope that we could avoid AC when unnecessary, but at this point it's clear this isn't going to happen

view this post on Zulip Simon Hudon (Sep 25 2018 at 07:07):

I wonder if that's part of why mathlib was able to move quickly too

view this post on Zulip Scott Olson (Sep 25 2018 at 07:08):

i don't have much understanding of the implications of using such axioms in a system like Lean. i understand noncomputable prevents even bytecode, but any axioms at all prevent the term from evaluating to a normal form, and i'm curious if that can cause problems in practice

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:09):

We don't evaluate proofs at all in practice

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:09):

it doesn't matter if they are classical or not because they aren't programs

view this post on Zulip Scott Olson (Sep 25 2018 at 07:10):

that was my thinking for Prop, but i haven't been able to find much documentation talking about this point

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:10):

The only mechanism we have for evaluating proofs is #reduce and it falls over on all but the most trivial examples

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:10):

I guess there isn't much docs on this

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:11):

The VM evaluates anything that is not a Prop and is not noncomputable

view this post on Zulip Simon Hudon (Sep 25 2018 at 07:11):

When computation is involved, you really need to look at defs that are in Type 0 and over. Then an effort is often made to be efficient

view this post on Zulip Scott Olson (Sep 25 2018 at 07:13):

that makes sense, thanks for all the responses

view this post on Zulip Simon Hudon (Sep 25 2018 at 07:13):

:+1:

view this post on Zulip Scott Olson (Sep 25 2018 at 07:14):

i realized while talking to a friend just now that an interesting argument in favor of using fewer axioms is that it makes the proof potentially more "portable" to different formalisms, but that's somewhat aspirational and lacking it doesn't block anything in mathlib in the meantime

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:14):

Unfortunately, the axioms that really prevent portability of lean proofs aren't turn-off-able

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:15):

Most systems have some equivalent of the axiom of choice, but few have inductive types and a hierarchy of universes

view this post on Zulip Kevin Buzzard (Sep 25 2018 at 07:27):

i realized while talking to a friend just now that an interesting argument in favor of using fewer axioms is that it makes the proof potentially more "portable" to different formalisms, but that's somewhat aspirational and lacking it doesn't block anything in mathlib in the meantime

I'm a pure mathematician (as are several other people here) and one of the things that attracted me to Lean is precisely the attitude that "we will do maths like regular pure mathematicians do" (i.e. assume things like the axiom of choice, which in my circles is regarded as "just another axiom, with no particular reason to fuss about it".)

view this post on Zulip Sean Leather (Sep 25 2018 at 07:30):

I'm a pure mathematician (as are several other people here) and one of the things that attracted me to Lean is precisely the attitude that "we will do maths like regular pure mathematicians do" (i.e. assume things like the axiom of choice, which in my circles is regarded as "just another axiom, with no particular reason to fuss about it".)

On the other hand, some of the things that attracted me to Lean included the ability to do constructive mathematics, the nice syntax, a fast theorem prover, and a comprehensive library. :slight_smile:

view this post on Zulip Scott Olson (Sep 25 2018 at 07:36):

i figured some of what i said might have given away my friend's and my bias towards constructive type theories :P

i can see why Lean attracted pure mathematicians who might have otherwise used Coq or similar, though. the experience out of the box with Lean in VSCode is the best i've seen from any theorem prover

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:41):

I am also attracted to constructive mathematics generally, but the pure mathematicians have worn me down. :) I realize now that lean is not remotely geared towards limiting its axiom strength, and if you want a system for playing with axioms you should look elsewhere. "Having few axioms" only means having few interesting subsystems, and none of the available subsystems are recognizable to traditional mathematicians except possibly intuitionistic type theory

view this post on Zulip Simon Hudon (Sep 25 2018 at 07:42):

@Sean Leather how inconvenient is it for you that mathlib makes such liberal use of classical axioms?

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:42):

Instead, it seems much more likely that lean will be able to support doing logic at the meta level, which is something that few systems can currently do well. This approach is much more flexible, of course, with regards to its axioms and with the permissible methods of proof

view this post on Zulip Sean Leather (Sep 25 2018 at 07:42):

I haven't had any issues so far. I'm not even sure where I would run into any.

view this post on Zulip Scott Olson (Sep 25 2018 at 07:43):

i figure i'll just adjust my expectations of what exactly i will play with in lean, but it will still be suitable for a lot of the stuff i want to experiment with

view this post on Zulip Sean Leather (Sep 25 2018 at 07:43):

The only thing is this output:

#print axioms
quot.sound :  {α : Sort u} {r : α  α  Prop} {a b : α}, r a b  quot.mk r a = quot.mk r b
classical.choice : Π {α : Sort u}, nonempty α  α
propext :  {a b : Prop}, (a  b)  a = b

view this post on Zulip Simon Hudon (Sep 25 2018 at 07:43):

Is your requirement that functions be computable or actually to avoid the axioms?

view this post on Zulip Sean Leather (Sep 25 2018 at 07:44):

Computable, I suppose. I don't do anything actively to avoid axioms, but I don't think I use anything that does use the axiom of choice.

view this post on Zulip Scott Olson (Sep 25 2018 at 07:45):

#print axioms <name> will list the axioms used (transitively) for the given thing

view this post on Zulip Scott Olson (Sep 25 2018 at 07:45):

but as we discussed, this shouldn't be a problem in the bodies of proofs that will never need to be evaluated or examined by other proofs

view this post on Zulip Sean Leather (Sep 25 2018 at 07:46):

#print axioms <name> will list the axioms used (transitively) for the given thing

When I create an empty file, #print axioms shows what I wrote above. :smile:

view this post on Zulip Scott Olson (Sep 25 2018 at 07:47):

yeah, #print axioms just prints the axioms that are currently in scope

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:47):

Can anyone come up with a reasonable (not completely contrived) example of a computable function that uses AC/LEM in its definition?

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:55):

I will amend "not completely contrived" to not eliminable, in the sense that there isn't a way to write the same function without the axiom, or at least it's not easy to do so

view this post on Zulip Kevin Buzzard (Sep 25 2018 at 07:56):

on nat?

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:57):

sure, I doubt it makes a difference but nat -> nat is a fine target

view this post on Zulip Kevin Buzzard (Sep 25 2018 at 07:57):

I'm sure you're right but I'm such a noob at this sort of thing. A year ago I wouldn't even have been able to formalise the question rigorously.

view this post on Zulip Mario Carneiro (Sep 25 2018 at 07:58):

To give a hint on why it's even possible: nat.find will calculate the smallest value satisfying a predicate, given only a proof that there is such a value (in Prop). This proof can rely on any axioms, and the function will still be computable

view this post on Zulip Kevin Buzzard (Sep 25 2018 at 07:58):

What about f(n)=1 if Fermat's Last Theorem is true and 0 otherwise? It's completely contrived but I'm trying to get the hang of the question. All known proofs of FLT use AC.

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:00):

That won't work because f is just the constant function 1, it doesn't need any axioms for its definition

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:01):

But I think you are on the right track. Can you think of any forall exists theorem on nat that relies on AC?

view this post on Zulip Simon Hudon (Sep 25 2018 at 08:02):

I don't know how to formalize that statement but it seems like a computable function like you described cannot be constructed

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:07):

Here is an example that relies on the input being in a nonoptimal form: if the input is a function f : nat -> nat which is not the constant zero function, then you can computably find a nonzero nat in the range of f

view this post on Zulip Simon Hudon (Sep 25 2018 at 08:10):

That's true. I stand corrected

view this post on Zulip Kevin Buzzard (Sep 25 2018 at 08:12):

What about f(n)=1 if Fermat's Last Theorem is true and 0 otherwise? It's completely contrived but I'm trying to get the hang of the question. All known proofs of FLT use AC.

So by "computable" you mean "externally provable to be equal to a certain given fixed computable function", rather than "provable in Lean with/without AC to be equal to a certain given fixed computable function"

view this post on Zulip Kevin Buzzard (Sep 25 2018 at 08:13):

What about f(n)=1 if RH is true and 0 otherwise? Don't I need LEM to define this?

view this post on Zulip Kevin Buzzard (Sep 25 2018 at 08:13):

I'm still struggling to move away from the "contrived" part, as you can see ;-)

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:17):

If you pick something which is definitely not decidable, or not known to be decidable like RH, then the function won't be computable either. By "computable" I mean "passes lean's noncomputable check"; you can't write def f := if RH then 1 else 0 because RH is not decidable

view this post on Zulip Scott Olson (Sep 25 2018 at 08:18):

yeah, that would specifically require the classical instance for decidable that uses LEM internally, which is noncomputable, which forces f to be noncomputable

view this post on Zulip Kevin Buzzard (Sep 25 2018 at 08:18):

Here is something much less contrived but I am much less clear about whether it fits into the scope of this question. Let's say a pure mathematician proves that for every g>=2 there is a computable upper bound B(g)B(g) for the number of rational points on a smooth projective curve of genus g over the rationals, and their proof uses a bunch of algebraic geometry and AC / LEM everywhere. I suspect I could find arithmetic geometers who were prepared to conjecture that this mathematical statement was true. If this result got proved, and it turned out that a deep theorem implied that B(g)=10000gB(g)=10000*g, this would not be an example, right? :-/

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:19):

You can write def f := if FLT then 1 else 0 only if you have already provided a computable proof of decidable FLT, which will involve a proof of FLT. This falls afoul of the second restriction because then you could just replace the definition of f with 1

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:20):

You are right, this is an interesting situation. If we know a bound on the function then we can skip the clever maths and just use the bound

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:21):

Somehow it has to be an existence theorem with no bound

view this post on Zulip Edward Ayers (Sep 25 2018 at 08:26):

How about f(n) is 1 if the nth turing machine halts and 0 otherwise? If I'm not mistaken the proof that f is total requires LEM.

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:27):

I have been thinking about examples like that, but again it needs to be computable

view this post on Zulip Edward Ayers (Sep 25 2018 at 08:27):

But that might be because I've never seen a constructive proof of halting problem

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:28):

To define that function you have to know whether the nth turing machine halts

view this post on Zulip Edward Ayers (Sep 25 2018 at 08:30):

Ah in that case I think that it's impossible.

view this post on Zulip Edward Ayers (Sep 25 2018 at 08:33):

As in you can always rewrite the function to not use AC

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:34):

Here's another way to put it: Find computable predicates p(n), q(m,n) such that if p(n) is true then there exists an m such that q(m,n), but there is no computable upper bound on the least satisfying instance

view this post on Zulip Scott Olson (Sep 25 2018 at 08:37):

so with nat.find we could find the least nat satisfying some predicate while only proving this search will actually terminate with, for example, a proof by contradiction (the kind that requires classical double negation elimination)?

view this post on Zulip Edward Ayers (Sep 25 2018 at 08:37):

I can just run the q machine on each value of m = 0,1,2,... in turn. Since there exists an m where q(m,n) works, that program will halt. Right?

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:38):

yes, that's the idea

view this post on Zulip Edward Ayers (Sep 25 2018 at 08:38):

So it's impossible (to find such computable predicates)

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:38):

that's the computable function

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:42):

hm, you may be right. The very constraint that makes it lean-computable will also produce a computable upper bound, namely this function

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:44):

but I think maybe "computable upper bound" isn't what I want either; it needs to be an upper bound that you can't prove using lean without AC

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:44):

you can't use this function as a proof because it requires a proof that it will halt to run

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:46):

If we use something weaker than DTT, it should be possible to use some Ackermann-like function here

view this post on Zulip Edward Ayers (Sep 25 2018 at 08:47):

Ok I think I see what you mean now. You want a pair p(n), q(m,n) where the existence of a satisfying mis proved using AC or LEM.

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:48):

exactly

view this post on Zulip Johan Commelin (Sep 25 2018 at 08:51):

Can you prove that such a function exists using AC?

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:52):

You can use whatever methods you like to prove the existence of such p and q, but they have to be computable functions

view this post on Zulip Johan Commelin (Sep 25 2018 at 08:54):

Ok, I should have put more emphasis on you in my last post (-;

view this post on Zulip Johan Commelin (Sep 25 2018 at 08:54):

I have no clue at all about all this computability stuff.

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:55):

I don't have a solution to this puzzle

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:55):

but I believe it is possible

view this post on Zulip Edward Ayers (Sep 25 2018 at 08:56):

I am still not satisfied that the question is well posed. If I found a p and q with that property. I could take the AC proof, throw it away and replace it with a machine that just tries all m. Eventually it would find the m (which I know but Lean doesn't) and Lean would use that. But then I guess my new program would have to run in unsafe mode.

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:57):

For a fixed n you can do that, but I don't think you can do that for all n

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:57):

i.e. if p(5) is true and it turns out that q(100,5) is the satisfying instance, then you can use an upper bound of 100 in the construction

view this post on Zulip Johan Commelin (Sep 25 2018 at 08:57):

Mario, do you want a proof that can only prove the upper bound under the assumption of LEM/AC?

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:57):

right

view this post on Zulip Johan Commelin (Sep 25 2018 at 08:58):

Or is it enough that we know no such proof.

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:58):

Even that would be nice

view this post on Zulip Mario Carneiro (Sep 25 2018 at 08:58):

I'm worried that since no axioms lean has the same consistency strength as lean + AC, it will not be able to prove any new turing machines halt

view this post on Zulip Johan Commelin (Sep 25 2018 at 08:59):

So, there are only finitely many abelian varieties of dimension g over rat with good reduction outside {favourite finite list of primes}.

view this post on Zulip Johan Commelin (Sep 25 2018 at 08:59):

I don't think we know any upper bounds on this. The proof is a celebrated theorem of Faltings and uses classical maths all over the place.

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:00):

If your favourite finite list of primes is not empty, then this function is extremely hard to compute.

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:00):

(Otherwise it is if g = 0 then 1 else 0.)

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:01):

Does this mean that f g = card (abelian varieties of dim g with good reduction outside blah) is not computable?

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:02):

Hmmm.... I'm too much of a newbie when it comes to such questions.

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:05):

hm, this theorem has AEA quantifier complexity, which is a bit hard to use

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:06):

AEA?

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:06):

\forall \exists \forall?

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:06):

"for all g, there exists an n such that all variety things don't have good reduction above n"

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:07):

No, I don't think that's what it says.

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:07):

I assume there is a way to enumerate abelian varieties?

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:08):

and the theorem says this enumeration runs dry after a certain point

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:08):

For all P : finset primes and for all g there exists n such that card { abvar of dim g and good reduction outside P } is less than n.

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:09):

Well, an abelian variety is defined by a finite number of polynomials

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:09):

right, so we enumerate all such things

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:09):

and only a finite number of them will have good reduction

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:09):

Right (the polys are over Q), so we could do that.

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:09):

so there is an upper bound on the last one with good reduction

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:09):

thus AEA

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:09):

Right, but testing the good reduction has to happen at all primes outside P

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:10):

So you can't enumerate that.

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:10):

oh, I see

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:10):

But I guess you can compute some discriminant in terms of the polynomials

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:10):

the property of having good reduction depends on all p?

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:10):

and then bad reduction at p implies that p divides the discriminant.

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:11):

This works for elliptic curves (the case g = 1)

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:11):

then it is AEAE

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:11):

Lol

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:11):

for all g/P, there exists n, such that for all abvars above n, there is a p such that the var has bad reduction at p

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:12):

No, it isn't about abvars above n, I think.

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:12):

At least I can't parse that.

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:12):

Ooh, wait, you enumerated them

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:12):

that is to exclude the finite number of things with good reduction

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:13):

Hmmm.... but we still need a decision procedure to determine if a bunch of polynomials defines an AV

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:13):

that's surely decidable

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:13):

Ok, if you say so... I have no idea how to do that...

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:13):

I have no idea what an AV is, so there

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:14):

but it surely can't be more than AE complexity

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:14):

It means that there exists a group structure on the solution set defined by the polynomials, and the solution set must be compact (in the algebro-geometric sense of compact)

view this post on Zulip Johan Commelin (Sep 25 2018 at 09:15):

Both seem hard to check at first sight.

view this post on Zulip Edward Ayers (Sep 25 2018 at 09:16):

For a fixed n you can do that, but I don't think you can do that for all n

Is this argument on the right lines?
If p and q are computable and we know that for all n, if p(n) then there exists a m such that q(m,n). Then there exists a computable function n -> m using AC. So I can find the code which runs that function, and put that in Lean. So n doesn't have to be fixed.

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:17):

but the code that runs that function uses AC

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:17):

oh you mean the code of a computable function

view this post on Zulip Edward Ayers (Sep 25 2018 at 09:17):

Right but I can find the code outside Lean and just put the code in

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:17):

but then you need to know it codes a (total) computable function

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:17):

and the proof of that uses AC

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:18):

lean won't just let you run whatever function you like

view this post on Zulip Edward Ayers (Sep 25 2018 at 09:19):

I can run the n->m in unsafe mode because it's not part of the proof. I just need to get the m

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:20):

the idea with this reduction is to build a computable function in no axioms lean, right? You can't run in unsafe mode since then you don't have a well defined term

view this post on Zulip Mario Carneiro (Sep 25 2018 at 09:21):

i.e. the m that you pick depends on n, so there is no closed term you can give for the function without unsafe lean stepping in to provide the m

view this post on Zulip Jared Corduan (Sep 25 2018 at 18:44):

how about this:
let A(n) be some computable predicate that requires either AC or LEM to show that either {n | A(n)} or {n | ~A(n)}is infinite. (in other words, A witnesses the nonconstructive nature of the infinite pigeon hole principle).

then let q1(m, n) be the statement that there is an n < x < m such that A(x) holds. and similarly define q2(m, n) with ~A(x). both of these are computable since A is computable. since either {n | A(n)} or {n | ~A(n)}is infinite, then for at least one of q1 or q2we can show the existence of such an m for any given n. but we need AC or LEM for the existence of the ms.

view this post on Zulip Kenny Lau (Sep 25 2018 at 18:45):

is there a tl;dr for this thread?

view this post on Zulip Patrick Massot (Sep 25 2018 at 18:46):

Do you really want me to write it?

view this post on Zulip Kenny Lau (Sep 25 2018 at 18:46):

well this thread is way too long, a tl;dr would be good, I don't see why not

view this post on Zulip Patrick Massot (Sep 25 2018 at 18:47):

Ok, let me try: constructivity questions are pointless.

view this post on Zulip Kenny Lau (Sep 25 2018 at 18:49):

I don't think that's a very faithful summary, nor is it contributing to the discussion at hand

view this post on Zulip Patrick Massot (Sep 25 2018 at 18:50):

I'm sorry, but you explicitly asked for it!

view this post on Zulip Patrick Massot (Sep 25 2018 at 18:50):

Anyway, I should work instead of trolling

view this post on Zulip Mario Carneiro (Sep 25 2018 at 18:51):

I don't think that works, although it's so close I can taste it. What is the computable function that we are defining?

view this post on Zulip Mario Carneiro (Sep 25 2018 at 18:52):

(Kenny, the gist is I posed a puzzle here and people are trying to solve it.)

view this post on Zulip Jared Corduan (Sep 25 2018 at 18:53):

well, it's one of two functions. either 1) it is f(n) is the least m>nsuch that A(n) or 2) it is f(n) is the least m>nsuch that ~A(n).

view this post on Zulip Jared Corduan (Sep 25 2018 at 18:53):

but I punted on giving you an actual A...

view this post on Zulip Mario Carneiro (Sep 25 2018 at 18:53):

But we can't define either of those functions unless we have a proof (possibly using AC) that A(n) is infinite (resp. co-infinite)

view this post on Zulip Jared Corduan (Sep 25 2018 at 18:54):

you can prove the infinite pigeon hole with AC and LEM, so all I'm missing is a good A, right?

view this post on Zulip Mario Carneiro (Sep 25 2018 at 18:56):

right, but if we assume A is something about which we can prove very little, then we can't prove A(n) is infinite, so 1) can't be defined, and we can't prove ~A(n) is infinite either, so 2) can't be defined

view this post on Zulip Chris Hughes (Sep 25 2018 at 18:56):

What's the constructive proof that there exists a natural such that a^n=1 in a finite group?

view this post on Zulip Mario Carneiro (Sep 25 2018 at 18:57):

If it is finite, then there is an upper bound on the cardinality, enumerate them all and test for equality

view this post on Zulip Mario Carneiro (Sep 25 2018 at 18:57):

(you need decidable equality)

view this post on Zulip Jared Corduan (Sep 25 2018 at 18:58):

ok, I might have misunderstood the problem! I thought we wanted an f that needed AC and/or LEM in order to be defined, though it was built from these computable predicates.

view this post on Zulip Mario Carneiro (Sep 25 2018 at 18:59):

That is what we want, but it also needs to be a term that represents a lean-computable function

view this post on Zulip Mario Carneiro (Sep 25 2018 at 18:59):

It is okay if the proof of existence of the term is nonconstructive, like you tried, but the term itself must contain a proof that it halts since lean expects as much

view this post on Zulip Jared Corduan (Sep 25 2018 at 19:00):

ah ok, I'll have to think about that some more!

view this post on Zulip Reid Barton (Sep 25 2018 at 19:14):

Could we do something like this? Inside Lean, build a language for programs in STLC or another system which Lean can prove is strongly normalizing, but incorporating the type N^\hat \mathbb{N} = nondecreasing functions nat -> bool. Then the input to our function is a code for a function f from N^\hat \mathbb{N} to bool together with a proof that f inf = tt (where inf N^\in \hat \mathbb{N} is the constant function ff); we can enumerate such programs because the system is strongly terminating. In Lean+LEM, we can prove that every such function satisfies f n = tt for some finite n, and we ask that our function return the smallest such n.

view this post on Zulip Reid Barton (Sep 25 2018 at 19:16):

Actually we don't even need the type N^\hat \mathbb{N}, we can just use the whole type nat -> bool, but with the same idea.

view this post on Zulip Reid Barton (Sep 25 2018 at 19:17):

If f (const ff) = tt, then there must be some finite n such that f (\lam x, x > n) = tt.

view this post on Zulip Reid Barton (Sep 25 2018 at 19:17):

Then we seek g f = the least n for which the above holds, provided that f (const ff) = tt, otherwise 37

view this post on Zulip Reid Barton (Sep 25 2018 at 19:19):

(Compare http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/)

view this post on Zulip Reid Barton (Sep 25 2018 at 19:19):

Maybe this is actually still computable without LEM though

view this post on Zulip Reid Barton (Sep 25 2018 at 19:30):

Yeah, I doubt this can be made to work. If you can constructively define a normalizer for your language, then you can presumably modify it to keep track of the invocations of the argument, and return the largest number on which it is invoked, then search up to there. If you can't constructively define a normalizer for your language, then you should just use a normalizer for your language as the function we're looking for.

view this post on Zulip Mario Carneiro (Sep 25 2018 at 19:37):

Note that one way to "cheat" here is to have as input a nondecidable proposition, which you then use in the construction. I did something similar with my example of a function that takes as input a function that is not constant zero and returns a value in the range

view this post on Zulip Mario Carneiro (Sep 25 2018 at 19:46):

Here again we seem to be stuck: if we use STLC or something provably normalizing, then we won't need LEM to prove the compactness property, and if we use DTT functions then even AC won't help since compactness isn't provable (though true)

view this post on Zulip Reid Barton (Sep 25 2018 at 19:47):

Yes. We would need a language whose power is just right so that the proof of normalization requires LEM, which I have no idea how to go about (or whether it is even plausible that such a language could exist).

view this post on Zulip Reid Barton (Sep 25 2018 at 19:50):

Can we prove that Lean-with-N-universes is normalizing inside Lean-with-N+1-universes? What do we know about the relative consistency of AC?

view this post on Zulip Reid Barton (Sep 25 2018 at 19:51):

Any term of type nat -> nat is equal (in a meta sense) to one defined without using universe variables right?

view this post on Zulip Mario Carneiro (Sep 25 2018 at 19:51):

I believe that Con(CIC+AC) = Con(CIC) for the same reasons as Con(ZF) = Con(ZFC)

view this post on Zulip Reid Barton (Sep 25 2018 at 19:52):

I wonder whether we can just describe a meta-level procedure for taking a function defined in Lean+AC and producing an equal one defined in Lean (using one more universe) explicitly

view this post on Zulip Mario Carneiro (Sep 25 2018 at 19:52):

I believe that lean-with-n-universes is normalizing in n+1 universes

view this post on Zulip Mario Carneiro (Sep 25 2018 at 19:52):

I have to prove that lean is normalizing first though :)

view this post on Zulip Mario Carneiro (Sep 25 2018 at 19:53):

any term of type nat -> nat may contain universe variables but is parametric in them, so you get the same result no matter what they are set to

view this post on Zulip Kenny Lau (Sep 25 2018 at 19:53):

Any term of type nat -> nat is equal (in a meta sense) to one defined without using universe variables right?

I heard FLT uses universes

view this post on Zulip Kenny Lau (Sep 25 2018 at 19:54):

Fermat's Last Theorem

view this post on Zulip Reid Barton (Sep 25 2018 at 19:54):

by writing an evaluator for Lean+AC-in-N-universes in Lean-in-N+1-universes, and then at the meta level looking to see how many universes are actually used, picking N to be bigger than that and writing down a term in the model that corresponds to the given function

view this post on Zulip Mario Carneiro (Sep 25 2018 at 19:54):

It may be that even without any universe variables you still need type 3 or something in the term

view this post on Zulip Mario Carneiro (Sep 25 2018 at 19:54):

(re: kenny)

view this post on Zulip Kenny Lau (Sep 25 2018 at 19:55):

but is it just because nobody has cleaned up the proof yet?

view this post on Zulip Kenny Lau (Sep 25 2018 at 19:55):

do we really need type 3?

view this post on Zulip Reid Barton (Sep 25 2018 at 19:55):

Kenny is taking over for Patrick on trolling duty

view this post on Zulip Kenny Lau (Sep 25 2018 at 19:56):

i'm serious

view this post on Zulip Mario Carneiro (Sep 25 2018 at 19:56):

We know that ZFC is equiconsistent with ZF, but I think that may include a double negation translation

view this post on Zulip Mario Carneiro (Sep 25 2018 at 19:56):

(if you use IZF in place of ZF)

view this post on Zulip Reid Barton (Sep 25 2018 at 19:57):

I believe that Con(CIC+AC) = Con(CIC) for the same reasons as Con(ZF) = Con(ZFC)

This is unclear to me because, in the case of ZF, we start from classical logic, at least in the version I know. But that's not to say that LEM is required for the relative consistency, only that I don't know whether it is.

view this post on Zulip Mario Carneiro (Sep 25 2018 at 19:58):

I also know that classical prop calc is equiconsistent with intuitionistic

view this post on Zulip Reid Barton (Sep 25 2018 at 20:00):

@Kenny Lau https://mathoverflow.net/questions/35746/inaccessible-cardinals-and-andrew-wiless-proof (See the first few answers.)

view this post on Zulip Reid Barton (Sep 25 2018 at 20:07):

Mario, right, that seems plausible then.

view this post on Zulip Kevin Buzzard (Sep 26 2018 at 07:42):

What's the constructive proof that there exists a natural such that a^n=1 in a finite group?

Let n be the order of the group ;-)

view this post on Zulip Kevin Buzzard (Sep 26 2018 at 07:44):

Any term of type nat -> nat is equal (in a meta sense) to one defined without using universe variables right?

I heard FLT uses universes

Kenny that is fake news, but the rumour seems hard to kill. Some people might argue that "the proof is written using universes" (because at some point Wiles says the word "representable functor" and at some other point uses etale cohomology) but they can easily be expunged using standard tricks.


Last updated: May 16 2021 at 05:21 UTC