Is it possible to 'prove' `False`

?

I was trying:

```
Goal
False.
Proof.
...
```

only if you find the right bugs

Ah.. :sweat_smile: okay.

Julin S has marked this topic as resolved.

Because of the elimination principle of False, if you can prove it then you will be able to also prove any other sentence. This would be a disaster because there would not be any interesting distinction between sentences. All sentences would be provable, there is a proof that 2 + 3 = 5 but also a proof that 2 + 3 = 9 and so on. So we hope not.

You probably want to use Falso for this https://inutile.club/estatis/falso/

Last updated: Jun 23 2024 at 23:01 UTC