[FOM] From EFQ to Research 3

Thu Sep 10 14:21:36 EDT 2015

Tennant's reply to my EFQ to Research 2 provided some more
information. But all of the research items seem to be very much still
in play. I think there are still some issues involved in carrying out
the plan in question 7 that ought to reveal something interesting.

Neil refers to some technical notion of relevance from an earlier
posting, Since there are so many earlier postings, a short posting by
Neil restating this notion in simple words, without natural deduction
diagrams, would be helpful - assuming it bears on the questions below
- particularly 6.

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.

With regard to systems without negation, I plan to deal with this
systematically on numbered postings.

I have added some comments and editing.

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

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

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