[FOM] From EFQ to Research

[Mario Carneiro]

On Mon, Sep 7, 2015 at 2:29 AM, Harvey Friedman <hmflogic at gmail.com> wrote:

> I am still interested in delineating productive research programs
> surrounding this discussion. Here is a list getting longer. And I
> probably have forgotten some.
>

I think I can answer or at least address some of these questions. Like you
I also believe that the main property being addressed in Core logic is one
of proofs, not of the turnstile. To fix some terminology, let us call a
proof conforming to Tennant standards a Core proof, and the Tennant
turnstile asserts the existence of a Core proof. Assume that there is
already an ambient notion of 'classical proof' such as natural deduction,
of which Core proof is a reduct.


> 1. What can we prove about the Tennant turnstile? With propositional
> calculus with atoms p,q,r,... we do not have p,notp |- q. But we do
> have p |- notp arrows q. What essential feature, capable of
> generalization, does one have but not the other? E.g., do we have a
> completeness theorem to the effect that the Tennant turnstile has some
> general strategic properties, and no turnstile stronger than the
> Tennant turnstile shares such exquisite general strategic properties
> (whatever they are)?
>

I believe the key property is, as mentioned earlier by Tennant, the
minimality property: no proper subproof of a Core proof of A:B proves a
subsequent of A:B (i.e. A':B or A':# for some subset A' of A), and the
subproofs of a Core proof are Core proofs. To ensure that there are any
core proofs, one can demand that every classical proof is a subsequent of a
Core proof. This should get you close to uniqueness of the "is a Core
proof" predicate, but you might need additional conditions. In particular,
one needs to choose the inference rules for classical proof correctly so
that all the desired 'invalid' moves are detected in subproofs. For
example, if EFQ is written as #:A, then any proof of A:B using EFQ will
contain the proper subsequent A:# in the previous step.


> 2. What is being offered for first order predicate calculus? I have
> not seen the Tennant turnstile in action on the FOM with quantifiers.
> Here are there more things mathematicians prove normally and quickly
> that do not conform, maybe well beyond, emptyset containedin A?
>

I believe that Tennant said in one of his postings that "Gentzen got
quantifiers right": all the quantifier rules are unchanged in Core.


> 6. What is the best example, if any, of just exactly what we
> know if we have conformed to the Tennant turnstile? If you conform to
> not using negation at all, then this has profound consequences of an
> algebraic nature, in the case of arithmetic. Now I recognize the
> difference here that the Tennant turnstile does not affect what is an
> acceptable theorem, just what is an acceptable proof. So the answer
> for the Tennant turnstile has to be more nuanced. That something
> happens of a clearly identifiable mathematical nature in the proof
> conforming to the Tennant turnstile that doesn't happen in a proof not
> conforming to the Tennant turnstile?
>

What happens in a Core proof that does not happen in a non-Core proof is
the certification that you have not wasted time proving something
manifestly inefficiently (i.e. you already proved the result somewhere
earlier in the proof tree, but forgot and kept going), and additionally
your result is the sharpest you can make it w.r.t thinnings - there are no
hypotheses to the theorem that are not used somewhere in the proof, and you
did not inadvertently prove that the hypotheses are contradictory (unless
your result claims exactly this).

Note that since these are properties of *your particular proof*, and not
all proofs of the statement, you do not actually know that your proof is
the sharpest possible, only that it is sharp with respect to subproofs of
your proof. Thus if ZFC is inconsistent there may be a Core proof of ZFC:A
(where A is your favorite ZFC theorem) and also a Core proof of ZFC:#,
where the Core proof of ZFC:A is a normal one that does not approach the
line of reasoning that gives a contradiction in ZFC.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150907/9cf73e7c/attachment-0001.html>