[FOM] Concerning EFQ and Cut

[Harvey Friedman]

Since Neil's reproof of

empty set is contained in A

in normal mathematical language still has the idea that a
contradiction yields anything, what Neil writes must be tied to some
idiosyncratic way of looking at the formalization of proofs.

In fact, there ought to be a theorem to the effect that any proof of

"empty set is contained in A"

must have the idea that a contradiction yields everything. ONCE I see
a proof of this theorem in NORMAL mathematical language that does NOT
have the idea that a contradiction yields anything, then I can REVISIT
the matter in some productive way. Until then, we are simply being
presented with the fact that in some formalization associated with
mathematical proofs, you can replace one rule or axiom scheme by
others.

NEVERTHELESS, the fact is that the normal way mathematicians prove
this and similar things DOES explicitly use the idea that a
contradiction yields anything. So even if there is a way of proving
the above without explicitly using the idea - which I have not seen -
there is the question of just why we should be changing the way
mathematicians write proofs along these lines?

ALSO - what about asking the only people on the planet who create
absolutely rigorous proofs of serious mathematical theorems, the proof
assistance people, like. e.g., the MIZAR people, what EFQ and EFQ like
things look like in their systems, and whether they use them? I wonder
if Neil has connected with them about just this?

There are a couple of other aspects of this. I see "ghastly EFQ". I
don't know of a single working mathematician who has this view. For an
analogous situation

c times x

for integers c,x, does really depend on what c,x is. They are both
relevant --- EXCEPT when c is not 0. This is very much like EFQ to a
working mathematician. That 0 times x has answer with x being
irrelevant. Why should EFQ be any different, conceptually, from this
basic situation?

Which of the following

A or (A implies B)
(A and not(A)) implies B

are "Ghastly"? When I occasionally see something like the first one, I
either go to truth tables, or I reason like:

case 1. A. Done.
case 2. not A. Assume A. Then B. Done.

For the second:

Assume A and not(A). Then A, not(A). Contradiction. Hence B.

Are these proofs "Ghastly"?

Now let me turn to the "cut" aspect of this. Here I think we can also
turn the discussion into productive channels.

You cannot prove any of

1+...+1 = 0 implies 1 = 0

for more than one plus sign. And if you add all of the above axioms to
the negation free PA I wrote about, you still cannot prove a whole
bunch of things. By the way, with or without the above axioms, the
system is decidable, and provable consistent within EFA. But I leave
this discussion for now, falling short of getting into some deeper
issues

On the "cut" side of things, I think Neil is offering up a system with
no cut. And once again, one has a proof that cut is not needed.

However, cut is badly needed in a different sense. If we are talking
about pure predicate calculus, we know that there is a super
exponential blowup. In a real world example, there simply cannot be a
super exponential blowup in an appropriate formalization of an actual
mathematical proof, since the Solar System does not have enough room
for proofs of this kind of size.

Once again, the issue of whether cuts REALLY are used, or REALLY can
be removed, depends on the exact way you formalize mathematics. Here
again, consulting the MIZAR or other similar kinds of people, would be
important. There are contests surrounding proving validness in
predicate calculus alone, even though these days, much more attention
is paid to interacting with proper axioms.

I would guess that these experts are armed with plenty of examples of
predicate calculus validities with proofs by hand and by machine with
cuts, but where it is much harder to eliminate the cuts, OR EVEN where
it is suspected that there is a serious blowup, and EVEN where it is
known that there is a serious blowup.

The best examples of known blowup are somewhat nice. They involve
induction for a free predicate symbol on the numbers below 2^2^...^2.
One needs a very small number of proper axioms, and these are put on
the left side of the implication. Here there is provable blowup, AND
the proofs with cut are very natural. As interesting as these examples
are, it would be fascinating to get a variety of real world examples
like this, to understand the boundary between cut elimination being
reasonable, and cut elimination being ridiculous.

Harvey Friedman

On Thu, Sep 3, 2015 at 12:06 AM, Tennant, Neil <tennant.9 at osu.edu> wrote:
> Let me address Harvey's complaint (to the Core logician) that
>
> "... the significance of what you are saying for
> actual mathematical proofs is not at all apparent. The distinction you
> seem to be making does not seem to reflect in the way mathematicians
> write or think of proofs."
>
> and enter once again my respectful disagreement.
>
> Avron asked how the Core logician would prove the simple set-theoretical
> statement "the empty set is included in every set". I showed exactly how the
> Core logician would do this. Remarkably, Harvey ended up offering as the
> best possible *informal* proof a passage in logician's English that
> translates directly into a core proof. (That he did not see this seems, to
> me, to be evidence for the charitable hypothesis that he might be conflating
> Core Logic---for want of thorough familiarity with that system---with some
> other kind of really weird relevance logic that is clearly inappropriate for
> the faithful formalization of mathematical reasoning.)
>
> We are going to carry on talking right past each other unless I enable my
> tenacious interlocutors to achieve a much clearer understanding of Core
> Logic than has been evident thus far in our exchange.
>
> Here are some important points about Core Logic (and/or its classicized
> extension, Classical Core Logic).
> (I'll make the points as though we are discussing constructive mathematics,
> and its formalizability in Core Logic. Completely analogous points would
> hold for classical mathematics, and its formalizability in Classical Core
> Logic.)
>
> 1. Core Logic, in its natural deduction formulation, has only introduction
> and elimination rules, *suitably formulated*. All elimination rules are in
> parallelized form, and in all applications of the elimination rules, their
> major premises stand proud, with no proof-work above them. There is no rule
> EFQ. Parallelization of the elimination rules, with the condition that MPEs
> stand proud, makes all proofs normal.
> 2. Core Logic, in its sequent calculus formulation, has only Left and Right
> logical rules, *suitably formulated*. The only structural rule is
> Reflexivity. So there is no rule of Cut, and there is no rule of Thinning.
> 3. Core natural deductions are isomorphic, in a rigorously definable sense,
> to the corresponding sequent proofs.
> 4. Just as Core natural deductions are in normal form, so too Core sequent
> proofs are cut-free and thinning-free.
> 5. Core Logic has enough transitivity of deduction to do everything that
> needs to be done. There is a computable binary operation [ , ] on core
> proofs such that: if P is a core proof of the sequent X:A, and P' is a core
> proof of the sequent A,Y:B, then [P,P'] is a core proof of X',Y':B or of
> X',Y':#, for some subsets X',Y' of X,Y respectively. More pithily: [P,P']
> proves a subsequent of X,Y:B.
> 6. [Confining ourselves now to the natural deduction formulation:] The
> introduction and elimination rules are altered in slight but very subtle
> ways from the familiar rules in the Gentzen-Prawitz tradition. The rules ->I
> and vE are liberalized in the important ways described in earlier postings.
> These liberalizations enable one to *directly and faithfully* formalize
> simple moves that mathematicians make in their deductive reasoning (such as
> 'closing off a case' within a proof by cases when they have shown that the
> case-assumption leads to absurdity; or inferring "if A then B" immediately
> upon refuting A).
> 7. Core Logic is complete: if the sequent X:A is valid, then there is a core
> proof of some subsequent of X:A.
> 8. Thus: If A is a logical truth, then Core Logic proves A; if X is not
> satisfiable, then Core Logic proves X':#, for some subset X' of X; and if X
> is satisfiable and X:A is valid then Core Logic proves X':A, for some subset
> X' of X.
>
> Core Logic does NOT 'allow EFQ in through the back door', or 'exploit EFQ in
> some tacit or hidden way'. That kind of criticism is completely
> ill-informed. For Core Logic satisfies a 'variable sharing' condition (or
> 'extralogical vocabulary sharing condition, at first order) that is more
> demanding than any that has been established, to date, for any competing
> relevance logic. This result can be found in
>
> ‘The Relevance of Premises to Conclusions of Core Proofs’ [pdf], Review of
> Symbolic Logic, 8, no. XXX, 2015, pp. XXX-XXX, DOI:
> http://dx.doi.org/10.1017/S1755020315000040
>
> Now, let us return to Harvey's allegation
>
> "... the significance of what you are saying for
> actual mathematical proofs is not at all apparent. The distinction you
> seem to be making does not seem to reflect in the way mathematicians
> write or think of proofs."
>
> Au contraire, it should (now, at least) be painfully apparent. What I am
> saying is that actual mathematical proofs can all be faithfully formalized
> in Core Logic, without any recourse to the irrelevance-inducing rule EFQ.
>
> And the distinction I am seeking to make, between a system of constructive
> *and relevant* reasoning like Core Logic, and the better-known system of
> constructive but permissibly *irrelevant* reasoning called Intuitionistic
> Logic, is being made precisely because (I maintain) the former system
> perfectly reflects the way [constructive] mathematicians write or think of
> proofs.
>
> Remember too that I said earlier that analogous points hold in the classical
> case:  the distinction I am seeking to make, between a system of
> non-constructive *and relevant* reasoning like Classical Core Logic, and the
> better-known system of non-constructive but permissibly *irrelevant*
> reasoning called Classical Logic, is being made precisely because (I
> maintain) the former system perfectly reflects the way [non-constructive]
> mathematicians write or think of proofs.
>
> The Core systems AT LAST capture the essence of mathematical reasoning,
> which, intuitively---and pacete Avron and Harvey---NEVER trades on
> irrelevancies. It is simply in error to think that we have to have the
> *rule* EFQ in order to formalize what might look like the occasional
> exploitation of 'anything follows from a contradiction'. Those apparent
> exploitations can ALWAYS be regimented by using the liberalized rules of ->I
> and vE mentioned earlier. So the Core systems are free of this truly ghastly
> rule EFQ, which should never have been put into the canon in the first
> place. I think the only reason why it was (by Gentzen) is that he was hung
> up on having conclusions of case-proofs in proofs-by-cases be *equiform*,
> and on having ->I formulated as the usual rule of conditional proof that did
> not accommodate, as a primitive move, concluding A->B as soon as one has
> refuted A.
>
> Neil Tennant