Zulip Chat Archive

Stream: maths

Topic: truth and provability


view this post on Zulip Kevin Buzzard (Feb 17 2021 at 11:09):

I don't understand whether if P : Prop and hP : P then hP is supposed to say "P is true" or "P is proved". I don't know too much about logic, but I know enough to know that truth and provability are different. Can someone clarify what's going on? I have to figure out how to teach this stuff.

view this post on Zulip Mario Carneiro (Feb 17 2021 at 11:26):

In a formal theorem prover you can feel free to think of it in either way. In your mental model (or even formal model) of what the statements mean, it is "P is true", but in actual usage what it means is "P is proved" since at the end of the day you are constructing a finite object (a proof), not actually working with the platonic ideal things in your head

view this post on Zulip Mario Carneiro (Feb 17 2021 at 11:28):

The thing is, inside the prover you aren't allowed to "internalize" the idea that truth and lean-provability are different, which is why things like P \/ ~P are okay in the prover, which would not make any sense with the reading "P is proved or its negation is"

view this post on Zulip Mario Carneiro (Feb 17 2021 at 11:30):

I think there is a blog post by Tao about the different meta-levels of proof that touches on some of this

view this post on Zulip Mario Carneiro (Feb 17 2021 at 11:32):

Unfortunately I can't find it

view this post on Zulip Mario Carneiro (Feb 17 2021 at 11:46):

To summarize my recollection (mixed with an unknown quantity of editorializing): there are at least two distinct meta-levels you can consider when doing mathematics (normally, but especially in the computer).

In the first meta-level, you are thinking about rings and vector spaces and arguing about all things with property X having property Y and so on; this is the mentality of the working mathematician, and in this mode the computer is giving you a language to talk about abstract objects, and so you want to think about hP : P as "P is true".

In the next meta-level up, you step back and look at what you are doing and say "hey, I'm writing words on a page, bytes in a computer, and creating a finite object, namely a proof". In the first meta-level proof didn't really enter the picture, only facts, but really you were constructing proofs the whole time. But proofs are objects too, they can be coded as natural numbers and verified by machines and all that good stuff. When you are thinking about this metalevel, hP : P is really a piece of syntax, representing part of a lambda function that if you apply to a closed term might be a proof of some statement. So it's not really directly a proof, but certainly something like theorem sylow_1 : ... is a proof.

You can of course also do mathematics at the second meta-level, that's usually the domain of logic and proof theory, and most type theorists spend a significant amount of time thinking about this level, but at some point the mathematics gets complicated enough that it starts to look like the first level again and you might consider stepping back once more. Most logical foundations like metamath or LF work at the third meta-level, where they are verification systems that let you define axiom systems that let you do mathematics.

view this post on Zulip Mario Carneiro (Feb 17 2021 at 11:52):

It's fun to bring up Skolem's paradox in this context: We can prove there are uncountably many real numbers, but there are countable models of ZFC, that contain an object called the real numbers (necessarily also countable) for which the uncountability proof holds

view this post on Zulip Mario Carneiro (Feb 17 2021 at 11:59):

I guess something like Agda can also be seen as working at the third meta-level, since it looks at all those type theorists trying to classify mathematics and tries to classify the type theories and present a useful tool for working and experimenting with them

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 12:22):

Thanks for this, this has clarified my thinking!

view this post on Zulip Jeremy Avigad (Feb 17 2021 at 18:29):

In TPIL I describe one way to avoid all the confusing metaphysics. The most straightforward way to give CIC a set-theoretic semantics is to interpret types as sets, interpret "t : T" as elementhood, and interpret Prop as, say, the set { emptyset, {0} }.

With that interpretation, when we write down the Goldbach conjecture, we are just writing a fancy definition of the set { x in {0} | Goldbach is true ). Establishing "t : P" means showing that there is something in P, which means showing that it is not the empty set, which means showing that it is true. In that case, t is just a fancy notation for 0.

The fact that, as an expression, t has enough information for a deterministic type checker to determine that it is in P means we can think of t as evidence that P is true, or a proof that P is true. It's like showing a number is composite by giving the factors. If I write 111 = 37 * 3 and you have the means to check the calculation, then we have "proved" that 111 is composite. So we have shown that "111 is composite" is true, and given that the expression "37 * 3" gave you the information you needed to confirm that, you can think of that expression as a proof.

That doesn't preclude other ways of thinking about type theory, but I think it is important to make it clear to a general mathematical audience that there is nothing deeply mysterious about it. If you can make sense of something like "the set of x in {0} such that the Goldbach conjecture is true," you can make sense of propositions as types.

view this post on Zulip Eric Wieser (Feb 17 2021 at 18:32):

Something that caught me out as a beginner is that having h : 0 = 1 in your goal context does not mean 0 = 1 is true, it just means that in the local context you've assumed it is true.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 18:36):

What confuses me is that if I can prove P    QP\implies Q then I know that I can deduce that QQ is true from the assertion that PP is true, and i can deduce that QQ is provable from the assertion that PP is provable, so I am sometimes confused about whether hP : P means that PP is true or PP is provable. This is because I know enough about Goedel to know that these things are distinct, and yet my general day-to-day fuzzy thinking is not clear enough to actually know what I am doing. For example, I might grandiosely say in a paper "let X be a Noetherian scheme". Am I assuming that Noetherian-ness of X is something which is true, or something which is provable? I realise that I am somehow confused on this point.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 18:37):

I suspect that for all my day-to-day interactions with the mathematical world, I could be doing either, although it might be a good idea to stay consistent about my choices within one reasoning session.

view this post on Zulip Mario Carneiro (Feb 17 2021 at 18:38):

One thing to keep in mind is that P -> Q does not mean the same thing as P is provable -> Q is provable, because the latter might be vacuously true where the second is not. For example nat = int -> false is not provable in lean, however it is true in lean that if nat = int is provable then false is provable, because nat = int is not provable

view this post on Zulip Mario Carneiro (Feb 17 2021 at 18:40):

the implication only goes one way: if (P -> Q) is provable then if P is provable then Q is provable, this is modus ponens

view this post on Zulip Johan Commelin (Feb 17 2021 at 18:41):

Mario Carneiro said:

For example nat = int -> false is not provable in lean, however it is true in lean that if nat = int is provable then false is provable, because nat = int is not provable

Unless false is provable, in which case nat = int is provable. :rofl:

view this post on Zulip Mario Carneiro (Feb 17 2021 at 18:42):

but in that case the right half of the implication is true

view this post on Zulip Mario Carneiro (Feb 17 2021 at 18:43):

(that said, if lean proves false then the first assertion fails, since lean does prove nat = int -> false)

view this post on Zulip Johan Commelin (Feb 17 2021 at 18:43):

I should have only quoted the final subphrase "because nat = int is not provable"

view this post on Zulip Jeremy Avigad (Feb 17 2021 at 18:55):

Again, this all sounds too confusing. Consider the statement "if 111 is composite then so is 333." One way I can convince you of that fact is by showing you that if we have any nontrivial divisor of 111, then we can multiply it by 3 to get a nontrivial divisor of 333. (O.k., that's a stupid way to do it, but bear with me.) That works whether or not 111 is really composite, but if you eventually find evidence that it is, you can leverage it to get evidence that 333 is composite.

As an expression, t : P -> Q shows you how to turn evidence for P into evidence for Q. In the set-theoretic interpretation, it is a function from P to Q. In any case, the net effect of having an expression t : P -> Q and recognizing it as such is that you know that if P is true then Q is true.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 18:56):

I don't know whether "having evidence for P" should be interpreted as "P is true" or "P is provable", and I am beginning to wonder whether the correct answer is "you can choose".

view this post on Zulip Jeremy Avigad (Feb 17 2021 at 19:05):

I think you are right, you can think of it either way. It depends whether you are trying to make a statement about the proof system or what the expressions mean when interpreted as mathematical statements.

To really beat the analogy, "37 * 3 = 111" can be interpreted as saying "111 is composite" or "I have a factorization of 111."

But if you want to think about formal proving like informal proving, forget about the proof system and focus on what it says. So it's probably better to read "t : P" as "P is true" or just "P" (remembering that in a context, the judgment may be hypothetical).

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:06):

Right, this is what I've been telling my students -- think of "hP : P" as the hypothesis that P is true, except that sometimes I wax lyrical about how f : P -> Q is a function from proofs of P to proofs of Q and then I realise I've painted myself into a corner :-)

view this post on Zulip Jeremy Avigad (Feb 17 2021 at 19:12):

Yeah, I'd avoid talking about functions from proofs to proofs.

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:14):

Oops, I've done that pretty often :see_no_evil:

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:15):

lol I'm sure I learnt that amazing way of thinking about implications from TPIL!

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:16):

The only problem is when you tell people that all proofs of Fermat's Last Theorem are equal, when everyone knows that some are historically older / use different heavy machinery etc.

view this post on Zulip Massimiliano Gubinelli (Feb 23 2021 at 08:46):

Can somebody give me pointer on why "proof irrelevance" is needed? Where in the functional interpretation one needs to identify all the terms in the type of a proposition? E.g. I would like to distinguish proofs which use the axiom of choice from proofs which doesn't. If I look at the code I can see that they refer to some different global constants, why the language has to ignore this informations?

view this post on Zulip Johan Commelin (Feb 23 2021 at 08:47):

You don't need it, per se. It's just very convenient.

view this post on Zulip Johan Commelin (Feb 23 2021 at 08:49):

For example, there is the type pnat of positive natural numbers. It is really useful to know that x : pnat and y : pnat are the same if they have the same underlying natural number. Their equality shouldn't depend on how you proved that x and y are positive.

view this post on Zulip Eric Wieser (Feb 23 2021 at 08:54):

You can still distinguish whether a proof uses the axiom of choice from meta code

view this post on Zulip Eric Wieser (Feb 23 2021 at 08:55):

You just can't define something like "a function that is 1 if its proof argument uses the axiom of choice else zero"

view this post on Zulip Kyle Miller (Feb 24 2021 at 04:05):

Along the lines of @Johan Commelin's example, it's very nice that the map subtype.val : {x : A // p x} -> A is injective. (I don't know if proof irrelevance is necessary for it to work out this way though -- maybe you could have used trunc?)


Last updated: May 14 2021 at 19:21 UTC