propext {P Q : Prop} : (P ↔ Q) → P = Q

Stream: Berkeley Lean Seminar

[Kentarô YAMAMOTO]

The exercise 0057 by Massot involves the axiom propext {P Q : Prop} : (P ↔ Q) → P = Q. Is this what Issac was talking about on Friday?

Back then, I jumped to the conclusion that this had something to do with proof relevance, but I doubt if it does now. I found https://leanprover.github.io/reference/expressions.html#computation as an article mentioning proof irrelevance. But it merely says that the meta-theoretic definition of definitional equivalence contains proof irrelevance, right?

So is the formal system behind Lean proof relevant or not?

[Patrick Lutz]

I don't think that's what Izaak was talking about. Instead he was talking about the fact that if P : Prop and t : P and s : P then t and s are definitionally equal

[Patrick Lutz]

See here: https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html

[Patrick Lutz]

But I think you could do things at the level of types instead of propositions and then you would recover proof relevance

[Patrick Lutz]

but I don't really know what I'm talking about

[Kentarô YAMAMOTO]

Do you know what, then, differentiates types of type Prop from other types in terms of proof relevance
?

[Patrick Lutz]

If P : Prop then any two inhabitants of P are definitionally equal in Lean. That's not true if P : Type

[Kevin Buzzard]

https://xenaproject.wordpress.com/2019/10/26/counting-binary-relations-an-apology/

[Kevin Buzzard]

I have been setting undergraduates questions of the form "how many binary relations are there on a set with two elements" for years, and I could never understand why some of them thought the answer was "infinitely many"

[Kevin Buzzard]

@Patrick Lutz -- right. Proof irrelevance is the idea that if P : Prop (i.e. if P is a true/false statement, like FLT or the Riemann Hypothesis or 2+2=4) and if s : P and t : P then s = t. What does it mean for two proofs to be equal? This is a really thorny question in proof theory. Is Furstenburg's topological proof of the infinitude of primes the same as Euler's? Some days I think it is, some days I think it isn't.

[Patrick Lutz]

I have been setting undergraduates questions of the form "how many binary relations are there on a set with two elements" for years, and I could never understand why some of them thought the answer was "infinitely many"

Extensional vs. intensional I guess

[Kevin Buzzard]

Lean avoids this by decreeing that all proofs of P are equal, and that's the end of that. But Propositional Extensionality is something else.

[Patrick Lutz]

Sorry, I was trying to respond to a different message

[Patrick Lutz]

I've edited my reply

[Patrick Lutz]

Kevin Buzzard said:

Patrick Lutz -- right. Proof irrelevance is the idea that if P : Prop (i.e. if P is a true/false statement, like FLT or the Riemann Hypothesis or 2+2=4) and if s : P and t : P then s = t. What does it mean for two proofs to be equal? This is a really thorny question in proof theory. Is Furstenburg's topological proof of the infinitude of primes the same as Euler's? Some days I think it is, some days I think it isn't.

Hilbert's 24th problem: https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_problem

[Kentarô YAMAMOTO]

Ah, that's by the (meta-)definition of definitional equality, right?

[Patrick Lutz]

Kentarô YAMAMOTO said:

Ah, that's by the (meta-)definition of definitional equality, right?

Yes

[Kentarô YAMAMOTO]

Here's a sloppy argument based on something I remember hearing "showing" that proof irrelevance hold true of any type P: Having choice as an axiom brings the ambient logic classical. Also, in a classical system, all proofs of a single proposition normalize to the same thing. What is wrong here? (Is the fact that Lean's choice applies only to types belonging to a certain universe relevant?)

[Patrick Lutz]

I think choice is not on by default in Lean

[Kyle Miller]

Patrick Lutz said:

Hilbert's 24th problem: https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_problem

(Speculation alert.) I've always been taken by the idea of constructing a topological space (CW complex?) whose points correspond to provable statements and paths between them to logical equivalence; a proof being a path to True. Then two proofs are "the same" if they are homotopic. One could wonder what it might mean having non-homotopic proofs. (I know pretty much nothing about homotopy type theory or infinity categories, both which might be related to this idea.) Regarding what Kentaro just said, perhaps having a choice axiom forces the topology to be contractible or at least simply connected?

Less speculatively, at least in knot theory a proof that two knots are the same is an isotopy that transforms one into another, and there are non-isotopic isotopies.

[Kentarô YAMAMOTO]

Have I been looking at an outdated document? https://leanprover.github.io/reference/expressions.html#axioms

[Patrick Lutz]

https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html

[Patrick Lutz]

I think you have to include some line like open locale classical at the beginning of a file where you want to use choice, etc

[Patrick Lutz]

and if you use choice you have to declare the theorem noncomputable

[Patrick Lutz]

so what I meant was that if you don't provide such annotations you can't use choice or lem or whatever and it is possible (I think? I'm not sure) to have proof relevance for constructing inhabitants of non-Prop types

[Kentarô YAMAMOTO]

Thank you for that document. (What document have I been looking at, then?)

[Patrick Lutz]

I don't think those two contradict each other

[Patrick Lutz]

But the reference manual seems to be somewhat incomplete right now

[Patrick Lutz]

the document "Theorem Proving in Lean" is written a bit more like a textbook but currently looks like a better source of information about how Lean works

[Kentarô YAMAMOTO]

OK!

[Patrick Lutz]

Kyle Miller said:

(Speculation alert.) I've always been taken by the idea of constructing a topological space (CW complex?) whose points correspond to provable statements and paths between them to logical equivalence; a proof being a path to True. Then two proofs are "the same" if they are homotopic. One could wonder what it might mean having non-homotopic proofs. (I know pretty much nothing about homotopy type theory or infinity categories, both which might be related to this idea.) Regarding what Kentaro just said, perhaps having a choice axiom forces the topology to be contractible or at least simply connected?

I've had vaguely similar thoughts but also know very little about those topics. I think I eventually decided that it wasn't clear they captured what I intuitively mean when I say "these two proofs are not the same"

[Kyle Miller]

Patrick Lutz said:

I've had vaguely similar thoughts but also know very little about those topics. I think I eventually decided that it wasn't clear they captured what I intuitively mean when I say "these two proofs are not the same"

It would be cool if you could take a forall statement (the space would be a fiber bundle with base space the universe for the quantification and the fibers being spaces of proofs for all the corresponding statements; a proof of the forall is a section of this fiber bundle) and consider some map to a "axiom of choice classifying space" which would be homotopically nontrivial iff the axiom of choice is required for any given proof. Not sure if this makes any real sense, but it seems at least mildly plausible.

[Kevin Buzzard]

@Kyle Miller this is exactly what Voevodsky was doing. This is called homotopy type theory. The proofs of X=Y are a space. Unimath does not have proof irrelevance. You can have two proofs of X=Y and these should be considered as paths from X to Y, and then a proof that these proofs are equal corresponds to a homotopy between these paths

[Kevin Buzzard]

Here is a simple example of two different proofs of something: there are two proofs of (P and Q) implies (P or Q), one going via a proof of P and the other going via a proof of Q. My understanding is that these proofs are not homotopic

[Kevin Buzzard]

This whole thing sounds like a really cool idea. But here's the catch

[Kevin Buzzard]

Voevodsky spent 15 years developing his theory with proof relevance and in some sense got nowhere.

[Kevin Buzzard]

Lean 2 also had this homotopy type theory univalence axiom

[Kevin Buzzard]

And then in lean 3 they dumped it and went for proof irrelevance, and in the three years after that the size of the maths library went through the roof

[Kevin Buzzard]

What I think is going on is that if you try and do normal mathematics in a proof relevant context then you get stuck because you can't "substitute in" as much as you want, because you need to start proving that proofs are equal

[Kevin Buzzard]

Many homotopy type theory people have told me I am wrong about this

[Kevin Buzzard]

And my response to them is: show me how to make a theory of schemes. Voevodsky got his fields medal for developing a homotopy theory of schemes and they never even got as far as the definition of a scheme in his system. Me and two first year undergraduates knocked off schemes in a few months in Lean as part of a learning project

[Kevin Buzzard]

In short, I think proof relevance is dangerous in practice

[Kevin Buzzard]

I think it inhibits mathematics

[Kyle Miller]

Kevin Buzzard said:

Here is a simple example of two different proofs of something: there are two proofs of (P and Q) implies (P or Q), one going via a proof of P and the other going via a proof of Q. My understanding is that these proofs are not homotopic

If modeling this as plain-old topological spaces is anything to go by then when P and Q are both true (are nonempty sets) the proofs are non-homotopic because P or Q (the disjoint union of P and Q) is disconnected. Maybe this suggests proof spaces for inductive types are too discrete for homotopy to be interesting in general. (Though, I could imagine the proofs might be homotopic in a suitable setting -- disjoint union might be too naive, however I propose no solutions to this.)

It seems like it's useful to go for proof irrelevance to make a significant math library, then perhaps revisit proof relevance once its strong enough, assuming there's an application. Maybe you need a well-developed and powerful system to automatically provide all the proofs of equality-up-to-higher-equivalences, and doing it "right" (from the point of view of the homotopy type theory people) is beyond our capabilities right now. (There's this classic essay in CS titled "The Rise of Worse is Better" contrasting different development styles for operating systems. Deciding to throw out proof relevance might be "worse," but it sounds like it's "better" because of how much more math you can quickly formalize.)

I'm more into trying to formalize some low-dimensional topology (one project might be to show there are at least three distinct knots), so these are all rather abstract concerns for me right now, but thanks for sharing your thoughts! You've given me some things to think about.

[Kentarô YAMAMOTO]

Is there an elementary example of a formalization of an ordinary theorem in mathematics (as opposed to something of predominantly logical interest) for which proving two proofs of the same proposition being equal is necessary? I am a little bit skeptical about that idea.

[Kevin Buzzard]

This whole thing is very well understood, but just not by me, so I am reluctant to say too much more. The main problem I've had learning the area is that a lot of the people who study homotopy type theory tend to be people interested in foundational matters and we seem to have little in common. The observation that very little of what I recognise as "normal mathematics" is in these provers is normally met by the counterargument that people that use them aren't really interested in that kind of mathematics. There are some fundamental big research questions about the nature of homotopy types and their relation to computation and infinity categories etc, and this is what people think about.

In some sense the main difference is this. In Lean"s dependent type theory the mental model is that a type is a set, and equality of terms of that type is equality of elements of that set. In homotopy type theory the mental model is that types are topological spaces up to homotopy, and equality of terms is interpreted as paths. My main objection to this is that if you have a topological space then it appears that it's an open problem to construct a type representing that topological space, whereas if you have a set then it's pretty easy to make a type in lean which corresponds to it. This whole thing about proofs being isomorphic is cool but is not something I want to be hung up on as an algebraic number theorist -- I don't want it to be in the way. Believe me I've seen enough problems in lean with proofs of x=x fail because if you expand out the terms it turns out that two multiplications you used somewhere deep down were not quite equal by definition and you have to apply an obvious lemma to finish the proof. For this issue to be made worse is not a place I want to go in practice. There is a whole HoTT Zulip chat which I'm sure would welcome any questions you have, but don't mention my name there ;-)

[Kentarô YAMAMOTO]

Gamma \turnstile P : Prop, s : P, t : P and Gamma \turnstile Delta implying Gamma \turnstile Delta[t/s] is an admissible rule in Lean, right? How does one derive that from first principles?

[Jalex Stark]

the thing you said looks to me like a fancy way of saying "Prop has proof irrelevance", so there's probably a way to prove what you said from the proof-irrelevance axiom, whatever that is

[Kentarô YAMAMOTO]

I looked at the definition of the equality type, but I couldn't figure out how proof irrelevance follows from it.

[Jalex Stark]

so your question is something like "where does the proof irrelevance axiom live"?

[Jalex Stark]

i see the phrase "Proof irrelevance is implemented in the kernel" in these notes
https://lean-forward.github.io/logical-verification/2018/41_notes.html