[FOM] The incomplete logic needed for mathematics

[Harvey Friedman]

Since you say that this ancestral logic is an extension of FOL, does
it come equipped like FOL with a recursive set of axioms that can be
displayed nicely, regardless of whether or not you have a suitable
completeness theorem?

And since it is as you say an extension of FOL, is there nicely
presented recursively axiomatized systems as such?

1. An Ancestral arithmetic which is essentially different from PA?
2. An Ancestral Z_2 which is essentially different from Z_2?
3  An Ancestral Z which is essentially different from Z?
4. An Ancestral simple theory of types essentially different from the usual?
5. An Ancestral ZF essentially different from ZF?

Harvey Friedman



On Wed, Sep 9, 2015 at 11:12 AM, Arnon Avron <aa at tau.ac.il> wrote:
> 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