Any statement is either true or false. If we can prove that false is true, then ... | Hacker News

Hacker News new | past | comments | ask | show | jobs | submit

login

jstanley on March 25, 2015 | parent | context | favorite | on: Proving false in Coq using an implementation bug

Any statement is either true or false. If we can prove that false is true, then any statement is true.

EDIT: For example: 1+1=3. That's false. We've learnt that false=true, therefore 1+1=3 is true.

heinrich5991 on March 25, 2015 [–]

I don't think it's that easy. Not every statement is either true or false in Coq, you'd need to accept the law of excluded middle for that.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact