Explosion Use in Math

[Lawrence Paulson]

> On 20 May 2022, at 02:41, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> 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? 

In Isabelle/HOL, the empty set (a typed set in higher-order logic) is DEFINED as {x | False} and assuming x∈∅ would indeed trigger the principle of explosion.

> 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?

Automatic proof methods never use cuts because such steps require creativity. On the other hand, an explicit formal proof can capture any mathematical argument within the scope of the formal system.

Larry