[FOM] From EFQ to Research

[Harvey Friedman]

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

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

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?

3. It has been suggested that cut is not needed to formalize actual
mathematical practice. I take this to be prima facie false from the
fact that the blowup in cut elimination is vicious, and there are
beautiful examples. Yes, I am using a 21st century notion of "need"
here. HOWEVER, we do not have varied examples of this and related
phenomena. At the level of pure logic, I suggested looking at the
contests between logic provers, and also the experience of logic
provers - where perhaps they are even cutting all the way through
whole forests?. Also, provers in the context of proper axioms. What in
fact does one see? I would imagine a lot of cuts by the machines, and
probably not removable without some blowup. I don't know if such
unremoveability has been established?

4. A related issue is of course simply that in the presence of
standard proper axioms, one wants to prove an interesting thingie. One
should often find that you must invoke proper axioms that are very
very far from the thingie to be proved. Document this, and prove that
it is essential in fundamental real world situations.

5. For real revisionary-ism, let's ban negation entirely - on the
grounds that negation is simply causing too much controversy on the
FOM (smile). What happens? Systematically, what is really going on?
Maybe even what is going on philosophically? This looks like it has a
lot of deep technical ramifications of an unexpected sort, and my own
view is: where there is new mathematical smoke, there is often new
foundational fire.

6. Even mathematicians who are disgusted by the very thought that
someone can criticize the law of excluded middle and related badass
things that are done all the time, realize that something deep must be
done to avoid it with a so called constructive proof, that often gives
you clearly identifiable computable information, or strongly explicit
information. 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?

7. There is an attempted argument against intuitionists that goes
something like this. Well, I can PROVE that classical PA is sound.
Therefore why are you (intuitionists) complaining about classical PA?
The "fallacy", of course, is that there are nonconstructive steps in
this soundness proof. In this case, the offending steps are very
clearly identifiable. Now, what if I attempt to prove that PA is sound
and the issue is not LEM? In a sense, this is different because
Tennant claims that we can still prove everything we normally prove by
conversion. So then a couple of scenarios arise:

a. Such soundness proofs for the usual systems are Tennant certified.
Then we could have everybody quote that result and proof, and then go
about our usual business ignoring the Tennant turnstile. I.e., use
this as a rubber stamp.

b. Such soundness proofs for the usual systems are Tennant
decertified. Then are these soundness proofs similarly fixable the way
Tennant fixes proofs now? If so, can Tennant rewrite the proof in a
satisfactory Tennant form? Then we can use this fixed proof as a
rubber stamp

In any case, we have the prospect of having a good Tennant Rubber
Stamp, so that the mathematicians can sleep well.

8. Automated conversion? Has Tennant written software that will
convert an arbitrary bad proof into a good one? Then instead of a
rubber stamp, we could have a parallel set of Journals called the
Tennant Journals, which simply takes the proofs appearing in the
present Journals and converts them to proofs conforming to the Tennant
turnstile, and there would be a huge discount available for these new
Tennant Journals.

9. It has been suggested that somehow the Tennant turnstile might be
useful in improving current Proof Assistants - i.e., provers. I have
severe doubts about this, but it does raise the general issue of just
how EFQ and related things get used or non used in the Provers arena?
Independently of this, what do we now know about the frequencies and
patterns present in the Prover logs as to the various logic rules and
logic moves? I think that it is still so painful to get a serious
proof out of the required intimate relationship with a Prover, that
ANY legitimate - in the usual sense that we use - move that stops or
lessens the agonizing pain involved in such work will be seized on
without hesitation - even if it does not conform with the full
approval of (the) Tennant (turnstile). Such are the temptations of
evil. So let's get some hard data on what is really gone on in the
intense battlefield.

10. Finally, I often like to wear Black Hats, at least temporarily.
Can we improve philosophically on the argument that mathematicians
using things like EFQ (and maybe cut) should be jailed or at least
fired? Can we improve on the argument that things like EFQ (and maybe
cut) are philosophically defective? Perhaps by comparison, with the
really "nice" moves? This spills over of course to 1 (which is more at
a technical level). And at the risk of going around in circles, I stop
here.

Harvey Friedman

On Sun, Sep 6, 2015 at 11:09 PM, Tennant, Neil <tennant.9 at osu.edu> wrote:
> There are two matters I would like to address in Alan Weir's
> characteristically insightful comments about EFQ/ECQ.
>
> Alan writes
>
> "... transitive chaining is in fact deeply embedded in ordinary mathematical
> proof and to amend it is highly revisionary."

.....