[FOM] Concerning EFQ and Cut

[Harvey Friedman]

So we have established that under the usual formalization of
mathematics, there is plenty of uses of EFQ. I think the same applies
to CUT, except here we haven't similarly fixed the ideas to the point
of me giving such vivid examples (suggested originally in this FOM
thread by Avron).

I presented the obvious mathematical proof that "emptyset containedin
A" in normal publishable mathematical form. I gave two versions, in
accordance with how real mathematical proofs work. For convenience I
repeat here: (I corrected typos and put in "y be arbitrary").

THEOREM 1. {x: absurdity} containedin A.

THEOREM 2. emptyset containedin A.

Proof: of Theorem 1: Let A be a given set and y be arbitrary. It
suffices to show that y in {x: absurdity} implies y in A. Suppose y in
{x: absurdity}. Then absurdity. Hence y in A. QED

Proof of Theorem 2: Let A be a given set and y be arbitrary. It
suffices to show that y in emptyset implies y in A. Suppose y in
emptyset. Since not(y in emptyset), we have y in A. QED

Neil has responded with some detailed account in technical proof
theory language about how "you can avoid use of EFQ". This is not the
kind of response that furthers a productive discussion. What we need
to see is some completely clear alternative proof to Theorem 1 or 2 in
normal publishable informal and then semiformal ordinary mathematical
writing.

Then we can compare the two to see just what kind of claim "you can
eliminate EFQ" really amounts to.

Let me anticipate how the discussion can continue. This is rather optimistic.

1. Neil presents such an alternative proof in normal publishable form.
It will likely be considerably more complicated than what I wrote
above. I will claim that it is not publishable, and that the style is
not publishable - in the usual Mathematics Journals. A referee would
ask it to be rewritten more or less in the standard form that I
presented above.

2. Neil will nevertheless claim that it is better or more honest and
perhaps claim that mathematicians should rewrite their proofs like
this (to be presented).

3. Meanwhile somebody, maybe me, maybe Avron, will spot an arguably
buried form of EFQ lurking in even Neil's normal mathematical
discourse proof of Theorems 1,2.

4. There will be an altered system at least vaguely formulated, and
THEN the discussion turns productive. Namely, what can you or can't
you prove on the basis of a new system coming out of 3.

Under this optimistic scenario we will have the beginnings of a
possibly interesting subject where one considers robust restrictions
of the rules of classical logic, and of the rules of intuitionistic
logic, and proves independence results. The key word here is "robust".

I will stop speculating and wait and see.

Harvey Friedman

NEIL TENNANT

We take the set term-forming operator as a primitive. So {x|Fx} is a
well-formed singular term.
So we have to work in a free logic, designed to deal with non-denoting
singular terms.
We express "x is a member of y" by "x in y" in ascii.
Ex is our existential quantifier in ascii.
Ax is our universal quantifier in ascii.
We abbreviate Ex(x=t) to E!t.
The absurdity symbol is #. It occurs only as a punctuation marker in
proofs, never as a subformula of any formula.

The Axiom of Existence of Empty Set is the zero-premise rule

           ________
           E!{x|~x=x}

The Rule of Reflexivity of Identity in free logic is

           E!t
           ___
           t=t

Core Logic has as a primitive rule that one can prove a conditional by
refuting its antecedent. This forms part of the rule of
->Introduction. Note the absence of any application of EFQ:

On Tue, Sep 1, 2015 at 11:32 AM, Tennant, Neil <tennant.9 at osu.edu> wrote:
> Towards the end of his posting with this thread-subject, and because of his
> apparently continuing misgivings about Core Logic, Harvey writes
>
> "I think another issue is that of cut. ...".
>
> In order not to have to rehearse the Core Logician's answer to any question
> or objection Harvey might raise in connection with how the Core Logician
> formalizes mathematical reasoning without making any use of the cut rule,
> may I please direct the reader to the following earlier message of mine?
>
> http://www.cs.nyu.edu/pipermail/fom/2013-August/017546.html
>
> The latter message ended with "Exeunt ad tavernam"; apparently the resulting
> hangover has been of exactly two years' duration.  :-)
>
> Neil Tennant