FOM: logical vs mathematical

[Till Mossakowski]

Martin Davis wrote:

>The issue of in what sense higher order logic can reasonably be considered 
>as "logical" while set theory must be regarded as "mathematical" has come 
>up in exchanges between Harvey Friedman and Joe Shipman. Quine addressed 
>this (I think in a conference paper in 1960). He pointed out that the 
>theorems of what he called SOL (by which he meant the standard at that time 
>deductive systems studied by Hilbert-Ackermann and Church) divide neatly 
>into two classes: those that depend on comprehension and those that follow 
>just from the first order deductive rules. He proposed that only the 
>theorems of the second class should be considered logical since those of 
>the first, in their intended interpretation, have ontological presuppositions.
>
>I was convinced and have taken that position ever since.

Actually, the "theorem proving in HOL" community has formalized a good 
portion of mathematics in

	HOL + comprehension + Axiom of infinity

This system is obviously weaker than ZFC, but still it has some
technical advantages (namely the use of lambda abstraction,
and the Hilbert choice operator, among others), that make computer-assisted
proofs easier.

Both comprehension and infinity are not part of HOL, but they are
added as axioms later on. They seem to be the minimum of mathematical
axioms that are needed to formalize any reasonable part of mathematics.

Till Mossakowski
-----------------------------------------------------------------------------
Till Mossakowski                Phone +49-421-218-4683, monday: +49-4252-1859
Dept. of Computer Science       Fax +49-421-218-3054
University of Bremen            till at informatik.uni-bremen.de           
P.O.Box 330440, D-28334 Bremen  http://www.informatik.uni-bremen.de/~till
-----------------------------------------------------------------------------