3 ms·

Uncomputable or unsolvable?

• pygy_ 11y ago
  Undecidable. https://en.wikipedia.org/wiki/Undecidable_problem https://en.wikipedia.org/wiki/Undecidable_problem See here for a concrete example of a similar problem (props to adrianN for the link in the first place): https://en.wikipedia.org/wiki/Wang_tile#Domino_problem https://en.wikipedia.org/wiki/Wang_tile#Domino_problem
• jordigh 11y ago
  These two are roughly the same thing. Formally, a proof is just a computation within an axiomatic system. A computation is just transforming one expression into another according to a set of rules. Whether this transformed expression is an algebraic or a logical formula is not a huge difference. In terms that may be more familiar to programmers, lisp's homoiconicity of data and code corresponds roughly to how Gödel was able to express logical formulae as arithmetic statements via Gödel numbering. Once you are able to encode logical formulae as natural numbers, you can then use laws of arithmetic (e.g. Peano's axioms) to compute/prove other statements/numbers.