[FOM] From EFQ to Research 4/External Response 1

[Harvey Friedman]

I just received a response to my inquiry about the significance of EFQ
and cut avoidance for the theorem proving community. I have Jeremy
Avigad's permission to post his reply to me.

Dear Harvey,

Most automated methods rely on classical reductions and/or rules that
presuppose EFQ. In the constructive theorem proving community, most
people are convinced by the usual stories about the computational
interpretation of falsity, so I don't know of anyone in that community
that is keen to give that up.

Of course, in higher-order systems, you can define "false" by "forall
P, P" in which case EFQ is valid. In Coq and Lean, it is defined by an
inductive definition (i.e. the empty one). So, in a sense, these
systems don't rely on EFQ, falsity is simply defined in a way that
makes it true.

In short, I don't know of anyone seriously interested in avoiding EFQ.
Is there any good motivation to do so?

As far as using cut: in interactive theorem proving, of course, we
prove libraries of theorems and use them in proofs. So cut is used all
the time. In resolution theorem proving, one proceeds by negating the
conclusion and trying to prove a contradiction with the resolution
rule, essentially "from 'A or B'  and 'not A' conclude B". So that is
sort of like a "cut calculus". As far as "guessing" lemmas or
generalizations in automated reasoning, there has been some work along
these lines, but I don't know of any striking successes.

Best wishes,

Jeremy

I added Neil's reference in 1. As far as 2 is concerned, there really
isn't much until such basics have been thoroughly examined, as sqrt(2)
is irrational in the form i mentioned, and there are infinitely many
primes. With regard to 3, The letter above from Jeremy Avigad
indicates that in the usual sense of the word "used", cut is used
endlessly in interactive theorem proving.

NEIL WRITES:

I"n Harvey's repeated questions 3-10 inclusive (on this last
iteration), I see no evidence that he has absorbed any of the details
that I offered in response to them in my posting
'From EFQ to Research 2--reply to Harvey Friedman'
http://www.cs.nyu.edu/pipermail/fom/2015-September/019108.html"

I see no evidence that Neil has absorbed my continued suggestions that
he is using standard expressions like "using and avoiding EFQ" and
"using and avoiding cut" in nonstandard ways, which has the effect of
dodging the interesting issues that remain concerning actual
mathematical proofs.

E.g., we have discussed

p, not p |- q
p |- (not p arrows q)
|- p implies (not p arrows q)
|- (p and not p) implies q

The offered treatments of these four have all the trappings of a
rhetorical point that is not responsive to what is going on in actual
mathematical proofs.

There is quite a difference between making rhetorical points in order
to highlight a certain specific line of research, and recognizing and
engaging with the deeper foundational issues.
Rhetorical points cannot succeed in establishing the significance of
any approach for understanding the nature of mathematical proof.

Rhetorical points have a better chance of contributing to a question
like 10 - black hats. This comes up also in the above from Avigad "In
short, I don't know of anyone seriously interested in avoiding EFQ. Is
there any good motivation to do so?"

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

Tennant has provided a number of results in
http://dx.doi.org/10.1017/S1755020315000040. However, no
characterization is available. One is,
according to Tennant, that if A |= B by truth tables, then A |-' B or
A |-' # in the Tennant turnstile |-' (classical logic). Also if A |= #
by truth tables, then A |-' # in the Tennant turnstile.

There are analogous results for the other main calculi such as
intuitionistic propositional calculus, or classical predicate
calculus, and intuitionistic predicate calculus.

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?

According to Tennant, the axioms and rules for quantifiers are
unchanged. But there may be unexpected interactions. What would a
detailed analysis of Tennantism look like for, say, the usual proofs
of

n^2 = 2m^2 has no solution in nonzero integers
p^2 = 2q^2 has no solution in nonzero rationals

for all integers n there exists p > n such that p is prime.

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.

Tennant strongly believes that such soundness proofs can be adjusted
in Tennant standard ways in other to get Tennant certified, thus
leading to a fine Tennant Rubber Stamp.

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.

Tennant has generously offered his own data for perusal. But I was
rather thinking of the stuff in from the Proof Assistants currently in
intense use to create rigorous proofs of very impressive pieces of
mathematics. This is not a one man show, not even for Neil.

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.

11. Tennant has emphasized that all classical (intuitionistic)
validities (provabilities) are provable in his setup. But is there a
rigorous sense in which Tennant's system is either minimal or minimum?
Minimal would mean that any, or any reasonable, weakening of Tennant's
setup results in losing some validities (provabilities).

Harvey Friedman