truth and provability

Stream: maths

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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"

[Mario Carneiro]

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

[Mario Carneiro]

Unfortunately I can't find it

[Mario Carneiro]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Thanks for this, this has clarified my thinking!

[Jeremy Avigad]

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.

[Eric Wieser]

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.

[Kevin Buzzard]

What confuses me is that if I can prove $P\implies Q$ then I know that I can deduce that $Q$ is true from the assertion that $P$ is true, and i can deduce that $Q$ is provable from the assertion that $P$ is provable, so I am sometimes confused about whether hP : P means that $P$ is true or $P$ 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.

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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:

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Jeremy Avigad]

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.

[Kevin Buzzard]

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".

[Jeremy Avigad]

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).

[Kevin Buzzard]

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 :-)

[Jeremy Avigad]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Massimiliano Gubinelli]

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?

[Johan Commelin]

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

[Johan Commelin]

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.

[Eric Wieser]

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

[Eric Wieser]

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

[Kyle Miller]

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?)