[FOM] The incomplete logic needed for mathematics

[Harvey Friedman]

Let me restate what I was most interested in along the lines of
unconventional formalization. Your answer is not exactly what I am
looking at, but is interesting nonetheless.

I was looking for a restriction on FOL based on observations about
actual FOL used in real mathematical proofs.

Suppose one could spot some restriction - that mathematicians stay
within X, a fragment of FOL.

Then we might have the following kind of phenomena:

1. PA based on X instead of full FOL is a system that can be proved
consistent within PA.
2. Same with a number of other systems. E.g., ZFC based on X can be
proved consistent within ZFC.

In some sense, we already do this, but in an unexciting way. We adhere
to the fragment of FOL where proofs have size at most, say, 2^1000.
Yes, you can prove that PA based on this restriction is consistent
within PA. However, presumably not if you make the corresponding
restriction on PA when proving such consistency. I called this finite
Goedel's theorem - not quite this strong a result. It was followed up
by Pavel Pudlak, Theorem 6.2.3,
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=7935D5CE84D16C4C2FC12BB9ED7E5E01?doi=10.1.1.156.3109&rep=rep1&type=pdf

The classic situation along these lines is to use intuitionistic FOL
instead of FOL - even though mathematicians do not generally adhere to
this. In any case, we know already from Goedel that PA does not prove
the consistency of HA.

Instead, your ancestral logic is an extension, not restriction, of
FOL. So from the point of view of the above 1,2, we are talking about
something quite different. Namely, a restriction of SOL = second order
logic - and an extremely weak such restriction at that.

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

Is your use of the word "rule" here importantly different than just
saying that nobody has suggested a natural valid sentence of ancestral
logic which is not provable in the commonly associated proof system?

This raises the following general question. Call a system T *naturally
complete* if every natural sentence in the language of T that is
valid, is provable in T.

Are you suggesting that Ancestral Logic with usual axiomatization is
naturally complete? And what about other systems being naturally
complete?
>
> 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?
>
>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.)

This sort of thing happens also with Count Arithmetic, where you don't
even need S,+,dot. See the discussion near the end of
http://www.cs.nyu.edu/pipermail/fom/2015-September/018978.html

There is also the question of interesting decision procedures for
fragments of ancestral logic.

Harvey Friedman