Zulip Chat Archive

Stream: general

Topic: truth v provability


view this post on Zulip Kevin Buzzard (Nov 09 2019 at 21:10):

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    QP\implies Q means "If PP is true then QQ is true", not "if PP is provable then QQ is provable". So my problem is that I need to justify the idea that f : P -> Q means "ff is a function from proofs of PP to proofs of QQ" 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 "hh is evidence for the truth of PP" or something? I'm sure this is all very well understood, but being a "proper mathematician" it's not very well understood by me ;-)

view this post on Zulip Chris Hughes (Nov 09 2019 at 21:33):

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

view this post on Zulip Kevin Buzzard (Nov 09 2019 at 21:34):

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

view this post on Zulip Kevin Buzzard (Nov 09 2019 at 21:35):

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"

view this post on Zulip Chris Hughes (Nov 09 2019 at 21:37):

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.

view this post on Zulip Kevin Buzzard (Nov 09 2019 at 21:39):

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.

view this post on Zulip Kevin Buzzard (Nov 09 2019 at 21:40):

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"

view this post on Zulip Reid Barton (Nov 09 2019 at 21:41):

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

view this post on Zulip Reid Barton (Nov 09 2019 at 21:41):

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

view this post on Zulip Chris Hughes (Nov 09 2019 at 21:42):

witness?

view this post on Zulip Kevin Buzzard (Nov 09 2019 at 21:45):

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.

view this post on Zulip Chris Hughes (Nov 09 2019 at 21:47):

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.

view this post on Zulip Reid Barton (Nov 09 2019 at 21:48):

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

view this post on Zulip Kevin Buzzard (Nov 09 2019 at 21:50):

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

view this post on Zulip Chris Hughes (Nov 09 2019 at 21:51):

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

view this post on Zulip Kevin Buzzard (Nov 09 2019 at 21:51):

I just want to argue that P    QP\implies Q can be thought of as a function from proofs of PP to proofs of QQ, 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.

view this post on Zulip Kevin Buzzard (Nov 09 2019 at 21:52):

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

view this post on Zulip Kevin Buzzard (Nov 09 2019 at 21:53):

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

view this post on Zulip Kevin Buzzard (Nov 09 2019 at 21:56):

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?

view this post on Zulip Chris Hughes (Nov 09 2019 at 21:58):

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

view this post on Zulip Reid Barton (Nov 09 2019 at 22:00):

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

view this post on Zulip Chris Hughes (Nov 09 2019 at 22:01):

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.

view this post on Zulip Chris Hughes (Nov 09 2019 at 22:05):

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

view this post on Zulip Reid Barton (Nov 09 2019 at 22:06):

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.

view this post on Zulip François G. Dorais (Nov 09 2019 at 22:48):

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

view this post on Zulip François G. Dorais (Nov 09 2019 at 22:52):

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

view this post on Zulip Kevin Buzzard (Nov 09 2019 at 23:02):

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

view this post on Zulip François G. Dorais (Nov 09 2019 at 23:18):

Happy to help!(?)

view this post on Zulip Ulrik Buchholtz (Nov 10 2019 at 08:57):

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:AB f : A \to B maps hypothetical elements of A A to elements of B B , f:PQ f : P \to Q maps hypothetical proofs of P P to proofs of Q Q , and we may well have more hypothetical proofs of P P than actual, canonical proofs. (And maybe throw in a link/reference to What the Tortoise Said to Achilles!)

view this post on Zulip Ulrik Buchholtz (Nov 10 2019 at 09:43):

But it is tricky, as is illustrated by the story of Brouwer's Fan Theorem: It's an implication PQ P \to Q , where Pα,n,αˉ(n)V P \equiv \forall \alpha, \exists n, \bar\alpha(n) \in V and QN,α,αˉ(N)V Q \equiv \exists N, \forall \alpha, \bar\alpha(N) \in V . (Here P P is a decidable property of finite sequences of zeroes and ones, α \alpha ranges over infinite sequences, and αˉ(n) \bar\alpha(n) is the initial n 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 p : P could be brought into canonical form. Kleene later showed that the Fan Theorem fails in a computable model.

view this post on Zulip Jason Rute (Nov 10 2019 at 15:49):

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.

view this post on Zulip Kevin Buzzard (Nov 10 2019 at 16:54):

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.

view this post on Zulip Jason Rute (Nov 10 2019 at 16:59):

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.

view this post on Zulip Jason Rute (Nov 10 2019 at 17:05):

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.

view this post on Zulip Kevin Buzzard (Nov 10 2019 at 17:21):

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


Last updated: May 08 2021 at 03:17 UTC