-2
$\begingroup$

In classical logic, any given theorem implies any other given theorem (the soundness of classical logic comes as one way to help realize this). I realize the term "mathematics" has a certain vagueness to it, but I would think that the idea of provable propositions in number theory, group theory, analysis, or any other field of mathematics doesn't have a similar vagueness to it (perhaps I'm naive in this belief). In number theory, group theory, or any other mathematical field, does any given theorem imply any other given theorem? If not, does it make sense to use classical logic when talking about any of these fields? Or does the notion of a theorem concerning the integers depend on the system of logic one takes for granted, and thus we don't really have a single field which talks about all the theorems concerning the integers, but rather number theories distinct in some way? Does there exist any sort of consensus with respect to these questions?

  • 0
    @anon By "completeness" I meant "semantical completeness". This means that if a proposition p is true, then p qualifies as a theorem. So, to deductively get from "(a->b) is true if "a" and "b" are true" to "(a->b) is a theorem if "a" and "b" are theorems" or equivalently "any theorem "implies" any other theorem" you need semantical completeness. But, you can get "any theorem "implies" any other theorem" without taking semantical completeness for granted, basically if you have conditional introduction as a valid rule of inference.2011-08-22

1 Answers 1

7

There are several possible answers, depending on the level of formality.

In formal number theory: Let $\varphi$ be a sentence of formal number theory, say the assertion that every odd natural number which is not of the form $8k+7$ is the sum of three squares. Suppose we have just given a proof of $\varphi$ in first-order PA. So we know that $\text{PA}\vdash \varphi$.

Then indeed we now know that $\text{PA}\vdash ((0=0)\longrightarrow\varphi)$. So what? If after the lengthy proof of $\varphi$, someone observed that now we knew that $\text{PA}\vdash ((0=0)\longrightarrow\varphi)$, we would presumably look at the person bemusedly. The person's (hypothetical) assertion is correct, of course, but kind of silly.

In informal number theory: A colleague might say something like "The fact that every odd positive integer not of the form $8k+7$ is the sum of three squares follows from Fermat's (little) Theorem." The word "implies" might be used instead of "follows from."

Even though it was proved by Gauss that every odd positive integer not of the form $8k+7$ is the sum of three squares, the above assertion would not be considered silly. Gauss's result is not easy to prove, or at least one needs a fair amount of prior machinery. By contrast, Fermat's (little) Theorem is low level, with several easy proofs.

In our colleague's assertion, "follows from" or "implies" could not possibly mean logical consequence. The intended meaning would be that the colleague had a proof whose most "advanced" ingredient was Fermat's (little) Theorem, perhaps used in a very clever way.

It would be difficult to give a plausible formalization of the "follows from" as it was used in the hypothetical conversation above. Sure, there are related notions in complexity theory that could provide a beginning. But, in my opinion, there is no pressing reason to attempt a formalization.

Ordinary language is rich and complex. For doing mathematics and talking about it, there is no need to try to capture the richness of ordinary language in a formal system. What matters is that when we seek to be precise, we can be. It is possible to use "implies" both formally and informally, with different meanings or at least different connotations.

  • 1
    @Doug Spoonwood: Yes, the formalization of “A follows from B” as “the proof of A mentions the proof of B” seems right to me too. Thus we need to formalize proofs, which is done in logic (proofs are trees, i.e. terms) and in type theory (proofs are lambda-terms). Then we can formalize further to “the name of the proof of B is a free variable in the proof of A.” The *formal* language of proofs is also interesting, and it is distinct from the formal language of propositions/formulas.2011-08-26