[FOM] From EFQ to Research 3---further reply to Harvey Friedman

[Tennant, Neil]

There were some matters that I did not take up from Harvey's posting 'From EFQ to Research 3', and I need to deal with them here briefly.

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

The posting that explained this notion of relevance in simple words was
'From EFQ to Research---reply to Harvey Friedman's questions 1-3',
http://www.cs.nyu.edu/pipermail/fom/2015-September/019084.html

That Harvey did not immediately recall this part of my posting in connection with the topic of relevance may be owing to the circumstance that I wrote of "extralogical-vocabulary-sharing", rather than relevance. So I shall repeat here, with minor additions, what I wrote about the topic. The minor additions are in uppercase, and are not meant to be understood as screaming.
___________________

[T]here is a very strong result about extralogical-vocabulary-sharing, for first-order Classical Core Logic. Let P be a Classical Core proof of the conclusion A from the set X of premises. (Note that A can be #.)
I SHALL NOW DEFINE A RELEVANCE CONDITION R(X,A). FOR EVERY SEQUENT X:A THAT IS PROVABLE IN CLASSICAL CORE LOGIC, WE HAVE R(X,A).
There are three cases to consider:
(1) X is empty (so A is a theorem).
(2) A is # (so X is inconsistent).
(3) X is non-empty, A is not #.
In Case (1), A will have both a positive and a negative occurrence of some primitive extralogical expression.
In Case (2), every sentence in X connects to every other sentence in X by means of a path on which any two neighboring sentences contain some same primitive extralogical expression with opposite parities.
In Case (3), X partitions into components that are internally connected in the way just described for Case (2) [where X was the sole component]. Every component X' of X contains some sentence B such that some primitive extralogical expression enjoys an occurrence in B and an occurrence in A of the same parity.

THIS RESULT WAS PROVED IN MY PAPER
‘The Relevance of Premises to Conclusions of Core Proofs’, Review of Symbolic Logic, 8, no. XXX, 2015, pp. XXX-XXX, DOI: http://dx.doi.org/10.1017/S1755020315000040. The intrested reader can download a .pdf from my publications webpage . It's #6 under 'Articles'.

FAMILIARITY WITH THIS PAPER WILL BE PRESUMED IN ANY FURTHER CONTINUATION OF THIS DISCUSSION WITH HARVEY. I KNOW THAT THIS IMPOSES AN OBLIGATION TO READ CERTAIN PUBLISHED WORKS BY OTHERS IN REFEREED JOURNALS. I APOLOGIZE PROFUSELY TO ALL CONCERNED FOR IMPORTUNING THEM IN THIS WAY.

REMEMBER, THE COMMENTS IN UPPERCASE ARE NOT MEANT TO BE UNDERSTOOD AS SCREAMED.

_______________________

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

And the reasoned basis for such skepticism is ... ? And after reading my book Autologic when?...

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

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

Neil Tennant

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150912/990779f4/attachment-0001.html>