User:Boris Tsirelson/Sandbox1: Difference between revisions

Revision as of 14:42, 12 June 2010

wp:Strict_conditional

@@ Line 1: / Line 1: @@
-==Decidable or undecidable==
+[http://en.wikipedia.org/wiki/Strict_conditional wp:Strict_conditional]
-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,
-*there is no guarantee that it will be decided in the first 10<sup>6</sup> steps of the algorithm, nor in the first 10<sup>1000</sup> steps, nor in any time estimated beforehand;
-*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.
-Independent statements appear naturally in multivalent theories. For example, in linear algebra the statement "three vectors cannot be linearly independent" is neither provable nor disprovable, since the dimension of a linear space may be 2 or 3 (or anything else).
-What about independent statements in univalent theories? Seemingly, these should not exist. For example, the plane Euclidean geometry should prove all geometric statements that hold on the Euclidean plane, and only such statements. Similarly, arithmetics of natural numbers should prove all true arithmetical statements about natural numbers, and only these. Unexpectedly, the situation is far more complicated than these naive ideas.
-Imagine a theory able to describe the whole discrete mathematics (the set theory?) or, at least, arbitrary algorithmic computations, in other words, formal machines (like computers, but with unlimited resources). Assume that the theorems include all true statements about these machines, and no wrong statements about them. Then a formal machine can use this theory as a "crystal ball", — for predicting the future of any formal machine. In particular, for deciding, whether a given machine will eventually halt, or will run forever (so-called halting problem). To this end it runs the theorem-generating algorithm until either the statement "such machine eventually halts" or its negation appears among the theorems.
-In order to predict the future of a formal machine ''Y'', a formal machine ''X'' needs the code of ''Y''. It does not mean that the code of ''Y'' must be inscribed into (and therefore be shorter than) the code of ''X''. Instead, ''X'' can generate the code of ''Y''. This way, a single machine ''X'' can predict the future of infinitely many machines ''Y'', and moreover, of all possible machines ''Y'', generating their codes in an endless loop.
-Can ''X'' predict its own future? It may seem that the affirmative answer is ensured by the argument above. However, how can ''X'' know, which ''Y'' is identical to ''X''? In other words, how can ''X'' know (it means, be able to generate) its own code?
-It is a well-known and nontrivial fact that some programs, so-called quine programs, can generate their own texts.

User:Boris Tsirelson/Sandbox1: Difference between revisions

Revision as of 14:42, 12 June 2010

Navigation menu

Search