Explosion Use in Math

[Harvey Friedman]

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

I asked how these two commonly proved and commonly taught and commonly used
theorems are proved without the principle of explosion:

The emptyset is included in every set.
There is one and only one set that is included in every set.

Of course, I have taught both of these theorems with the obvious use of
explosion. I.e., let x be in emptyset. Want to show x is in A. Clearly x in
A by explosion.

I'd like to bring Larry Paulson into the conversation if he is interested.

Is there any natural way or way you have seen that these two theorems or
theorems of this shape would be proved in proof assistants?

Also don't you see quite often in proof assistant use that A is proved by
cases on B and not B, where B is not any kind of subformula of A? I.e.,
serious cuts?

Again is there any natural way or way you have seen that this kind of proof
is avoided, where one proves A sticking to subformulas of A in any
reasonable sense?

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