[FOM] Concerning EFQ and Cut

[Harvey Friedman]

On Tue, Sep 1, 2015 at 4:09 PM, Tennant, Neil <tennant.9 at osu.edu> wrote:
> Here is an informal proof of the theorem Harvey wishes to see proved. It
> does not use EFQ.
>
> 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. But b was arbitrary. So
> for all y, if y in {x|~x=x}, then y in A. Hence by definition {x|~x=x}
> containedin A.

The referee would say: you were done after the sentence starting with "So."
Revised as follows:

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

This is obviously the same proof that I gave before (twice).
​From the working mathematicians point of view, they all use EFQ. ​
What I wrote was:

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


​My earlier proofs use EFQ and your Proof* looks identical. In order to
make a distinction between the two, it looks like you have to use some
particular way of formalizing proofs that may not faithfully reflect how
mathematical proofs operate in the real world.

Instead of simply writing "b in A", you have repeated the original
implication. But how do you get this implication? The same idea that
contradictions yield anything. I doubt if there is a working mathematician
on the planet who has any idea what distinction you are drawing between
your  Proof* ​and my proof(s).

It would appear that the notion "not using EFQ" is not sufficiently robust
for the study of actual mathematical proofs. It appears to be too sensitive
to the exact way one chooses to formalize actual mathematical proofs.

On the other hand, the notion "not using the law of excluded middle", after
serious investigations, has turned out to be sufficiently robust for a
tremendously important study of actual mathematical proofs. It appears not
be sensitive to the exact way one chooses to formalize actual mathematical
proofs.

Let me repeat my earlier question/challenge which I think is possible to
meant, leading to a productive direction.

QUESTION. Is there a restriction on the rules of logic, or intuitionistic
logic, which has the property that
i. We know that the restriction is a real restriction in that it reduces
the class of provable validness, or intuitionistic validates.
ii. A very large amount, but perhaps not all, of mathematics, or
intuitionistic mathematics, can live within that restriction.
iii. Even better, if the restriction is fully reflected in a way that is
apparent to the working mathematician.

Intuitionistic logic does this over classical logic, and provides a very
deep and interesting development in f.o.m.

NOW I do see something that makes sense along these lines. WHAT ABOUT the
issue of NEGATION FREE MATHEMATICS?

I don't quite see how to do this for set theory, but for arithmetic I think
it works well!

PANF = PA negation free. 0,S,+,dot,=,and,or,if then,iff,formal, therapists,
variables. No negation.

The usual axioms and rules of logic without negation. The usual axioms for
0,S,+,dot, except we don't have Sx not= 0, since we don't have negation!
Induction with respect to all formulas (without negation).

Now let's take a great theorem whose formulation does not use negation.

EULER. Every n is the sum of four squares.

THEOREM. Euler's theorem cannot be proved in PANF.

In PANF, S0 = 0 does serve as a substitute for an EFQ ridden negation:

THEOREM. Let A be a formula in the language of PANF. S0 = 0 implies A is
provable.

QUESTION. Which sentences serve similarly as an EFQ ridden negation in PANF?

Using "arrows 1 = 0", we can nicely formalize a lot of important number
theoretic statements.

THEOREM. For no exponent, is FLT provable in PANF.

QUESTION. What can we say about extensions of PANF to make the system much
more effective in proving fundamental statements in number theory?

​Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150901/1e154788/attachment.html>