[FOM] The incomplete logic needed for mathematics

[Arnon Avron]

On Fri, Sep 04, 2015 at 01:27:50AM -0400, Harvey Friedman wrote:
 
> EVEN MUCH MORE INTERESTIiNG, would be to show that mathematicians
> actually work in a (natural, coherent, identifiable) system of logic
> that is INCOMPLETE. That could have major implications for all sorts
> of issues in f.o.m.

I guess you are not going to agree, and it is most probably
not what you have in mind here, but I believe that it is relevant
to point out that for many years now I am claiming that this is indeed what 
mathematicians do. I think that  the *logic* underlying
math is ancestral logic, which is an incomplete extension of FOL.
Nothing less than it would suffice  even for defining the most
basic notions of formula, formal proof, and natural number; it is
no less universal than FOL (in fact, it is used and understood even by the 
famous "man in the street"), and it involves no doubtful ontological 
commitments like second-order "logic" does (SOL is in my opinion
just set theory in disguise, as Quine has said with full justice).

  Here are references to two papers of mine which explain and provide support
for this thesis:

"Transitive Closure and the Mechanization of Mathematics",
In  "Thirty Five Years of Automating Mathematics"
(F. Kamareddine, ed.), 149-171, Kluwer Academic Publishers, 2003.

"A New Approach to Predicative Set Theory",
In "Ways of Proof Theory" (R. Schindler, ed.), 31--63,
onto series in mathematical logic, onto verlag, 2010.

Arnon Avron