Principle of Explosion

[Arnon Avron]

This is the example  I have always given to students of a simple case in which
it is clear that the mathematician's implication is indeed based on the truth-function
for -> that I teach them.

It is also true that the two theorems cannot be proved without using some form of EFQ
(like the disjunctive syllogism).

Having said that,  I should add that one can give  proofs of e.g.  Theorem
in which the use of EFQ is rather hidden. For example: the intersection
of A and B is contained in both A and B. In particular: the intersection of A and the
emptyset is contained in the emptyset. Hence this intersection has no elements,
and so is emptyset. but the intersection of A and  emptyset is contained
in A too. Hence emptyset is contained in A.

Arnon


________________________________
From: FOM <fom-bounces at cs.nyu.edu> on behalf of Harvey Friedman <hmflogic at gmail.com>
Sent: Thursday, May 19, 2022 8:12 AM
To: Foundations of Mathematics <fom at cs.nyu.edu>
Subject: Principle of Explosion

I wrote https://cs.nyu.edu/pipermail/fom/2022-May/023297.html

Wiki calls this the principle of explosion and I will go with that rather than EFQ. EFQ is being discussed by Arnon and Tennant on FOM.

This is NOT the law of excluded middle or any of its inferential variants.

I had something further to say about this.

THEOREM. The emptyset is contained in every set.

Proof: Let A be any set. To show emptyset containedin A, we need to show the following:

if x is in emptyset then x lies in A

Assume x is in emptyset. Then absurdity. Hence x lies in A. QED

This is the way mathematicians normally prove the Theorem. THis proof uses the principle of explosion.

The use of explosion occurs also in the proof of this theorem that does not explicitly mention the empty set.

THEOREM'. There is one and only one set that is included in every set.

How does one prove Theorem and Theorem' without use of explosion?

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