3

I have posted this in Philosophy SE as well because I feel that it is appropriate both here and there.

As practiced, mathematical proof seems not to be an explicit formal deduction within a formal system. Instead, proof seems to be a sort of critical thinking about things which appear to be necessarily true. The assumptions used in this thinking can be reasonably identified, but they are not explicitly stated at the outset.

Given this, what is the nature of mathematical conclusions in practice? Are they "informal deductions?" Is there any epistemological advantage to explicitly forming mathematical conclusions within a formal system, rather than what is commonly practiced (e.g. you probably haven't proved something like the fundamental theorem of calculus by tracing it back to axioms like ZFC, but maybe it should be done)? If so, why is this not standard procedure in the mathematical community?

I hope these questions are at least relatively clear - and thanks in advance for any insights!

JWP_HTX
  • 1,644
  • 2
    As to tracing back the Fundamental Theorem of Calculus to ZFC, this is can be one in principle by collecting the relevant theorems from the literature, and giving them a unified presentation. Because it is clear that it can be done, and would yield no additional insights, it is not worth bothering with. – André Nicolas Apr 15 '16 at 17:51
  • 1
    You might find interesting the discussion of realism vs. anti-realism in the Wikipedia article on philosophy of mathematics. I suspect the difference in viewpoints is of little interest to "working" mathematicians because the sufficiency and consistency of such axiomatic systems are "informally" accepted. – hardmath Apr 15 '16 at 17:52
  • ^Definitely - I've been the philosophy of math wiki page far more than I'd like to admit :) – JWP_HTX Apr 15 '16 at 17:58
  • @AndréNicolas even if it yields no additional "mathematical" insights, I am not so sure that makes it not worth bothering with. Perhaps there is greater epistemological certainty to be gained by being as explicit as possible from the outset about the assumptions upon which we are basing our reasoning? – JWP_HTX Apr 15 '16 at 18:13
  • Given a reasonable amount of time, and suitable financial incentives, I could do it. So could tens of thousands, perhaps hundreds of thousands, of others. And there would be the odd error that makes no difference. – André Nicolas Apr 15 '16 at 18:21
  • @AndréNicolas - I certainly agree that you and a lot of other people could formalize your proofs, but choose not to because you don't believe that you would gain any insight or clarity by doing so. I agree that you probably wouldn't gain any mathematical insights by doing so. However, formal proof leaves as little ambiguity as possible about one's assumptions and I think that maybe this greater epistemological certainty, while of course not perfect, is desirable enough to be worth pursuing. (Or at least having a computer do it) – JWP_HTX Apr 15 '16 at 18:48
  • Extension via definition: We introduce extensions of the language of set theory that do not imply any new axioms. E.g. we write $x=\phi$ rather than $\exists! y;(x=y\land \forall z;(z\not \in y.)$ After enough of this we can and do state and prove a calculus theorem in the language of set theory. It's just full of precisely defined abbreviations for formulae of set theory. – DanielWainfleet Apr 15 '16 at 19:53
  • @user254665 - sure, I agree with you (though I don't think I've ever seen a calculus theorem proved in the language of set theory). However, my question was essentially whether or not it is "more desirable" from an epistemological standpoint to do this sort of formal proof, or to prove theorems in the "normal" way that is common to the mathematical community. In particular, if it is more desirable, then why aren't there more mainstream efforts to do so? – JWP_HTX Apr 15 '16 at 20:18
  • it is generally undesirable.It can be tedious and not yield any further understanding, and may be very difficult to digest. – DanielWainfleet Apr 15 '16 at 21:40

1 Answers1

0

Basically, it boil down to convenience.

As practiced by mathematicians, a proof is "enough information that should be sufficent to write the formal proof if one would take the time and energy to do so".

When you write a proof, you should be able to explain everything if asked. But often, it's not asked, and the proof concentrate on the difficults points.

Now, if someone ask you to prove a step in your proof, and you're unable to prove it (or give a reference to a valid proof of this step), then your proof is invalid.

So, proofs practiced by mathematicians are not formal proofs, but they are things that could be converted to formal proof if needed

Tryss
  • 14,310
  • True, if we restrict attention to explanations given in lectures and papers, but note strong interest in proof automation and verification systems. – hardmath Apr 15 '16 at 17:56
  • Yeah, so I'm basically wondering if it may be "better" to actually formalize our proofs in math instead of just being comfortable with the fact that they could be formalized. Does it not make sense to strive from the outset for as little ambiguity as possible about the assumptions we use in our reasoning? – JWP_HTX Apr 15 '16 at 17:56
  • @Searching_for_a_foundation : the problem is that it become very heavy very fast. The idea is that you trade useless precision for efficiency. The keyword is useless. If you think there's an ambiguity, don't hesitate : formalise more ! – Tryss Apr 15 '16 at 18:12
  • @Tryss - yes, it does become very heavy very fast! But I think "how heavy" is an interesting question. Is it truly impossible for a human to do this? Maybe a computer could do it? In any case, I do see your point - it would be so vastly complicated to trace all of math up from axioms that for all intents and purposes, if there doesn't seem to be any real ambiguity in your work, then you should feel comfortable about it. – JWP_HTX Apr 15 '16 at 18:17
  • @Searching_for_a_foundation : yes, that's a task perfectly suited for a computer. There are some projects that aim to give formal proof of the usual theorems in analysis – Tryss Apr 15 '16 at 18:22