[FOM] The unbearable ghastliness of EFQ, and sundry other matters arising from Harvey's last post

[Harvey Friedman]

On Thu, Sep 3, 2015 at 8:45 AM, Tennant, Neil <tennant.9 at osu.edu> wrote:
> Harvey says
>
> "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. "
>
> OK, try to find such a theorem. You won't. For there is the counterexample
> that "empty set is contained in A" is provable in Core Logic from the axioms
> of set theory that one would normally use, without Core Logic in any way
> "having the idea that a contradiction yields everything".

I'm talking about such a theorem in the setting of pure logic like you
are working in.

The only proof you have offered of this "empty set contained in A" in
ordinary mathematical language read virtually identically to the usual
proof with explosion (EFQ), and so I still haven't seen any proof of
"empty set contained in A" that isn't obviously based on the idea that
a contradiction yields everything. I said that if I see such a thing,
I will revisit this whole matter.

> No one is suggesting that mathematicians should 'change the way they write
> proofs'. Rather, I am simply pointing out that when logicians approach the
> task of rendering in excruciatingly minute formal detail, in proofs within
> their formal systems, what the mathematicians have accomplished, they can do
> so very naturally indeed in a system that allows no applications at all of
> EFQ.

The obvious way to formalize the usual proofs such as "empty set is
contained in A" explicitly use EFQ. Furthermore, the proof assistant
people I would imagine have it freely available and it gets widely
used. I think you should check that out with that community.
>
> "I wonder if Neil has connected with them [i.e. 'the MIZAR people'] about
> just this [i.e., EFQ]?"

> "c times x
>
> for integers c,x, does really depend on what c,x is. They are both
> relevant --- EXCEPT when c IS 0. This is very much like EFQ to a
> working mathematician."

I changed my original typo to IS.

> No, it is not. Consider:
>
> "P->Q
>
> for sentences P,Q, does really depend on what P,Q is. They are both relevant
> --- EXCEPT when P is false or Q is true. This is not at all like EFQ to a
> working mathematician."

My point was that mathematicians are used to expressions where
sometimes part of the expression is irrelevant to the value of the
entire expression. P arrows Q, for certain P, makes the truth value of
Q irrelevant to the truth value of the entire expression. For certain
P, the truth value of Q is highly relevant. Same thing with cx. When c
= 0, what x is is not relevant, and when c is nonzero, what x is is
highly relevant.
>
> By the way, it ought to be pointed out that all this praise for 'working
> mathematicians' does rather idolize them.

This is totally irrelevant. The point is that we are talking about
f.o.m. and the investigation into the nature of actual mathematical
proof. I know that there are derived subjects like: idealized formal
systems for mathematical proof, and detailed properties of such. It is
this latter subject that you appear to be most interested in. Not so
much the former.

> "A or (A implies B)
> (A and not(A)) implies B
>
> are "Ghastly"? "
>
> I am happy to reassure Harvey that neither of these is ghastly.

But it is obvious that, from the point of view of mathematical proofs,
there is NO DIFFERENCE between these two and EFQ. That "or" is pretty
serious. And for reasons that I don't you understand, you call EFQ
"ghastly" but not the above?? Give me a proof in ordinary mathematical
language of the above two and compare it with my so called "ghastly"
proof of empty set containedin A.

> "You cannot prove any of
>
> 1+...+1 = 0 implies 1 = 0
>
> for more than one plus sign."

I put this sentence in in the wrong spot in my posting. This was ONLY
under the part of my posting concerned with ARITHMETIC WIThOUT
NEGATION. It has nothing to do with what you were talking about. Sorry
for the confusion.

I am a bit excited about arithmetic without negation, and then higher
systems without negation. It appears, superficially, that deep new
phenomena are probably going to appear when I go beyond PA without
negation based on 0,S,+,dot, to PA without negation based on
0,S,+,dot,exponentiation. And then there is adding full primitive
recursion, again all without negation.
>
> "On the "cut" side of things, I think Neil is offering up a system with
> no cut."
>
Neil talks about not needing to explicitly have a cut rule out in the
open. But since mathematicians are cutting and cutting and cutting,
what is to be gained? Again, this seems like a formal matter, and not
related to actual mathematical proof.

It would be very interesting to have a lot of genuine examples where
the issue of cut free is modified to robustly deal with the phenomena
of having all proofs of some basic elementary theorems, even in PA,
provably requiring the use of induction applied to formulas that are
far removed from the statement being proved. I'm talking for the
moment about PA with negation as usual. For example, it would appear
that the theorem

no solutions to 2n^2 = m^2

cannot be proved in PA, even liberal PA (using familiar functions way
beyond the list 0,S,+,dot), without resorting to axioms from PA that
are way way way beyond the statement of this wonderful theorem above.

Incidentally, as is well known, in PANF (PA negation free), 1 = 0
implies al formulas whatsoever. One immediate question is this. Which
sentences imply all formulas whatsoever in PANF? I mentioned last time
that PANF is decidable and you can fantastically prove that PANF does
not prove 1 = 0.

Harvey