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

[Harvey Friedman]

On Mon, Sep 7, 2015 at 10:37 PM, Tennant, Neil <tennant.9 at osu.edu> wrote:
> "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  ... ?"
>
...
> 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
>
This is of corse different than

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

So you don't have literal completeness, but a partial result. And
therefore, my research question seems to still stands: what,
mathematically, is the Tennant turnstile?

Now maybe this is readily answerable, or maybe even Neil has already
answered it. But I don't see the answer readily accessible in his
reply to me.

Does the following sum up the state of affairs here:

"There are some strong sufficient and some strong necessary conditions
for the Tennant turnstile, but we do not have a satisfactory exact
characterization".

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

But can you make a stab at defining what a "tight connection of
relevance" is between premises and conclusions? Obviously, even I can
understand that that is what is at issue.

> "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!)

The quantifier rules may be identical as written, but their
interactions with the Tennant propositional turnstile might be rather
subtle, and there may be a lot more examples of mathematicians
behaving badly when proving a lot bigger variety of things than "empty
set contained in B".

E.g., what happens if you examine the several usual proofs that

p^2 = 2q^2 has no solution in rationals p,q.not= 0.
>
> "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. ..."
>
> I am suggesting that we should simply do without an explicit rule of cut.

But then, prima facie, this will not be a faithful representation of
mathematical proofs.

> 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!
>
So Tennant is adjusting the notion of "faithful formalization of
mathematical proof" here to avoid the need to address the deep cut
phenomena. I would imagine that Tennant is interested in a variety of
deep foundational issues surrounding his main interests. Sidestepping
these deep foundational issues by restating the rules of engagement
does not move us forward toward a deeper understanding of the really
exciting issues that have real traction.

Harvey Friedman