4 ms·
I know of several computer verified proofs of the incompleteness theorem. See entry 6 of https://www.cs.ru.nl/~freek/100/ https://www.cs.ru.nl/~freek/100/ for a
by deadbeef57 5y ago
I know of several computer verified proofs of the incompleteness theorem. See entry 6 of https://www.cs.ru.nl/~freek/100/ https://www.cs.ru.nl/~freek/100/ for a small catalogue.
How does this relate to your objection? Are there bugs in the verifiers? Or did people verify the wrong theorem statement?
- ProfHewitt 5y agoProofs forgot to include order of proposition in its Gödel number.
- deadbeef57 5y agoSo you say that the computer verified proofs of the incompleteness theorem of verifying the wrong theorem? Because there can't be bugs in a computer verified proof. (Of course there can theoretically be bugs in a computer verified proof. If there are bugs in the verifier. But if 4 independent proof assistants verify a proof of a theorem, this is extremely unlikely.)
- ProfHewitt 5y agoA proof is only as good as definitions and axioms used in the proof. All of the computer-verified proofs of existence of [Gödel 1931] proposition I'mUnprovable left out the order of proposition in its Gödel number :-(