[FOM] Are proofs in mathematics based on sufficient evidence?
rgheck at brown.edu
Fri Jul 9 21:32:26 EDT 2010
> On Thu, Jul 8, 2010 at 5:17 PM, Martin Davis<eipye at pacbell.net> wrote:
>> > Gottlob Frege discovered the simple logical rules of inference that
>> > underlie mathematical proofs.
On 07/09/2010 01:25 PM, Robert Lindauer wrote:
> In Frege's system, obviously the Frege's foundations of Arithmetic is
> primarily a philosophical exploration in which he contrasts -not
> completely fairly- opposing views of the concept of number, and
> proposes his own concept of number (again philosophical) which is in
> turn contradictory.
First of all, Frege's account of what Davis calls "the simple logical
rules of inference that underlie mathematical proofs" is quite
independent of any of the problems that afflict his account of number.
The account of logical inference is present already in
/Begriffsschrift/, and the more mature account given in /Grundgesetze/,
minus the problematic account of extensions of concepts, is essentially
what we now know as higher-order logic. Frege himself fully understood
the point that is, I take it, implicit in Davis's remarks, namely: We
must /of course/ distinguish the question "have we reasoned correctly?"
from the question "was the starting point of our reasoning sound?" (See
the paper on Peano, e.g.) What Davis is claiming is that Frege
discovered the answer to the former question, as least in some ideal,
normative sense. The answer to the latter---what the axioms should
be---is another matter entirely. Frege did think he had an answer to
that question, but it is there that he was, it would seem, wrong.
No progress is possible here unless we carefully distinguish these
questions. And, to my mind, the critical question that Vaughn raised
needs to be formulated in this light. It does seem a characteristic of
/mathematics/ that proofs are supposed to be /deductively/ valid,
whereas proofs in other realms do not have to meet that high standard.
Whether that means there are different notions of proof is not obvious,
but it makes clear where the issue is.
That said, even if we do consider Frege's account of the concept of
number, it is not that account as such that is contradictory. This ought
by now to be well-known. It is something of a scandal that it is not, in
Part of the problem is that it is not clear what we should mean by
"Frege's account of the concept of number". There are two options. The
first is the definition given in section 68 of /Grundlagen/:
the number belonging to the concept F is the extension of the concept:
equinumerous with the concept F
or the equivalent definition from /Grundgesetze/. The second option is
the characterization in terms of "Hume's Principle", or HP, given in
the number of Fs is the same as the number of Gs iff
there is a 1-1 correlation between the Fs and the Gs.
Neither is contradictory, in its own right.
Let's start with HP. HP is consistent, even in full second-order logic,
and it implies full second-order PA. Indeed, PA2 is equiconsistent with
FA2 = 2OL + HP, provably so over a very weak theory. For that reason, of
course, FA2 is proof-theoretically no stronger than PA2, so one might
not regard FA2 as a fully adequate foundation. Then again, some people
might think that is plenty of mathematics. And much finer-grained
results are available. E.g., for any fragment K of 2OL containing
Pi_1^1-CA, we have: HP + K = PA + K. That suggest a very intimate
relationship between HP and PA, which it is hard to see is not of
foundational interest. There are even extensions of such results to
weaker (predicative) logics, but these are swallowed by what follows,
mostly. And I have what I think are really nice extensions of such
results to first-order logics plus a scheme of parametric definition.
So let's talk about Frege's section 68 definition, in terms of
extensions. Then we need a theory of extensions, which is what leads to
the extension of F = the extension of G iff (x)(Fx <--> Gx)
That's inconsistent in 2OL and, indeed, in any fragment of 2OL that
yields Pi_1^1-CA or Sigma_1^1-CA. But it is consistent in (ramified)
predicative 2OL and even in Delta_1^1-CA, and in such theories it yields
a reasonable fragment of arithmetic: one containing what Harvey calls
EFA, or other people call I\Delta_0 + exp, and even something a bit
stronger, though it does /not/ yield superexp. (Work by Albert Visser
has allowed us to understand the strength of this theory pretty well.)
There is thus an extremely natural predicative theory that is
recoverable from Frege's work. Again, not one sufficient to found all of
contemporary mathematics, but the view that ALL of contemporary
mathematics has a logical foundation was always pretty bold. Maybe only
some of it does.
Richard G Heck Jr
Romeo Elton Professor of Natural Theology
More information about the FOM