[FOM] Concerning EFQ and Cut

[Harvey Friedman]

Arnon and Levy may have other difficulties with what you are saying.
But for me, it seems like you have rearranged the symbols in some
particular way you want to formalize actual mathematics, and claim
that under this rearrangement of the symbols you can prove the same
logical truths. But then 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.

No matter how you look at it, mathematicians freely use and are used
to being comfortable with the basic idea that you can get anything
from a contradiction. Whether or not you want to call this EFQ seems
to depend on exactly how a certain kind of proof theorist wants to
package or display it.

In short, I do not see just what foundational or philosophical issue
is being addressed here. It certainly appears that there is no
mathematical issue being addressed.

On the other hand, removing negation entirely is a very major move
with lots of ROBUST consequences. I am planning to move what I wrote
on it to my numbered postings when I get a little more material. My
casual impression is that there is a substantial subject there when
you throw away negation, and then add lots of interesting axioms that
are iconic theorems of elementary and advanced number theory, stated
without negation. Sometimes like Euler's 4 square theorem, they can be
very nicely stated without negation. Other times it may be kind of
ugly with "arrows 1 = 0". In any case, you add iconic theorems and
then see which other iconic theorems follow or don't follow. I am
guessing and kind of hoping that what results is new kinds of heavy
algebraic questions of a sort that nobody considered because they
aren't that compelling as pure algebra, but now they are important for
unprovability results of a new(?) kind. I forgot to mention that what
I wrote last time about negation free arithmetic is proved by
algebraic methods, an idea I found in the joint paper "Whither
Relevant Arithmetic?" (the core mathematical part, with Meyer).

By the way, perhaps if negation is kept, there is an interesting way
to cut down the logic so that you get a smaller set of provable
formulas of arithmetic, with interesting independence results. Only
here, one has to be careful identifying something that is robust
mathematically. That it is easy for a mathematician to sense and feel
the distinction. Of course in the case of the removal of negation,
this criteria seems to be reasonably met.

Another thought is just what happens if we only allow intuitionistic
reasoning AND don't allow negation. E.g., A or (A arrows B) is not
accepted. Incidentally, this can be construed as a disguised form of
EFQ.

Actually now I see a lot of stuff even beyond this that needs to be
moved to my numbered postings after I absorb some more feedback. I
have the feeling that there is some relevant stuff already done that I
have either forgotten and never knew.

Harvey Friedman

On Wed, Sep 2, 2015 at 2:32 PM, Tennant, Neil <tennant.9 at osu.edu> wrote:
> Harvey judges my earlier informal proof to be too long! He offers the
> following revision. It is, in effect, a subproof of my own informal proof.
> It results by deleting from the latter its final step of explicit universal
> introduction, and its appeal to the definition of 'containedin'. That's just
> fine by me. Let those things be tacitly understood. So here is the informal
> prooflet we both agree on (Harvey's rendition):
>
>     THEOREM. {x|~x=x} containedin A.
>
>     Proof
> *
> : Let b be arbitrary. Suppose b in {x|~x=x}. Then ~b=b. But b=b.
>     Contradiction. So, if b in {x|~x=x}, then b in A. QED
>
> Harvey goes on to say
>
>     This is obviously the same proof that I gave before (twice).
>
> That's fine by me too. So now we both know and agree on what would need to
> be formalized. Schematically, what we have agreed on is a passage of
> reasoning like this:
>
>       ____________(1)
>        b in {x|~x=x}
>        ____________    _____
>            ~b=b              b=b
>            __________________
>
>                  Contradiction
>         ________________________(1)
>
>          if b in {x|~x=x}, then b in A
>
>
> Thank you, Harvey. That is a Core proof.
>
> Neil Tennant