|
> >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 |
> 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'