[FOM] The incomplete logic needed for mathematics

[Arnon Avron]

On Wed, Sep 09, 2015 at 11:30:40AM -0400, Harvey Friedman wrote:

> 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?

Yes. Up to equivalence, and as long as we restrict attention to the 
transitive closure of binary relations (which is insufficient unless 
pairing functions are available) there is basically one corresponding
natural proof system. In Hilbert-type form it was already 
given by R. M. Martin in the forties and by J. Myhill in 1952.  
I myself prefer a rather natural Gentzen-type equivalent formulation,
whose main rule generalizes Gentzen's translation of the
induction schema into a rule (in his version of PA). 
I should add here that this Gentzen-type does *not* admit
cut-elimination (although some important fragments of it do),
and it is a challenging problem to find one that does. Anyway,
to my best knowledge, although the set of valid formulas
of ancestral logic is not r.e., nobody has ever suggested
a valid rule of it which is not derivable in this proof system,
and  again I think that it is an important research question to 
find one.

Now the power of the above-mentioned system becomes strictly stronger if
the introduction of TC^{2n} is allowed also for n>1. However, no new 
idea is involved in the corresponding reformulation of the rules.
  
> 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?

This depends on the question what you mean by "essentially different".
In the official language of PA (with both + and * as primitives)
the use of ancestral logic with the above-mentioned natural
proof system does not provide any extra power, since the use of TC
can be simulated by using Godel-type representations of finite
sequences of numbers. On the other hand, the use of ancestral logic
makes unnecessary this artificial  introduction by brute force of  
+ and * as primitives - 0 and S suffice. (To be more 
precise, if one uses only TC^1 then * can be defined in terms of
0,S, and +, but + should still be taken as primitive. However,
with TC^2 one can define also + in terms of 0 and S.)

> 2. An Ancestral Z_2 which is essentially different from Z_2?
> 3  An Ancestral Z which is essentially different from Z?
> 5. An Ancestral ZF essentially different from ZF?

The answer here is again: nothing essentially different
can be achieved by using ancestral logic with the above-mentioned natural
proof system. This is not surprising, given that to my
best understanding (please correct me if I am wrong)
no essentially different ZF (say) is obtained if one uses
as the underlying logic one of the standard incomplete
systems for SOL (instead of FOL). SOL (which is not a logic
in my view) is strictly stronger than ancestral logic.

  On the other hand the use of ancestral logic instead of FOL
makes an essential difference when it comes to systems
in which the definitional power is a major issue, like
in predicative set theories. To see this I refer you to my
paper on predicative set theories mentioned in my previous posting
(enclosed below).

> 4. An Ancestral simple theory of types essentially different from the usual?

Here it would be appropriate to mention a very recent work of Bob
Constable and my Ph.D student Liron Cohen. It is
the paper "Intuitionistic Ancestral Logic" which will appear in 
the Journal of Logic and Computation (JLC). They define in it
intuitionistic Ancestral Logic (iAL), which extends intuitionistic FOL. iAL
is a dependently typed abstract programming language with computational 
functionality given by its realizer for the transitive closure operator, TC. 
They derive this operator from the natural type theoretic definition of TC 
using intersection, and show that provable formulas in iAL are *uniformly*
realizable. Thus iAL is sound with respect to constructive type theory. It is 
conjectured that iAL is also uniform complete.  A short version of that 
paper can be downloaded from 
http://www.springer.com/cda/content/document/cda_downloaddocument/9783662477083-c2.pdf?SGWID=0-0-45-1514430-p177539457.

Now I am not sufficiently competent in constructive type theory to judge
to what extent this is "essentially different from the usual" -
and it again might depend on what is meant by the fuzzy notion of
"essentially different".

Arnon


> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom