[constantcrying]

I don't think this is convicing at all. None of this shows that there are generally accepted theorems without proofs.

The first one isn't lost at all, the second is just a single lost citation.

All of this is very far away from mathematicians building upon thr shaky grounds of mythical theorems. Also, in all my mathematical experience (going up to recent research in analysis) I never encountered something like this. In all textbooks I ever read either everything was proven or was cited to other works, which every time I checked included the proof.

[cubefox]

"Everything was proven" ... everything to satisfy a mathematician, not a logician. Formal proofs are generally very unwieldy, because informal proofs treat all the most obvious parts as obvious. In some cases these parts are not even trivial to prove formally. Last time I checked there was still no formal version of Cantor's diagonalization argument.

[scapp]

> Last time I checked there was still no formal version of Cantor's diagonalization argument.

Formalization? Like a computer checked proof?

Lean: https://leanprover-community.github.io/mathlib_docs/logic/fu...

Coq: https://github.com/bmsherman/finite/blob/63706fa4898aa05296c...

Isabelle: https://isabelle.in.tum.de/website-Isabelle2009-2/dist/libra...

[cubefox]

> Formalization? Like a computer checked proof?

Yes, that would be an example, though not all formalizations are written in software. I was originally talking just about standard formal logic, which is just first-order predicate calculus. Proof assistants use much more powerful systems in order to gain the same expressibility as the natural language which is used in informal proofs. (Which is kind of strange: In using natural language mathematicians don't seem to be using some advanced type theory.)

So I can't actually read these proof assistant languages, as they are using some advanced type theory based language. So just a few comments.

Lean: It looks suspicious that this seems to involve just one to two lines. Are they actually proving anything here? It doesn't look at all like Cantor's diagonal argument.

Coq: This looks better, at least from the description, and that it actually looks like a proof (Coq actually has a Qed keyword!). Though they, unlike Cantor, don't talk about real numbers here, just about sequences of natural numbers. Last time I read a discussion about it, it was mentioned that this exactly was a problem for the formal proof: Every natural number sequence (with a decimal point) corresponds to some real number, but real numbers don't necessarily have just one decimal expression, e.h. 0.999...=1. So real numbers and sequences can't straightforwardly be identified.

Isabelle: That seems to be a formalization of Cantor's powerset argument, not his diagonal argument.

Overall, this highlights a major problem with formalization of existing proofs. There is no way (at least no obvious way) to "prove", that a formal proof X actually is a formalization of some informal proof Y. X could be simply a different proof, or one which is similar but uses stronger or question begging assumptions, etc. One such example is informal proofs (like Cantor's) which didn't work in any axiomatized system, and where it isn't clear how much you can assume for a formal version without being question begging.

[constantcrying]

You have literally been given a fully formal proof of Cantor diagonalization.

The lean proof seens correct, I can't read lean well, but it appears to just be a formalization of the standard proof. It at least constructs the set needed for the proof.

>Proof assistants use much more powerful systems in order to gain the same expressibility as the natural language which is used in informal proofs. (Which is kind of strange: In using natural language mathematicians don't seem to be using some advanced type theory.)

Look up "Curry-Howard isomorphism".

>Overall, this highlights a major problem with formalization of existing proofs. There is no way (at least no obvious way) to "prove", that a formal proof X actually is a formalization of some informal proof Y.

And? This seems not relevant to the question at hand. Surely some textbook contains an insufficient proof, which couldn't be formalized without more steps. Why does that matter. The question still is whether "folk theorems" are real. Certainly Cantor's theorem is no such folk theorem, as you have just been given a fully formal proof.

>Though they, unlike Cantor, don't talk about real numbers here

Cantors theorem usually refers to the existence of uncountable sets, which can be proven by showing that there is no bijection between N and R, but also by showing that there is no bijection between a set and its powerset.

>Every natural number sequence (with a decimal point) corresponds to some real number, but real numbers don't necessarily have just one decimal expression, e.h. 0.999...=1. So real numbers and sequences can't straightforwardly be identified.

This is only relevant if you say that the real numbers are "infinte strings of digits", which is not a formal definition and therefore not used in mathematics.

[cubefox]

> The question still is whether "folk theorems" are real. Certainly Cantor's theorem is no such folk theorem, as you have just been given a fully formal proof.

I didn't say that Cantor's theorem is a folk theorem, only that some proofs aren't even trivial to formalize. Many other things are trivial to formalize, but they still require filling in a lot of obvious steps. It often wouldn't be practically feasible to prove them with a standard first-order calculus, otherwise proof system languages wouldn't need higher order systems with advanced type theory.

> Cantors theorem usually refers to the existence of uncountable sets, which can be proven by showing that there is no bijection between N and R, but also by showing that there is no bijection between a set and its powerset.

Yes, but I was talking about his diagonal argument, not his powerset argument. That's a different proof from a different paper.

> This is only relevant if you say that the real numbers are "infinte strings of digits", which is not a formal definition and therefore not used in mathematics.

Well, I'm not saying that, but the Coq proof seems to assume it. That was the problem I was talking about.

[constantcrying]

I don't get what the distinction is.

>because informal proofs treat all the most obvious parts as obvious.

No, they treat the most obvious parts as previously proven (which they are). That is an enormous difference.

I really have no idea what the difference to a "fully formal" and the standard proof would be, except the later argument includes verbose commentary, instead of logical symbols. But saying "since a is true and we formerly proved a implies b, we know b is true" instead of "(a and (a => b)) => b", does only seem to be a pedantic difference.

>Last time I checked there was still no formal version of Cantor's diagonalization argument.

AFAIK it is part of the standard libraries of multiple proof assistants, which means it is as fully formal as it can ever be.

[cubefox]

> >because informal proofs treat all the most obvious parts as obvious.

> No, they treat the most obvious parts as previously proven (which they are).

Well, I don't agree here. If you look at the history of mathematics, it shows that it progressed often in the opposite direction, where many "basics" were proven very late, e.g. by Dedekind, Peano, and Russell/Whitehead. Not to mention all these details which are now are getting expressed in languages for proof assistants. Many of these details couldn't even have been proved earlier, because the necessary formal systems were only invented recently.

> I really have no idea what the difference to a "fully formal" and the standard proof would be

Just look at actual formal proofs. They are very different from informal ones. To approximate the natural language of informal proofs, proof assistant languages actually have to use logics with advanced type systems, which most people who just write informal proofs wouldn't even understand.

> But saying "since a is true and we formerly proved a implies b, we know b is true" instead of "(a and (a => b)) => b", does only seem to be a pedantic difference.

It's more like they write "A, therefore B" (or even "A, then one easily sees that B") where the step from A to B is considered obvious by the guy who wrote the proof (a reviewer might reject it and ask for more intermediate steps, if he feels the "A therefore B" step isn't obvious), and where usually no commentary like "and we formerly proved A |= B" is included. Proofs are in fact not plastered with such commentaries, and if they were, people would expect a reference to where this was proven previously. But they don't expect references to obvious steps, because they are obvious, not because they necessarily expect they were proven previously somewhere. That wouldn't even make sense, since many theories were not, or are still not, axiomatized, so respective proofs have to rely on things that are considered obvious.

I already cited Yehuda Rav's 1999 paper "Why Do We Prove Theorems?"[1][2] elsewhere in this thread, and it's again relevant here.

From p. 13:

> A proof in mainstream mathematics is set forth as a sequence of claims, where the passage from one claim to another is based on drawing consequences on the basis of meanings or through accepted symbol manipulation, not by citing rules of predicate logic.4 The argument-style of a paper in mathematics usually takes the following form: '... from so and so it follows that..., hence...; as is well known, one sees that...; consequently, on the basis of Fehlermeister's Principal Theorem, taking in consideration α, β, γ, ..., ω, one concludes..., as claimed'. Why is it so difficult, in general, to understand a proof? Why does one need so much background information, training and know-how in order to follow the steps of a proof, when the purely logical skeleton is supposed to be nothing more than first-order predicate calculus with its few and simple rules of inference?

From p. 14f:

> In reading a paper or monograph it often happens—as everyone knows too well—that one arrives at an impasse, not seeing why a certain claim B is to follow from claim A, as its author affirms. Let us symbolise the author's claim by 'A —> B' . (The arrow functions iconically: there is an informal logical path from A to B. It does not denote formal implication.) Thus, in trying to understand the author's claim, one picks up paper and pencil and tries to fill in the gaps. After some reflection on the background theory, the meaning of the terms and using one's general knowledge of the topic, including eventually some symbol manipulation, one sees a path from A to A_1, from A_1 to A_2, ..., and finally from A_n to B. This analysis can be written schematically as follows:

> A —> A_1, A_1 —> A_2, ..., A_n —> B.

> Explaining the structure of the argument to a student or non-specialist, the other may still fail to see why, for instance, A_1 ought to follow from A. So again we interpolate A —> A', A' —> A_1. But the process of interpolations for a given claim has no theoretical upper bound. In other words, how far has one to analyse a claim of the form 'from property A, B follows' before assenting to it depends on the agent.

[1] https://doi.org/10.1093/philmat/7.1.5 [2] http://sgpwe.izt.uam.mx/files/users/uami/ahg/1999_Rav.pdf

[ithinkso]

> (The arrow functions iconically: there is an informal logical path from A to B. It does not denote formal implication.)

> In other words, how far has one to analyse a claim of the form 'from property A, B follows' before assenting to it depends on the agent.

Or just prove the implication instead of inventing 'informal logical paths'

[cubefox]

The "informal logical path" proves the informal implication, but what counts as a proof of this implication here can be agent dependent. If we talk about proving formal implication, then we have still the problem of deduction[1][2][3]. In short, natural language doesn't distinguish between "inference rules" and expressing this rule in a sentence and using it as a premiss. Which leads to an infinite regress, unless the agent just stops at some point, unlike the tortoise in Carroll's story.

[1] https://doi.org/10.1093/mind/IV.14.278 [2] https://en.wikipedia.org/wiki/What_the_Tortoise_Said_to_Achi... [3] https://www.jstor.org/stable/2253263

[constantcrying]

I agree that proofs assume for readability that the reader fills in some blanks. I might even go so far as to say that this informality can be dangerous.

Still, the question is, are there "folk theorems", where no proof exist which could be written down fully formal?

[cubefox]

I said there are accepted statements for which nobody can "cite" a proof, not that these statements are not provable in principle.

[zozbot234]

I don't think this is correct. Cantor's diagonal argument follows easily from Lawvere's fixed-point theorem https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theore... and both are quite easy to formalize.

[cubefox]

That seems to be a different proof which implies Cantor's theorem, but not a formalization of Cantor's diagonal argument itself.

[zozbot234]

It is a formalization of Cantor's diagonal argument - in fact, of "diagonal arguments" more generally. See http://arxiv.org/abs/math/0305282 for an expository treatment.

[cubefox]

Thanks, looks interesting.