[FOM] From EFQ to Research---reply to Harvey Friedman's questions 4-10

[Tennant, Neil]

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

This is too general for me to be able to offer any useful claims about the
possible advantages of using the core systems in situations like this.
________________________________________________________

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

I'm all for looking at proper fragments. Go for it!
________________________________________________________

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

I would say the knowledge of the connections of relevance described in
my earlier posting dealing with your first three questions.

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

The relevance thingie again.
________________________________________________________

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

May I charge a fee for this rubber stamp?  :-)
I believe that all these soundness proofs will be easily formalizable in
 Classical Core Logic (in the metalanguage) anyway---as with any
 mathematical theorem proved from mathematical axioms.
 We all believe the axioms are consistent; so, the core proofs will
 always be of the thingie you want to prove, rather than #.

________________________________________________________

"8. Automated conversion? Has Tennant written software that will
convert an arbitrary bad proof into a good one?"

No, but I would foresee no difficulties in principle in doing so.
I shall write the software in Prolog, but only if the price is right---
say, double my current salary, inflation-adjusted, with no teaching
obligations, until 2020.  OK?

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

I don't know what the word "simply" is doing there. You want to take the
 'proofs appearing in the present Journals' as *inputs* to a mechanical
 conversion process?! You would need 2^100 Tennant clones operating
 in parallel at the terrabyte/second level to pull this off. [You would also
 have to sustain their focused interest in the operation, which would be
 an entirely different problem.] I should imagine the Tennant Journals,
 if they were ever to come into existence, would have an absolutely gigantic
 impact factor, and would never need to offer any discounts. We would
 probably be able to hire Donald Trump as our sales rep.
________________________________________________________

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

It's not used in my own automated proof-finder for propositional Core Logic.
As a matter of related interest: it was not used by Aristotle in his syllogistic, either!

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

I don't know what would count as 'hard data' here. I could send you a
file containing natural deductions around 5,000 steps long, generated
in mere milliseconds by my prover. You would be welcome to eyeball
them for interesting patterns.
________________________________________________________

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

I think we should build a big wall around the area where EFQ will
not be allowed, and get all the orthodox logicians on the outside
to pay for it. But then they might not be able to afford their subscriptions
 to the Tennant Journals.

Neil Tennant

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150908/b10c4698/attachment.html>