Let T be a Turing machine which, when started on an infinite blank tape extending to the left and to the right, is programmed to print out in some recursively enumerable order, all the theorems of ZFC (one after another) on the squares of the tape. It is also programmed to halt when and only when (if ever) it prints a theorem that is the negation of a theorem which it has already printed. Does anyone know of any estimates that have been made of the number of states and the number of symbols which would be sufficient for the machine T to have available in order to be able to accomplish this task-i.e. to test the consistency of ZFC?
$\begingroup$
$\endgroup$
3
asked Feb 7, 2011 at 18:31
-
$\begingroup$ If you were allowed a finite starting configuration on the tape, you could use a universal Turing machine and the appropriate program. You could then run an Internet contest to see who could come up with the shortest binary program to feed to the machine that accomplishes what you wanted. Gerhard "Ask Me About System Design" Paseman, 2011.02.07 $\endgroup$– Gerhard PasemanCommented Feb 7, 2011 at 21:19
-
$\begingroup$ In fact, the TM can be set up so that the first thing it does is print the program on the blank tape, then transfer control to the UTM. So Garabed's case includes Gerhard's. $\endgroup$– drbobmeisterCommented Feb 8, 2011 at 3:46
-
$\begingroup$ Thanks for your comments and suggestions. I amsure that the actual program. I am sure that the actual program for T, if one thinks of it as a sequence of ordered quintuples, will be tremendously long. I am really interested in an upper bound on the length of this sequence-if such a bound has ever been worked out. Perhaps the bound is too large to ever be worked out. I am not sure what effect (if any) the use of a Universal Turing machine would have on the size of this upper bound. $\endgroup$– Garabed GulbenkianCommented Feb 9, 2011 at 15:51
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
The Turing Machine you describe here can actually be constructed (from a practical standpoint also), but it would be tedious and not of much practical use.
First note that the finite set of symbols $\{ \in, \forall, \exists, x, \prime, \land, \lor, \lnot, \rightarrow, \leftrightarrow \}$ would be more than sufficient to represent all statements expressible in the language of set theory (prime used to differentiate the countably infinite set of variables: $x, x^{\prime}, x^{\prime\prime},\ldots$). We can have the scrap work occur to the left of the place where we list out all of our ZFC theorems. The (highly inefficient) process can be described as follows:
(1) Copy the tape counter, which can represent $n$ by $n$ successive primes written from right to left.
(2) Run a Turing Machine that on an input of $n$ primes, writes the first $n$ ZFC axioms (separated by spaces only working left on the tape) according to some recursive (computable) numbering.
(3) Run a Turing Machine that on an input of $n$ formulas, applies the first $n$ rules of inference in first-order logic (in the sense that there are an infinite number of substitution rules, each applying a specific change of variable) on each of the formulas already on the working part of the tape and writes them all to the left.
(4) Iterate through each formula on the left, determining whether it's the same as one already in your actual list or a negation of one. If not, add the formula to your list. If it's a negation of one, add the formula, reset your pointer to the beginning of the actual list, and HALT.
(5) Add a prime to the original counter, reset the pointer to the beginning of the prime list, and go to step (1).
In a nutshell, this procedure at every stage $n$, lists all ZFC theorems provable in $n$ steps (not already listed) by limiting oneself to the first $n$ rules of inference and the first $n$ axioms according to some recursive (computable) enumeration. Note that the the number of states required for such a Turing Machine is sensitive to ZFC only in the listing of the axioms (i.e., the number of states for the Turing machine carrying out step (2)).
The problem with such a Turing machine is that it exhibits no effective intelligence in its procedure. Its running time for producing theorems would be exponential as a function of the length of their shortest proofs and emulating it in a programming language such as C++ would not change this fact. Even if there were an obvious contradiction in ZFC with a proof requiring $1000$ lines (considering all of the formal manipulations, this isn't very long), it would most likely take somewhere on the order of $2^{1000}$ years to find. Therefore, the issue is not with the size of the Turing machine, but its running time. Indeed, there is an ongoing research program in automated theorem proving to only choose "smart" paths of deduction rather than mindlessly trying them all.
Finally let me address an issue with the number of symbols and coding. Anything that can be done with a Turing machine having a countable alphabet can be carried out by a Turing Machine having a binary alphabet (with a likely introduction of new states) under suitable coding. This is because there are only finitely many states and hence finitely many possible transitions. Specifically, given a finite collection of subsets $\{S_1, \ldots, S_n\}$ of a countable alphabet of symbols representing the possible transitions from one state to another, we can assign each symbol a Natural number so that each of the $S_n$ are finite unions of recursive sets (assigning first the $n$-intersection to a computable infinite coinfinite set of Natural numbers; then doing the same for each of the $(n-1)$-intersections with the remaining unassigned symbols and Natural numbers, down to the individual $S_i$) and hence recursive.
Also, with coding, your question admits an annoying answer. This is similar to a question I asked in Asymptotic density of provable statements in ZFC.
Specifically, if ZFC is inconsistent, then a Turing machine printing two contradictory statements and then halting would get the job done. Otherwise, we can bijectively associate the set of Natural numbers with the set of all binary strings. By taking any computable infinite and coinfinite subset $A$ of the Natural numbers, we can code the statements in the language of set theory so that the ZFC theorems are precisely the Natural numbers (binary strings) from $A$. This means that a Turing Machine could require an arbitrarily large number of states if $A$ is suitably complex or very few if $A$ were something simple.
