[FOM] From EFQ to Research---reply to Harvey Friedman's questions 1-3

[Tennant, Neil]

"1. What can we prove about the Tennant turnstile? ... do we have a
completeness theorem to the effect that the Tennant turnstile has some
general strategic properties  ... ?"

For definiteness, let's discuss Classical Logic versus Classical Core Logic.
Let |= be the familiar double turnstile of logical consequence, with respect to which soundness and completeness of proof systems are usually proved. Note that whatever single turnstile (for whatever proof system) one has, completeness is stated in the loose form (X a set of sentences, possibly infinite; and A a sentence)

            X |= A  =>  X |- A

Unpacked: if for every model M, M makes all of X true only if M makes A true, then there is a proof with conclusion A whose premises are drawn from X (and do not necessarily exhaust X). The parenthetical remark is obviously called for when X is infinite, since proof is finite. Now, since completeness can hold with 'subsetting down' on the left of the sequent X:A, there is no reason why it should not hold with subsetting down on the right. That is, no loss of ocmpleteness can be alleged if, when there is no proof of A from (members in) X, there is nevertheless a proof of # from (members in) X.

With this clarification, we know that Classical Core Logic is complete:

       X |= A   =>  there is a Classical Core proof of A or of # from (members in) X

Corollaries:

(i)      |= A (i.e. A logically true)  =>  there is a Classical Core proof of A from no assumptions

(ii)    X |= # (i.e. X not satisfiable)  =>  there is a Classical Core proof of # from (some subset of) X

(iii) (X satisfiable and A not logically true and X |= A)  => there is a Classical Core proof of A from (some subset of) X

We also know

(a)  If P is a classical core proof of X:A and P' is a classical core proof of A,Y:B, then there is an effectively determinable classical core proof [P,P'] of A or of # from (some subset of) X,Y

(b) if classicization of Core Logic is by adding Dilemma, then [P,P'] can have a lower degree of non-constructivity than the higher of the two such degrees for P and P'

(c) if classicization of Core Logic is by adding Classical Reductio, then such reduction of degree of non-constructivity is not to be had

(d) there is a linear-time algorithm f such that: for all normal proofs P of X:A in Classical Logic (with EFQ permitted) where the classical rule is Classical Reductio, f(P) is a Classical Core proof of some subset of X:A

(e) if classicization is by adding Dilemma, then the linear-time algorithm of (d) is not to be had.

Finally, there 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 #.) 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.

___________________________________________________________

"... [Can we prove that] no turnstile stronger than the
Tennant turnstile shares such exquisite general strategic properties
(whatever they are)?"

The tight connection of relevance among premises and conclusions of classical core proofs is a candidate property, I believe, with respect to which the turnstile of Classical Core Logic might well be maximal.

___________________________________________________________

"2. What is being offered for first order predicate calculus? I have
not seen the Tennant turnstile in action on the FOM with quantifiers."

The rules for the quantifiers are exactly the same in the core systems as in the orthodox systems. That's just as well!---it makes the formalization of mathematical reasoning by means of the core systems very direct. (Weierstrass lived in Core, even if he did not realize it!)

___________________________________________________________

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

As Harvey well knows---since he is so good at this---the judicious choice of lemmas is key to breaking long proofs down into manageable bits. The lemmas become cut sentences if one uses an explicit rule of cut in your system.

I am suggesting that we should simply do without an explicit rule of cut. Make do instead with formalizations of just those bits of proof---the 'links in the chaining', to use Alan Weir's image---that contain no cuts within themselves. The net effect of the desired chaining is guaranteed by our result about reducts. The result estabishes, in effect, the Admissibility of Cut (with potential epistemic gain) for the cut-free core system. Nothing is lost, epistemologically (concerning what follows from what), by refraining from "applying cut' rather than going ahead and applying it!

Neil Tennant

[coverage suspended for the Ohio State-Virginia Tech season-opener grudge re-match]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150908/fd4c61bd/attachment-0001.html>