[FOM] Use of ex falso quodlibet (EFQ)

[Harvey Friedman]

I have earlier expressed my skepticism that under the usual way mathematics
is formalized, EFQ is substantially used, especially in arguments by cases
- in such situations, often many cases are entirely vacuous.

Avron has given a more focused example which of course is much better.

THEOREM. For any set A, emptyset is a subset of A.

In the usual formalization of mathematics, the proof goes like this. First
of all one either formalizes this as

THEOREM 1. {x: absurdity} containedin A.

with absurdity sign. This would be common in some automated proof systems.
Or there would be a constant symbol introduced, emptyset, by instantiation,
with the condition

not(x in emptyset).

And then the formalization would read

THEOREM 2. emptyset containedin A.

Proof: of Theorem 1: Let A be a given set. 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. It suffices to show that y in
emptyset implies y in A. Suppose y in emptiest. Since not(y in emptiest),
we have y in A. QED

Now these proofs are still are the semiformal level, as the use of
mathematical definitions, and definitions by instantiation, etc., are not
yet formal. But the basic structure is clear.

So when we get to the ACTUAL mathematics, we see that EFQ is used, and used
without any qualms here. I have never heard of any working mathematician
who has any problems with this, I have never heard of any mathematician who
wants to eliminate this. I have heard of mathematicians interested in
eliminating various uses of the law of excluded middle - constructivists,
and mathematicians with constructive instincts who sense a problem that
they don't know how to formulate with regard to the law of excluded middle
in various contexts.

So there can be no doubt that there is plenty of EFQ all through
mathematics, and that mathematicians are quite comfortable with it, and
have no interest in its removal.

So now the issue between me, Avron, and Tennant focuses on these issues:

1. Maybe the usual formalization of mathematics, in which there is plenty
of EFQ, is not the appropriate formalization of mathematics. Instead, maybe
the usual formalization of mathematics needs to be replaced by another
formalization of mathematics. Why this is so, needs to be argued.

2. Maybe the usual formalization of mathematics is fully appropriate, but
mathematicians SHOULD be interested in the removal of EFQ. This begs the
question as to whether, under the usual formalization of mathematics, one
can remove EFQ. Of course, you can remove anything whatsoever and replace
it by something else, even to the point of changing a comma or period. So
the issue is whether there is a coherent systematic way of avoiding EFQ.
And then whether it is compelling in some sense. And then whether or what
there is to be gained by avoiding EFQ.

3. In particular, if avoidance of EFQ is proposed, one has to defend
against the idea that EFQ is simply buried in something that is being
allowed.

ARNON AVRON
On Mon, Aug 31, 2015 at 02:20:33AM +0000, Tennant, Neil wrote:

> In Core Logic, *there is no rule of EFQ*. That's because mathematicians
NEVER (NEED TO) USE IT!

I have always thought that  mathematicians (NEED TO) USE  it, e.g.,
when they claim that the empty set is a subset of any other set.
Do you have another logical explanation of this claim
on the basis of the standard definitions of the empty set
and the subset relation?

NEIL TENNANT
http://www.cs.nyu.edu/pipermail/fom/2015-August/018968.html

The Core logician has a reassuring answer to this question (and all others
> like it).
> I described in an earlier posting how Core Logic liberalizes the rule of
> v-Elimination, so as to avoid the need for EFQ within either of the case
> proofs. There is only one other rule that needs to be liberalized in a
> similar fashion, and this is the rule of ->Introduction (a.k.a. Conditional
> Proof). .....
>


> Let me repeat: mathematicians (whether constructivists or
> non-constructivists) never need to use EFQ when they get down to detailed
> formalizations of their reasoning. Core Logic (or its classicized
> extension) provides natural deductions (or sequent proofs) whose structures
> are absolutely homologous to those of the informal proofs being formalized.
> Logicians have simply been mistaken in thinking that the rule EFQ is needed
> for the faithful formalization of the deductive reasoning involved in
> either mathematics or the empirical testing of scientific theories.
> Another nice feature of Core Logic is that it is formulated in such a way
> that any natural deduction of X:A is structurally isomorphic to the
> corresponding sequent proof of X:A. The sequent system has only
> reflexivity, A:A, as a structural rule. It has no rule of thinning, and no
> rule of cut. And it has, besides reflexivity (which allows proofs to get
> started!), only the Left and Right logical rules for the connectives and
> quantifiers, *suitably formulated*. That qualification is very important,
> since it covers all the innovations by means of which Core Logic departs
> from the standard Gentzen-Prawitz systems of intuitionistic and classical
> logic.


​We have seen that under the natural straightforward formalization of
​mathematics, both by hand and in conjunction with machine, the natural
proof of emptyset containedin A uses EFQ. The case needs to be made for
departing from the usual.

"Logicians have simply been mistaken in thinking that the rule EFQ is
needed for the faithful formalization of the deductive reasoning involved
in either mathematics or the empirical testing of scientific theories."

I have no doubt that from my respect for your modus operandi, you can - and
probably did - create an alternative "faithful formalization ..." in which
EFQ does not appear. That is not the issue here, as I have been saying.

I think another issue is that of cut. The problem is that cut has different
shades of meaning depending upon just how you formalize mathematics. I
think that under the most natural formalization of mathematics both by hand
and in conjunction with machine, here too there is plenty of uses of cut.
(I haven't thought about this for a while). One thing is clear. A
fundamental idea about cut is from pure logic situations, where the idea is
that in order to prove something, you just need to use sub formulas
appropriate defined. It is certainly clear that mathematicians are always
proving theorems where the concepts used are nowhere to be found in the
statement being proved. However, when people argue about cut being used or
not, there is the issue of whether one counts the instances of the ZFC
axioms that are being used in the purely logical part of the proof as
proper axioms, and then one can start to say that there is no cut being
used. So it is important to fix an idea as to just what kind of
formalization of mathematics one is talking about, and then - why

All of this comes back to my original comment some time ago. I am not aware
of any distinction between different kinds of *logical* moves in
mathematical proofs (as opposed to strength of axioms, lengths of proofs),,
that has any robust foundational traction, other than that of constructive
proof. And as I said, I would be thrilled to see such a thing, and would
want to investigate it immediately.

Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150901/9949abc9/attachment-0001.html>