[FOM] From EFQ to Research 5

[Harvey Friedman]

Neil objects to my not reading technical accounts/resuults of/about
his turnstile. I generally don't read technical accounts of anything
UNTIL I see a reason to believe that it is worth the effort up front.
And that reason normally is

*do I see a simple short synopsis of what is being accomplished, in
nontechnical standard language, that is easily digestible and
reasonably compelling about an issue of fundamental importance?*

I generally judge the importance for me of some technical subject
someone(s) have created in terms of the extent to which it gains
traction on clearly identifiable foundational issues. If this depends,
as it does in this case, on redefining the normal meanings of basic
terminology, then I have to see up front why that is a productive move
rather than a merely rhetorical move.

In this particular case, we are facing wholly inadequate nonresponses
to two basic questions, that are prior to my reading technical
treatments.

For the first one, I quote from my previous posting:

"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."

It should be emphasized here that p,q are viewed in the above as
propositional letters. There is a separate issue of what goes on that
might take advantage of compound formulas.

Merely displaying some formal derivations in some system one has
invented does not address the issues. For instance, finite lists on
the right of a sequent are normally viewed only as disjunctions, and
not fundamental to mathematical meaning or actual mathematical proof
processes. So the normal attempt one might even try to make at the
differences between these four above, based on some sequent calculus,
or some equivalent version with natural deduction, is simply going to
bury EFQ in another format. This is what I mean by redefining the
problem.

This is exactly what occurred when Neil was challenged to give a proof
of "emptyset included in A" without use of EFQ. Neil just repeated the
usual proof of this with EFQ. Why does Neil say that his proof
allegedly without using EFQ doesn't use EFQ? Because "not using EFQ"
has been carefully defined in a way to justify a technical
development.

In short, redefining what it means by "avoiding EFQ" and then proving
that you can "avoid EFQ" does not get us anywhere. It is a solution in
search of a problem.

I am not going to be reading technicalities until I see a compelling
rationale for the offered treatments of these four items. If the
offered rationale is of a rhetorical nature, sidestepping legitimate
foundational issues as to the nature of mathematical proofs, then I
will continue to complain and not read any technicalities.

The second one is well illustrated by this statement of Avigad, and
Neil's response:

AVIGAD

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

TENNANT

"Yes, very good motivation: it ensures relevance, does not sacrifice
transitivity of deduction, and respects intuitions. Unfortunately,
however, the suggestion that we can and should explore the benefits of
avoiding EFQ gets some people really worked up!"

Here Neil fails to mention that the bidirectional Deduction Theorem is
destroyed, which is probably considered by most to be far more
egregious than any kind of irrelevance. Why doesn't Neil mention the
crucial fact that the bidirectional Deduction Theorem is destroyed?

Furthermore, there is also no indication of why irrelevance is even a
negative feature. After all, irrelevance occurs all through math and
all through life. So Neil is failing to engage Avigad (though the FOM)
even at the most fundamental motivational level.

Again, this suggests a rhetorical way of redefining the normal use of
the phrase "avoiding EFQ" that sidesteps any legitimate foundational
issues. If I see anything stated in nontechnical compelling terms that
points in the opposite direction, then my view of this changes.

Instead of "why and how and where is EFQ essential" we have "I can
redefine what we mean by "EFQ is essential", and avoid EFQ in my
system". So what? It doesn't change the legitimate foundational
issues. And it doesn't give any prima facie reason to even look at
such a system.

The same rhetorical methods are used to redefine the normal use of the
phrase "avoiding cuts" that sidesteps any legitimate foundational
issues. Look here:

AVIGAD

"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."

TENNANT

"Note the adjective "interactive". But more importantly: we don't have
to described this by saying "cut is used". That holds only if one
actually applies a rule of cut in constructing a proof. One could,
instead, simply refrain from cuts, and gather together all the
sections of cut-free proof. It's what good writers of textbooks in
mathematics actually do! That *there is* a proof of the 'overall'
result is guaranteed by the cut-admissibility result."

Instead of "why and how and where is cut essential" we have "I can
redefine what we mean by "cut is essential", and avoid cut in my
system". So what? It doesn't change the legitimate foundational
issues.

FRIEDMAN
>
> "I am still entirely skeptical on whether this work of Tennant offers
> up anything for the rather advanced and involved prover world, for any
> of the usual calculi."
>
> "I am starting to ask that community whether
> issues such as restricting EFQ or cut play any practical or
> theoretical role in the Proof Assistant work. And generally, if they
> have found any intelligible features of actual proofs that distinguish
> them from possible proofs."

TENNANT
>
> I can predict right away that this inquiry will be fruitless. How many of
> the informants in that community have even the remotest grasp of the
> subtleties and details of Core Logic?

FRIEDMAN

I indicated what kind of thing is needed for the Prover Community to
even consider looking at unorthodox turnstiles like Tennant's. These
necessary things are not being offered.

TENNANT

> Will they have been following this
> discussion on FOM in the necessary detail, so as to be aware of the extent
> to which Core Logic's credentials have remained unscathed, despite the best
> efforts on the part of lifelong users of the orthodox systems to pick holes
> in it, or to find something they want logic to do but which Core Logic
> supposedly cannot do?

FRIEDMAN

We are not even at the point where any "credentials" even come into
play, since the necessary prerequisites that I indicated above are not
even being offered. Failure to provide these prerequisites is not a
convincing way to remain "unscathed". One simply gets "unengaged"
which is quite different.

TENNANT

> I predict that Harvey will come back to this list with
> what he thinks is authoritative confirmation of his position; and the
> 'expert' criticisms thereby allegedly conveyed of Core Logic from that
> "rather advanced and involved" world will once again fall to rebuttal if
> ever the hearsay evidence becomes first-person testimony on this list.
>
FRIEDMAN

There won't be any rebuttal by Neil, but simply a repeat of rhetorical
points. Specifically, a repeat of rhetorically based redefinition of
"EFQ avoidance" and "cut avoidance". You can't seriously engage a
problem by simply changing definitions of the problem to make it go
away. YES, you could attempt to argue that the new definitions are in
some sense clarifying or superior to the usual definitions. A START at
that would be to address my prerequisites : my two basic questions in
the fourth paragraph of this posting.

Harvey Friedman