truth v provability

Stream: general

[Kevin Buzzard]

I'm writing natnumgame docs and I am being forced to wade into the truth v provability issue. "Proper mathematicians" are notoriously bad at this sort of thing -- they read a popular article about Goedel once and then think they're an expert. I am talking about P : Prop being a true/false statement and h : P being a proof of P. But every mathematician knows that $P\implies Q$ means "If $P$ is true then $Q$ is true", not "if $P$ is provable then $Q$ is provable". So my problem is that I need to justify the idea that f : P -> Q means "$f$ is a function from proofs of $P$ to proofs of $Q$" without exposing mathematician users to the possible confusion that they don't really understand truth and provability, but they are absolutely sure that they are not the same thing, and I am definitely talking about them as if they were. Can I argue that h : P means something like "$h$ is evidence for the truth of $P$" or something? I'm sure this is all very well understood, but being a "proper mathematician" it's not very well understood by me ;-)

[Chris Hughes]

TPIL says this

Some simplifications are possible, however. To start with, we can avoid writing the term Proof repeatedly by conflating Proof p with p itself. In other words, whenever we have p : Prop, we can interpret p as a type, namely, the type of its proofs. We can then read t : p as the assertion that t is a proof of p

[Kevin Buzzard]

But then $P\implies Q$ is not a function from proofs of $P$ to proofs of $Q$, at least not to a mathematician

[Kevin Buzzard]

I can isolate my confusion. LEM, which I am happy to assume as a mathematician, seems to say that for all P we can either find a proof of P or a proof of not P. So by "proof" this can't mean "proof from the axioms of maths", this must mean something more like "proof that this is true in this specific model I'm looking at"

[Chris Hughes]

Can't you just say it doesn't really matter. We just conflate provable and true, because they're the same thing in practice. I think of p or not p as a non constructive proof of the existence of a proof. Like, there is a proof, but I can't write one down. We don't mind that with reals.

[Kevin Buzzard]

I can say "it doesn't really matter" to undergraduates but I am concerned about saying that to people like Emily Riehl, who have played my natural number game and know full well that this isn't true.

[Kevin Buzzard]

I usually think of "proof" as meaning "proof from the axioms of maths" and Goedel gives you statements which are true but not provable. Worse, statements like the continuum hypothesis can be easily formalised in Lean and these are true in some models of maths and false in others. LEM provides me with a "proof" of either one or the other, so "proof" must not mean "proof from the axioms of maths", it must means something more like "proof that it's true in the model you're working in"

[Reid Barton]

An element s of a set S is _____ that S is nonempty.
A term h : P is _____ that P is true.

[Reid Barton]

You should fill in the same word here. What that word is and what you think the word means might depend on your background

[Chris Hughes]

witness?

[Kevin Buzzard]

An element of a set is a constructive proof from the axioms of maths that the set is non-empty. I'm not so sure that h : P is a constructive proof from the axioms of maths that the set is non-empty, because then I would be forced to reject Lean's LEM.

[Chris Hughes]

Why is an element of a set a constructive proof? By that logic, all sets are countable. So clearly not all elements of sets are constructive proofs.

[Reid Barton]

I thought the original issue was that both elements and sets belong to the object theory, while a proof is something in the metatheory, therefore an element cannot be a proof

[Kevin Buzzard]

The original issue is that Kevin doesn't understand Goedel properly.

[Chris Hughes]

I think the issue is that nobody invented a word for what h : P is, even though we all understand what it is.

[Kevin Buzzard]

I just want to argue that $P\implies Q$ can be thought of as a function from proofs of $P$ to proofs of $Q$, when "clearly" it doesn't mean that at all, it is a true-false statement defined by some stupid truth table diagram corresponding to the four possibilities TT,TF,FT,FF.

[Kevin Buzzard]

I want to be able to explain that concept to people like me in such a way that they don't go "wait a minute, we all know that truth isn't provability, how come these concepts are being conflated here?"

[Kevin Buzzard]

and such people will not know the difference between a theory and a metatheory, but they might well know that CH is not provable.

[Kevin Buzzard]

OK so I'm up and running. If I notice that compilation has produced some errors but is still running, can I just ctrl-C and type git bisect bad and then go back to git bisect run compile.sh?

[Chris Hughes]

It suffices to provide a function from proofs of p to proofs of q to prove p implies q.

[Reid Barton]

You can't avoid using the word "proof" forever, given that (h h' : P) -> h = h' is called "proof irrelevance" by everybody

[Chris Hughes]

Can't you just use the analogy, whilst saying it is only an analogy, and refer people to TPIL if they want some different explanation.

[Chris Hughes]

TPIL says that h : P is the fact that P is true

[Reid Barton]

You could say something along the lines that a Prop is really just a Type for which Lean has the built-in knowledge that it has at most one element. We think of P : Prop as encoding the proposition that this type is inhabited and by convention we call a term h : P a "proof" of this proposition.

[François G. Dorais]

@Kevin Buzzard Welcome to (classical) modal logic? https://plato.stanford.edu/entries/logic-provability/

[François G. Dorais]

As usual, logic is not essential to _do_ things, but it is useful and sometimes essential to _answer_ things
....

[Kevin Buzzard]

ha ha I knew someone like you would be pointing me to that encyclopedia at some point :D Many thanks Francois!

[François G. Dorais]

Happy to help!(?)

[Ulrik Buchholtz]

I think bringing in, and linking, the concepts of hypothetical proof and reasoning from hypotheses may help. Even classically, when doing a proof by contradiction, you eventually have to reason from hypotheses to derive a contradiction. So just as $f : A \to B$ maps hypothetical elements of $A$ to elements of $B$, $f : P \to Q$ maps hypothetical proofs of $P$ to proofs of $Q$, and we may well have more hypothetical proofs of $P$ than actual, canonical proofs. (And maybe throw in a link/reference to What the Tortoise Said to Achilles!)

[Ulrik Buchholtz]

But it is tricky, as is illustrated by the story of Brouwer's Fan Theorem: It's an implication $P \to Q$, where $P \equiv \forall \alpha, \exists n, \bar\alpha(n) \in V$ and $Q \equiv \exists N, \forall \alpha, \bar\alpha(N) \in V$. (Here $P$ is a decidable property of finite sequences of zeroes and ones, $\alpha$ ranges over infinite sequences, and $\bar\alpha(n)$ is the initial $n$-element subsequence of $\alpha$.) So the theorem expresses the compactness of Cantor space (classically true), but Brouwer's “proof” proceeded by assuming that a hypothetical $p : P$ could be brought into canonical form. Kleene later showed that the Fan Theorem fails in a computable model.

[Jason Rute]

I think there are two questions here.

- Question 1, what is really happening logically here.
- Question 2 is how to explain this to mathematicians without saying something false, but also not going down a logical rabbit hole.

I agree with others that TPIL does a fairly good job at the second problem, but you may feel otherwise. As for the first problem, the advantage and pain of logic is that it has many valid interpretations. Two broad categories are proof theory and model theory. In proof theory, we think about this logical framework as pure symbol manipulation. So if we have hp : P and hpq : P -> Q, then we can create hq : Q via hq := hpq hp. Now, one can just stick to the proof-theory viewpoint and say that all this is merely a symbolic contrivance which lets us treat hpq : P -> Q as "if it were a function" which takes a proof/witness of P and turns it into a proof/witness of Q. In other words, just think of it as a useful analogy that works.

One can also take a model theoretic viewpoint where we give a specific interpretation to all the symbols. There are a number of models which probably work here. (The picture is clear in my mind for classical first order logic, but I think an expert in categorical semantics might want to chime in to correct me here if I say anything slightly wrong.) Now, one has to fix a model to interpret the meaning of all the types A and the meaning of x : A. Then as for how to interpret h : P one still has multiple valid interpretations. Now if one is working in constructive logic only, then one can interpret a proposition P as the set of all proofs of P, in which case P is only inhabited if it is provable. Then P -> Q is simultaneously the proofs of P -> Q and all function from proofs of P to proofs of Q. Now, there is still a sticking point of what it means for two proofs to be the same. For example, if one just changes the variable names, is it the same proof? One viewpoint is that all proofs are the same (equal) so there is at most one proof of a proposition. This is proof irrelevance, and is consistent with the rest of constructive mathematics. However, once one moves to classical logic, I don't know how well the "P is the set of all proofs of P" interpretation works, specifically for the reasons you mentioned. (Actually, in Lean, since the logic is constructive but non-constructive axioms are added to the context, I think it makes sense to really say that the proposition CH \or \not CH is actually a different proposition that includes the full context. In that case, it would still make sense to say that the full proposition including the context, something like LEM -> (CH \or \not CH) can still be interpreted in this constructive propositions as types interpretation. It would also explain why both CH and \not CH could be empty but LEM -> (CH \or \not CH) is not, even though it would be appear locally as CH \or \not CH.)

In classical logic, one can take a more standard model theoretic approach. Fix a model of mathematics (something like a fixed model of the category of SET, but also taking into account universes, so a higher category of SET? I really don't understand categorical logic!). Then I think it would be consistent to interpret P as being inhabited with exactly one element if P is true in this model and uninhabited otherwise. (Yes, "truth" makes sense here since every proposition, including CH is either true or false in this model.) Then hp : P means that hp is that one element of P which witnesses that P is true. It is probably best to call it a "witness" to the truth of P. Since this interpretation is (hopefully) sound (it follows the rules of Lean's type theory), if there are witnesses hp : P and hpq: P -> Q, then Q is true in our model and hpq hp is a witness to that truth.

I hope this helps, and that I didn't say anything too false or just confuse you more.

[Kevin Buzzard]

one thing I absolutely want to stress here is that 99% of mathematicians have absolutely no idea what constructive logic is, and probably have never heard of the law of the excluded middle because it's obviously true. This means that I can't really say anything about constructive logic.

[Jason Rute]

99% of mathematicians have absolutely no idea what constructive logic is

More or less true (except that maybe about 5% or so of mathematicians are logicians, but that is still true of many logicians)

and probably have never heard of the law of the excluded middle

I find this doubtful. I bet 75% of mathematicians or more have heard of the the law of excluded middle.

[Jason Rute]

Also, to be clear, that long explanation was not for you to share to the users of the natural number game, but for your understanding. I find the better I understand something, the better I can know what I can brush under the rug without saying something completely false.

[Kevin Buzzard]

Yes, I thoroughly appreciate the explanations you and Ulrik have posted. Many thanks to both of you!