[FOM] Are proofs in mathematics based on sufficient evidence?

[Richard Heck]

>
> 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 
my opinion.

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 
section 63:
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 
Russell's paradox:
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 Heck

-- 
-----------------------
Richard G Heck Jr
Romeo Elton Professor of Natural Theology
Brown University