User:Boris Tsirelson/Sandbox1

Decidable or undecidable

Theorems of a theory are, by definition, statements that follow from the given axioms according to the given rules (called by different authors inference rules, derivation rules, deduction rules, transformation rules). Note that "a theorem" does not mean "a motivated theorem", "an important theorem" etc., not even "an already discovered theorem". All theorems are just an indiscriminate stream of logical consequences of the axioms. It is impossible to list all theorems, since they are infinitely many. However, an endless algorithmic process can generate theorems, only theorems, and all theorems in the sense that every theorem will be generated, sooner or later. (In more technical words: the set of all theorems is recursively enumerable.)

An open question (in a mathematical theory) is a statement neither proved nor disproved. It is possible (in principle, not necessarily in practice) to run the theorem-generating algorithm waiting for one of two events: either the given statement appears to be a theorem, or its negation does; in both cases the (formerly) open question is decided. However,

• (a) there is no guarantee that it will be decided in the first 10⁶ steps of the algorithm, nor in the first 10¹⁰⁰⁰ steps, nor in any time estimated beforehand;
• (b) worse, there is no guarantee that it will be decided at all.

A statement is called independent (in other words, undecidable) in the given theory, if it is not a theorem, but also its negation is not a theorem.