Stream: Coq users

Topic: ✔ Proof of False


view this post on Zulip Julin S (May 14 2022 at 15:24):

Is it possible to 'prove' False?

I was trying:

Goal
  False.
Proof.
 ...

view this post on Zulip Gaëtan Gilbert (May 14 2022 at 15:25):

only if you find the right bugs

view this post on Zulip Julin S (May 14 2022 at 15:28):

Ah.. :sweat_smile: okay.

view this post on Zulip Notification Bot (May 14 2022 at 15:28):

Julin S has marked this topic as resolved.

view this post on Zulip 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.

view this post on Zulip Li-yao (May 14 2022 at 16:52):

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


Last updated: Mar 28 2024 at 12:01 UTC