According to the Curry-Howard correspondence, there is an isomorphism between programs (algortihms) and proofs.
algorithms are proofs. nothing shocking about that i guess. algorithms prove how to solving a problem.
Topic: Understanding Godel Incompleteness on Bitcoin (Read 449 times)
According to the Curry-Howard correspondence, there is an isomorphism between programs (algortihms) and proofs.
algorithms are proofs. nothing shocking about that i guess. algorithms prove how to solving a problem.
One example of how Bitcoin runs into this issue is the fact that a legacy transaction's signature is part of the transaction, so it must be explicitly excluded from the signature's calculation.
Gödel's incompleteness theorems concern "formal axiomatic system containing basic arithmetic" to quote Wikipedia. POW is an algorithm not a formal axiomatic system so theorems do not apply.
According to the Curry-Howard correspondence, there is an isomorphism between programs (algortihms) and proofs.
So the Gödel's incompleteness discoveries should be extendable to algortihms.
Interesting necro
I guess Gödel's incompleteness theorem being applicable to algorithms is more or less reflected in the halting problem? Doesn't seem to be really relevant for PoW though. Both Gödel's incompleteness theorem and the halting problem require a minimum of complexity to be present which you don't have in Bitcoin's PoW algorithm (or even Bitcoin script).
Gödel's incompleteness theorems concern "formal axiomatic system containing basic arithmetic" to quote Wikipedia. POW is an algorithm not a formal axiomatic system so theorems do not apply.
According to the Curry-Howard correspondence, there is an isomorphism between programs (algortihms) and proofs.
So the Gödel's incompleteness discoveries should be extendable to algortihms.
Gödel's incompleteness theorems concern "formal axiomatic system containing basic arithmetic" to quote Wikipedia. POW is an algorithm not a formal axiomatic system so theorems do not apply.
Consider Gödel's incompleteness theorems (specifically the second one)
"For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, if T includes a statement of its own consistency then T is inconsistent."
Gödel's second incompleteness theorem proves that your theory, which assumes math is valid (aka "including basic arithmetical truths") and assumes itself to also be true, is inherently inconsistent. Math has been proven to be incomplete.
"any consistent effective formal system that includes enough of the theory of the natural numbers is incomplete: there are true statements expressible in its language that are unprovable within the system" (Gödel's first incompleteness theorem). It does, however, mean that it's impossible to prove mathematicians have nothing left to prove, so maybe its good for job security for them.
What about Bitcoin Proof Of Work Algorithm and Other Consensus rules
Thanks
"For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, if T includes a statement of its own consistency then T is inconsistent."
Gödel's second incompleteness theorem proves that your theory, which assumes math is valid (aka "including basic arithmetical truths") and assumes itself to also be true, is inherently inconsistent. Math has been proven to be incomplete.
"any consistent effective formal system that includes enough of the theory of the natural numbers is incomplete: there are true statements expressible in its language that are unprovable within the system" (Gödel's first incompleteness theorem). It does, however, mean that it's impossible to prove mathematicians have nothing left to prove, so maybe its good for job security for them.
What about Bitcoin Proof Of Work Algorithm and Other Consensus rules
Thanks
Jump to: