Stream: Coq users

Topic: ✔ Proof of False

Julin S (May 14 2022 at 15:24):

Is it possible to 'prove' False?

I was trying:

Goal
  False.
Proof.
 ...

Gaëtan Gilbert (May 14 2022 at 15:25):

only if you find the right bugs

Julin S (May 14 2022 at 15:28):

Ah.. :sweat_smile: okay.

Notification Bot (May 14 2022 at 15:28):

Julin S has marked this topic as resolved.

Patrick Nicodemus (May 14 2022 at 15:28):

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.

Li-yao (May 14 2022 at 16:52):

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

Last updated: Sep 23 2023 at 13:01 UTC