Navigation – Plan du site
Logic and Philosophy of Science in Nancy (I)

Gödel’s Incompleteness Phenomenon—Computationally

Saeed Salehi
p. 23-37


Nous soutenons que le théorème de complétude de Gödel est équivalent à la complétabilité de théories consistentes, et que son théorème d'incomplétude est équivalent au fait que cette complétion n'est pas constructive, en ce sens qu'il existe des théories consistantes et récursivement énumérables qui ne peuvent être étendues à aucune théorie complète et consistente et récursivement énumérable. Toutefois, n'importe quelle théorie consistente et décidable peut être étendue à une théorie complète, consistente et décidable. Donc la déduction et la consistence ne sont pas décidables en logique, et un analogue du théorème de Rice est valable pour les théories récursivement énumérables : toutes leurs propriétés non-triviales sont indécidables.

Haut de page

Texte intégral

1 Introduction

1The incompleteness theorem of Kurt Gödel has been regarded as the most significant mathematical result in the twentieth century, and Gödel’s completeness theorem is a kind of the fundamental theorem of mathematical logic. To avoid confusion between these two results, it is argued in the literature that the completeness theorem is about the semantic completeness of first order logic, and the incompleteness theorem is about the syntactic incompleteness of sufficiently strong first order logical theories. In this paper we look at these two theorems from another perspective. We will argue that Gödel’s completeness theorem is a kind of completability theorem, and Gödel-Rosser’s incompleteness theorem is a kind of incompletability theorem in a constructive manner. By Gödel’s semantic incompleteness theorem we mean the statement that any sound and sufficiently strong and recursively enumerable theory is incomplete. By Gödel-Rosser’s incompleteness theorem we mean the statement that any consistent and sufficiently strong and recursively enumerable theory is incomplete. Gödel’s original incompleteness theorem’s assumption is between soundness and consistency; it assumes ω − consistency of sufficiently strong and recursively enumerable theories which are to be proved incomplete.

2It is noted in the literature that the existence of a non-recursive but recursively enumerable set can prove Gödel’s semantic incompleteness theorem (see e.g., [Lafitte 2009] or [Li & Vitányi 2008]). This beautiful proof is most likely first proposed by [Kleene 1936] and Church; below we will give an account of this proof after Theorem 12. A clever modification of this proof shows Gödel-Rosser’s (stronger) incompleteness theorem, and in fact provides an elementary and nice proof of Gödel-Rosser’s theorem other than the classical Rosser’s trick [Rosser 1936]. This is called Kleene’s Symmetric Form of Gödel’s Incompleteness Theorem (see [Beklemishev 2010]) originally published in [Kleene 1950] and later in the book [Kleene 1952]. Indeed, Gödel’s semantic incompleteness theorem is equivalent to the existence of a non-recursive but recursively enumerable set, and also Gödel-Rosser’s (constructive) incompleteness theorem is equivalent to the existence of a pair of recursively (effectively) inseparable recursively enumerable sets.

3We will present a theory which is computability theoretic in nature, in a first order language which does not contain any arithmetical operations like addition or multiplication, nor set theoretic relation like membership nor sting theoretic operation like concatenation. We will use a ternary relation symbol τ which resembles Kleene’s T predicate and our theory resembles Robinson’s R arithmetic (see [Tarski, Mostowski et al. 1953]). The proofs avoid using the diagonal (or fixed-point) lemma which is highly counter-intuitive and a kind of “pulling a rabbit out of the hat” (see [Wasserman 2008]); the proofs are also constructive, in the sense that given a recursively enumerable theory that can interpret our theory one can algorithmically produce an independent sentence. For us the simplicity of the proofs and elementariness of the arguments are of essential importance. Though we avoid coding sentences and proofs and other syntactic notions, coding programs is needed for interpreting the τ relation. We also do not need any mathematical definition for algorithms or programs (like recursive functions or Turing machines etc); all we need is the finiteness of programs (every program is a finite string of ascii1 codes) and the finiteness of input and time of computation (which can be coded or measured by natural numbers). So, Church’s Thesis (that every intuitively computable function is a recursive function, or a function defined rigorously in a mathematical framework) is not used in the arguments.

2 Completeness and completability

4In mathematical logic, a theory is said to be a set of sentences, in a fixed language (see e.g., [Chiswell & Hodges 2007]; in [Kaye 2007] for example the word “theory” does not appear in this sense at all, and instead “a set of sentences” is used). Sometimes a theory is required to be closed under (logical) deduction, i.e., a set of sentences T is called a theory if for any sentence φ which satisfies T  ⊢  φ we have φ ∈ T (see e.g., [Enderton 2001]). Here, by a theory we mean any set of sentences (not necessarily closed under deduction). Syntactic completeness of a theory is usually taken to be negation-completeness: a theory T is complete when for any sentence φ, either T  ⊢  φ or T  ⊢  ¬φ. Let us look at the completeness with respect to other connectives:

5Definition 1 (Completeness). A theory T is called

  • ¬ − complete when for any sentence φ:
    T ⊢ ¬φT φ.

  • ∧ − complete when for any sentences φ and ψ:
    T  ⊢  φ ∧ ψ ⇔ T  ⊢  φ and T  ⊢  ψ.

  • ∨ − complete when for any sentences φ and ψ:
    T  ⊢  φ ∨ ψ ⇔ T  ⊢  φ or T  ⊢  ψ.

  • →  − complete when for any sentences φ and ψ:
    T  ⊢  φ → ψ ⇔ if T  ⊢  φ then T  ⊢  ψ.

  • ∀ − complete when for every formula φ(x):
    T  ⊢  ∀(x) ⇔ for every t, T  ⊢  φ(t).

  • ∃ − complete when for every formula φ(x):
    T  ⊢  ∃(x) ⇔ for some t, T  ⊢  φ(t).

6Let us note that the half of ¬ − completeness is consistency: a theory is called consistent when for every sentence φ, if T  ⊢  ¬φ then T φ. Usually, the other half is called completeness, i.e., when if T φ then T  ⊢  ¬φ for every sentence φ.

7Remark 2. Any theory is ∧ −complete and ∀ −complete (in first-order logic). Also, half of ∨ ,  → , ∃ −completeness holds for all theories T; i.e.,

  • if T  φ or T  ψ, then T  ⊢  φ  ψ;

  • if T  ⊢  φ → ψ, then if T  ⊢  φ then T  ⊢  ψ;

  • if T  ⊢  φ(t) for some t, then T  ⊢  ∃(x).

8A maximally consistent theory is a theory T which cannot properly be extended to a consistent theory; i.e., for any consistent theory T′ which satisfies T ⊆ T′ we have T = T′. The following is a classical result in mathematical logic (see e.g., [Dalen 2013]).

9Remark 3. A consistent theory is ¬complete if and only if is complete if and only if is  →  −complete if and only if is maximally consistent.

10Consistently maximizing a theory suggests using Zorn’s Lemma or (equivalently) the Axiom of Choice, which is non-constructive in general. To see if one can do it constructively or not, we need to introduce some other notions. Before that let us note that ∃ − completing a theory can be done constructively.

11Remark 4. Any arbitrary first-order consistent theory can be extended (constructively) to another consistent ∃ −complete theory.

12The main idea of the proof is that we add a countable set of constants {c1, c2, ⋯} to the language, and then enumerate all the couples of formulas and variables in the extended language as ⟨φ1, x1⟩, ⟨φ2, x2⟩, ⋯ and finally add the sentences ∃x1φ1 → φ(cl1/x1), ∃x2φ2 → φ(cl2/x2), ⋯ successively to the theory, where in each step cli is the first constant which does not appear in φ1, …, φi and has not been used in earlier steps (see e.g., [Enderton 2001]).

13Let us note that ∃ − complete theories are sometimes called Henkin theories or Henkin-complete or Henkin sets (see e.g., [van Dalen 2013]). These are used for proving Gödel’s Completeness Theorem by Henkin’s proof. The theory of a structure is the set of sentences (in the language of that structure) which are true in that structure. It can be seen that theories of structures are (¬, ∃) − complete theories. Conversely, for any (¬, ∃) − complete theory T one can construct a structure ℳ such that T is the theory of ℳ.

14Remark 5. Any consistent theory can be extended to a (¬, ∃) − complete theory. Note that any (¬, ∃) − complete theory is complete with respect to all the other connectives.

15Gödel’s completeness theorem is usually proved by showing that any consistent theory has a model (the model existence theorem–which is equivalent to the original completeness theorem). Note that for proving the model existence theorem it is shown that any consistent theory is extendible to a consistent (¬, ∃) − complete theory, which then defines a structure which is a model of that theory. Thus, we can rephrase this theorem equivalently as follows.

16Gödel’s completeness theorem : Any first-order consistent theory can be extended to a consistent (¬, ∃) − complete theory.

17This theorem can be considered as the fundamental theorem of logic, the same way that we have the fundamental theorem of arithmetic, or the fundamental theorem of algebra, or the fundamental theorem of calculus. We could also call this theorem, Gödel’s Completability Theorem, for the above reasons.

3 Incompleteness and incompletability

We now turn our attention to constructive aspects of the above theorem. A possibly infinite set can be constructive when it is decidable or (at least) recursively enumerable. A set D is decidable when there exists a single-input algorithm which on any input x outputs Yes if x ∈ D and outputs No if x ∉ D. A set R is called recursively enumerable (re for short) when there exists an input-free algorithm which outputs (generates) the elements of R (after running). It is a classical result in Computability Theory that there exists an re set which is not decidable (though, any decidable set is re); see e.g., [Epstein & Carnielli 2008]. For a theory T we can consider decidability or recursive enumerability of either T as a set of sentences, or the set of derivable sentences of T, i.e., Der(T)={φ | T ⊢ φ}. It can be shown that if T is decidable or re (as a set) then Der(T) is re; of course when Der(T) is re then T is re as well, and by Craig’s trick [Craig 1953] for such a theory there exists a decidable set of sentences such that Der(T)= Der(). So, we consider re theories only, and call theory T a decidable theory when Der(T) is a decidable set (of sentences). re theories are sometimes called axiomatizable theories (in e.g., [Enderton 2001]). Below we will show that there exists some decidable set of sentences (Image 100000000000000B0000000C4320FBE2.png) whose set of derivable sentences is not decidable (though it must be re of course).

18Definition 6. re, Decidable and re-Completable. A consistent theory

  • T is called an re theory when Der(T) is an re set.

  • T is called a decidable theory when Der(T) is a decidable set.

  • T is called re-completable when there exists a theory T′ extending T (i.e., T ⊆ T′) such that T′ is consistent, complete and re.

19It is a classical fact that complete re theories are decidable (see e.g., [Enderton 2001]): since by recursive enumerability of T both {φ ∣ T  ⊢  φ} and {φ ∣ T  ⊢  ¬φ} are re and by the completeness of T we have {φ | T φ}={φ | T ⊢ ¬φ\}, so the set Der(T) and its complement are both re and hence decidable (by Kleene’s Complementation Theorem—see e.g., [Berto 2009]). Completeness is a logician’s tool for decidability. Henkin’s completion shows that any re decidable theory is re—completable, see [Tarski, Mostowski, et al. 1953]. The main idea is that having a decidable theory T we list all the sentences in the language of T as φ1, φ2, ⋯ and then add φi or ¬φi in the ith step to T as follows: let T0 = T and if Tj is defined let Tj + 1 = Tj ∪ {φj} if Tj ∪ {φj} is consistent, otherwise let Tj + 1 = Tj ∪ {¬φj}. Note that if Tj is consistent, then Tj + 1 will be consistent as well (if Tj ∪ {φj} is inconsistent then Tj ∪ {¬φj} must be consistent). The theory T′ = ⋃i ≥ 0Ti will be consistent and complete. This was essentially Henkin’s Construction for proving Gödel’s completeness theorem. The point is that if T is decidable then so is any Ti since they are finite extensions of T. Finally, T′ is a decidable theory, because for any given sentence φ it should appear in the list φ1, φ2, ⋯, so say φ = φn. Now, for i = 1, 2, …, n we can decide whether φi ∈ T′ or ¬φi ∈ T′ inductively; and finally we can decide whether T′  ⊢  φ or not (T φ happens only when T′  ⊢  ¬φ). So, for consistent re theories we have the following inclusions:






20Below we will see that the converse conclusions do not hold (Remark 10). Whence, by contrapositing the above conclusions we will have the following inclusions and non-inclusions for some consistent re theories:






21Incomplete theories abound in mathematics: every theory which has finite models but does not fix the number of elements (e.g., theory of groups, rings, fields, lattices, etc.) is an incomplete theory. By encoding Turing machines into a first order language one can obtain an undecidable theory (see e.g., [Boolos, Burgess, et al. 2007]). But demonstrating an re-incompletable theory is a difficult task and it is in fact Gödel’s Incompleteness Theorem. re-incompletable theories are known as “essentially undecidable” theories in the literature (starting from [Tarski, Mostowski, et al. 1953]). Comparing Gödel’s Completeness Theorem with his Incompleteness Theorem, we come to the following conclusion.

22Every consistent theory can be extended to a (¬,∃)−complete theory (Gödel's Completeness Theorem) and this completion preserves decidability, i.e., every consistent and decidable theory can be extended to a consistent, decidable and (¬,∃)−complete theory. But this completion cannot be necessarily effective; i.e., there are some consistent re theories whose all consistent completions are non-re (Gödel's Incompleteness Theorem).

23So, calling the completeness theorem of Gödel Completability Theorem we can call (the first) incompleteness theorem of Gödel (and Rosser) re-Incompletability Theorem.

3.1 An undecidable but RE-completable theory

In this paper we introduce an incomplete but re-completable theory (Image 100000000000000B0000000C4320FBE2.png) and a novel re-incompletable theory (Image 100000000000000800000009CA37C756.png), and for that we consider the theory of zero, successor and order in the set of natural numbers, i.e., the structure ⟨ℕ, 0, s,  < ⟩ in which 0 is a constant symbol, s is a unary function symbol and  <  is a binary relation symbol (interpreted as the zero element, the successor function and the order relation, respectively). This theory is known to be decidable [Enderton 2001], and in fact can be finitely axiomatized as follows

A1 : ∀xy(x < y → y x),

A2  :  ∀xyz(x < y ∧ y < z → x < z),

A3  :  ∀xy(x < y ∨ x = y ∨ y < x),

A4 :  ∀xy(x < y ↔ s(x) < y ∨ s(x) = y),

A5 : ∀x(x ≮ 0),

A6 : ∀x(0 < x → ∃v(x = s(v))).

24The axioms A1, A2, A3 state that  <  is a (linear and transitive and antisymmetric, thus a) total ordering, A4 states that every element has a successor (the successor s(x) of x satisfies ∀y(x < y ↔ s(x) < y ∨ s(x) = y)), A5 states that there exists a least element (namely 0) and finally A6 states that every non-zero element has a predecessor. One other advantage of the language {0, s,  < } is that we have terms for every natural number n ∈ ℕ:

n is the {0, s} − term sn0 = Image 100000000000002B000000195F74C765.png 0.

25To the language {0, s,  < } we add a ternary relation symbol τ interpreted as:

for e, x, t ∈ ℕ the relation τ(e, x, t) holds when e is a code for a single-input program which halts on input x by time t.

26Timing of a program can be measured either by the number of steps that the program runs or just by the conventional seconds, minutes, hours, etc., and programs (say in a fixed programming language like C++) can be coded by natural numbers as follows (for example): any such program is a (long) string of ascii codes, and every ascii code can be thought of as 8 symbols of 0’s and 1’s (so, there are 256 ascii codes). So, any program is a string of 0’s and 1’s (whose length is a multiple of 8). The set of 0,1-strings can be coded by natural numbers in the following way:

























27This coding works as follows: given a string of ’s and ’s (take for example 0110), put a 1 at the beginning of it (in our example 10110) and compute its binary value (in our example 2+22+24=22) and subtract 1 from it (in our example 21) to get the natural number which is the code of the original string. Conversely, given a natural number (for example 29) find the binary representation of its successor (in our example 30=2+22+23+24=(11110)2) and remove the from its beginning (in our example 1110) to get the 0,1-string which corresponds to the given natural number.

28Whence, any program can be coded by a natural number constructively, and if a natural number is a code for a program, then that program can be decoded from that number algorithmically. Let us note the ternary relation τ resembles Kleene’s T Predicate (see [Kleene 1936]).

Definition 7 (The Theory Image 100000000000000B0000000C4320FBE2.png). Theory Image 100000000000000B0000000C4320FBE2.png is axiomatized by A1, A2, A3, A4, A5 and A6 with the following set of sentences in the language {0, s,  < , τ}:

A7 : {τ(e,x,t) | e,x,t ∈ ℕ & ℕ⊨ τ(e,x,t)}

29The set of axioms A7 consists of the sentences τ(e,x,t) (recall that n is the {0, s} − term representing the number n ∈ ℕ) such that τ(e, x, t) holds in reality (the single-input program with code e halts on input x by time t).

Remark 8 [re-completability of Image 100000000000000B0000000C4320FBE2.png]. The set of sentences in Image 100000000000000B0000000C4320FBE2.png is decidable (given any n,m,k one can decide whether τ(n,m,k) holds or not), and thus Image 100000000000000B0000000C4320FBE2.png is an re theory. It is also re-completable, since its extension by the sentence xyz(τ(x,y,z)) is a decidable theory (equivalent to the theory of the structure ⟨ℕ, 0, s,  < ⟩ which is decidable—see [Enderton 2001]).

The theory Image 100000000000000B0000000C4320FBE2.png is undecidable, since the halting problem is undecidable (see e.g., [Epstein & Carnielli 2008]): for any (single-input program with code) e ∈ ℕ and any (input) m ∈ ℕ, let φe,m be the sentence ∃z, τ(e,m,z). Then

Image 100000000000000B0000000C4320FBE2.png  ⊢  φe, m


ℕ⊨ τ(e,m,t) for some t


the program e eventually halts on input m.

30This can be shown directly, by incorporating the proof of the undecidability of the halting problem.

Theorem 9 (Undecidability of Image 100000000000000B0000000C4320FBE2.png) The theory Image 100000000000000B0000000C4320FBE2.png is undecidable.

Proof. If the set Der(Image 100000000000000B0000000C4320FBE2.png) is decidable, then so is the set
Image 100000000000000A0000000976EA13E6.png={n∈‎ℕ |Image 100000000000000B0000000C4320FBE2.png\⊬ ∃ z,τ(n,n,z)}.

Whence, there exists a program which on input n ∈ ℕ halts whenever n ∈ Image 100000000000000A0000000976EA13E6.png (and when n ∉ Image 100000000000000A0000000976EA13E6.png then the program does not halt and loops forever). Let e be a code for this (single-input) program. Then

the program (with code) e halts on input e  ⇔  ℕ⊨τ(e,e,k) for some k  ⇔  Image 100000000000000B0000000C4320FBE2.png ⊢ ∃ z\,τ(e,e,z)  ⇔  e ∉ Image 100000000000000A0000000976EA13E6.png ⇔  (by e’s definition) the program (with code) e does not halt on input e. Contradiction!

Remark 10. Thus far, we have shown that an undecidable theory need not be re-incompletable (Image 100000000000000B0000000C4320FBE2.png). One can also show that an incomplete theory need not be undecidable; to see this consider the theory {∃xyz(z=xz=y)} in the language of equality ( = ). This theory is decidable (holds in models of at most two elements) but not complete, since can derive neither xy(x=y) nor ¬xy(x=y).

31Corollary 11 (Undecidability of Consistency). It is not decidable whether a given re theory is consistent or not.

32Proof. By [T  ⊢  φ]  ⇔  [T ∪ {¬φ} is inconsistent] if consistency of re theories was decidable then every re theory would be decidable too.

Thus, we have shown the existence of an re theory (Image 100000000000000B0000000C4320FBE2.png) which is undecidable but re-completable. Next, we show the existence of an re theory which is not re-completable. Before that let us note that the above proof works for any (consistent and re) theory T ⊇ Image 100000000000000B0000000C4320FBE2.png which is sound (i.e., ℕ ⊨ T).

Theorem 12. There exists no complete, sound and re theory extending Image 100000000000000B0000000C4320FBE2.png. In other words, the theory Image 100000000000000B0000000C4320FBE2.png cannot be soundly re-completed.

33This is essentially the semantic form of Gödel’s first incompleteness theorem. As a corollary we have that the theory of ⟨ℕ, 0, s,  < , τ⟩ is not re (nor decidable). Let us note that the above proof of the first (semantic) incompleteness theorem of Gödel is some rephrasing of Kleene’s proof (see [Kleene 1936]). For a (single-input) program (with code) e let We be the set of the inputs such that e eventually halts on them, i.e., We = {n ∣ ℕ ⊨ ∃zτ(e, n, z)}. By Turing’s results it is known that the set K = {n ∣ n ∈ Wn} is re but not decidable (see e.g., [Epstein & Carnielli 2008]). Indeed, its complement ={n | n ∉ Wn} is not re because every re set is of the form Wm for some m (see e.g., [Epstein & Carnielli 2008]) and for any n we have n∈‎ (\ Wn) ∪ (Wn \ ). On the other hand for any re theory T the set

K̅T = {n | T ⊢ “n∈‎K̅”} = {n | T ⊢ ¬∃ z,τ(n,n,z)}

is re. Now, if T is sound (ℕ ⊨ T) then K̅T K̅. The inclusion must be proper because one of them (K̅T) is re and the other one (K̅) is not re. If K̅T=Wm (for some m ∈ ℕ) then m∈‎ K̅ - K̅T: because if m∈‎K̅T(= Wm) then m ∈ Wm and so mK̅, and this contradicts the inclusion K̅T K̅; thus m ∉ K̅T and so m ∉ Wm which implies that m∈‎K̅. Hence, the sentence ¬∃ z,τ(m,m,z) is true but unprovable in T; thus T is incomplete.

3.2 An RE-incompletable theory

In the above arguments we used the soundness assumption of T (and Image 100000000000000B0000000C4320FBE2.png). Below, we will introduce a consistent and re theory Image 100000000000000800000009CA37C756.png which is not re-completable. Let π be a binary function symbol (representing some pairing—for example π(n, m) = (n + m)2 + n) whose interpretation in ℕ satisfies the pairing condition: for any a, b, a′, b′ ∈ ℕ we have ℕ ⊨ π(a, b) = π(a′, b′) if and only if a = a′ and b = b′.

Definition 13 (The Theory Image 100000000000000800000009CA37C756.png). The theory Image 100000000000000800000009CA37C756.png is the extension of the theory Image 100000000000000B0000000C4320FBE2.png by the following sets of sentences in the language {0, s,  < , τ, π}:

A8 : {¬τ(e,x,t) | e,x,T ∈ ℕ & ℕ ⊭ τ(e,x,t)}

A9: {∀x<(x<k⟷<⋁i<kx=i) | k∈‎ℕ}

We now show that the theory Image 100000000000000800000009CA37C756.png is not re-completable. Let us note that Gödel’s original first incompleteness theorem showed the existence of some theory which was not soundly re-completable. Actually, Gödel used a syntactic notion weaker than “soundness”, namely ω consistency, which is stronger than consistency itself. Nowadays it is known that Gödel’s proof works for an even weaker condition than ω − consistency, the so called 1-consistency (see [Isaacson 2011]). It was then Rosser who showed that Gödel’s theorem can be proved without using the ω − consistency (even 1-consistency) assumption (see [Rosser 1936] or e.g., [Boolos, Burgess et al. 2007]); so the theorem of Gödel-Rosser states the existence of a consistent and re theory which is not re-completable.

Theorem 14 (re-incompletability of Image 100000000000000800000009CA37C756.png) If T is a consistent re theory that extends Image 100000000000000800000009CA37C756.png (i.e., TImage 100000000000000800000009CA37C756.png), then T is not complete.

Proof. Suppose T is a consistent and re extension of Image 100000000000000800000009CA37C756.png. We show that T is not complete. For any a, b ∈ ℕ let φa,b be the sentence

x(τ(a,π(a,b),x)∧ ∀ y<xτ(b,π(a,b),y)).

34Let m be a code of a program which on input p ∈ ℕ halts if and only if there are some k, l ∈ ℕ such that p = π(k, l) (in which case the numbers k and l are unique) and there exists a proof of φk,l in T (i.e., T  ⊢  φk,l). So, if (i) p is not in the range of the function π, or (ii) there are (unique) k, l such that p = π(k, l) and T φk,l, then the program does not halt on p. Whence, the program with code m searches for a proof of φk,l in T on input π(k, l).

35Also, let n be a code for a program which for an input p ∈ ℕ halts if and only if there are some (unique) k, l ∈ ℕ such that p = π(k, l) and there exists a proof of ¬φk,l in T (i.e., T  ⊢  ¬φk,l). So, if p is not in the range of the function π or if there are (unique) k, l such that p = π(k, l) and T ⊬ ¬φk,l then the program with code n does not halt on p. Again, this program searches for a proof of ¬φk,l in T on input π(k, l).

36We prove that φn,m is independent from T, i.e., T φn,m and T ⊬ ¬φn,m.

37(1) If T  ⊢  φn,m then by the consistency of T we have T ⊬ ¬φn,m. So, on input π(n, m) the program with code m halts and the program with code n does not halt. Whence, for some natural number t, ℕ ⊨ τ(m, π(n, m), t) and for every natural number s, ℕ⊭τ(n,π(n,m),s). So by A7 and A8 for that (fixed) t ∈ ℕ we have Tτ(m,π(n,m),t), and for every s ∈ ℕ we have T ⊢ ¬τ(n,π(n,m),s). Thus, T ⊢ ⋀it ¬τ(n,π(n,m),i), and so by A9, we conclude that T ⊢ ∀xt¬τ(n,π(n,m),x), therefore

(i) T ⊢ ∀x(τ(n,π(n,m),x)→x>t).

38Also by Tτ(m,π(n,m),t) we get

(ii) T ⊢ ∀x>t<(∃y<x,τ(m,π(n,m),y)).

39Combining these two conclusions we infer that

T ⊢ ∀x(τ(n,π(n,m),x)→∃y<x,τ(m,π(n,m),y)).

40On the other hand by the definition of φa,b we have

φn,m ≡ ∃x(τ(n,π(n,m),x)∧∀y<x¬τ(m,π(n,m),y)),

and so ¬φn,m ≡ ∀x(τ(n,π(n,m),x)→∃y<x,τ(m,π(n,m),y)).

41Thus we deduced T  ⊢  ¬φn,m from the assumption T  ⊢  φn,m; contradiction! Whence, T φn,m.

42(2) If T  ⊢  ¬φn, m then (again) by the consistency of T we have T φn,m. So, on input π(n, m) the program with code n halts and the program with code m does not halt. Whence, for some natural number t, ℕ ⊨ τ(n, π(n, m), t) and for every natural number s, ℕ⊭τ(m,π(n,m),s). Similarly to the above we can conclude that T τ(n,π(n,m),t) and T ⊢ ∀y<tτ(m,π(n,m),y). Thus (for x = t) we have

T ⊢ ∃x(τ(n,π(n,m),x)∧∀y<x¬τ(m,π(n,m),y))

43or T  ⊢  φn,m; contradiction! So, T ⊬ ¬φn,m.

44Whence, T is not complete.

The above proof is effective, in the sense that given an re theory (by a code for a program that generates its elements) that extends Image 100000000000000800000009CA37C756.png one can generate (algorithmically) a sentence which is independent from that theory. Let us note that for proving re-incompletability of theories, it suffices to interpret Image 100000000000000800000009CA37C756.png in them. So, the theories Q, R (see [Tarski, Mostowski & Robinson 1953]) and Peano’s Arithmetic PA are all re-incompletable (or, essentially undecidable).

4 Rice’s theorem for RE theories

45In this last section we show a variant of Rice’s Theorem for logical theories. In [Oliveira & Carnielli 2008] the authors (claimed to) had shown that an analogue of Rice’s theorem holds for finitely axiomatizable first order theories. Unfortunately, the result was too beautiful to be true [Oliveira & Carnielli 2009] and it turned out that Rice’s theorem cannot hold for finite theories. However, we show that this theorem holds for re theories, a result which is not too different from Rice’s original theorem. Recall that two theories T1 and T2 are equivalent when they prove the same (and exactly the same) sentences (i.e., Der(T1)= Der(T2)).

Definition 15 (Property of Theories). A property of (first order logical) theories is a set of natural numbers Image 100000000000000A0000000AA4CD0EB1.png ⊆ ℕ such that for any m, n ∈ ℕ if the theory generated by the program with code m is equivalent to the theory generated by the program with code n, then m ∈ Image 100000000000000A0000000AA4CD0EB1.png ↔ n ∈ Image 100000000000000A0000000AA4CD0EB1.png.

So, a theory is said to have the property Image 100000000000000A0000000AA4CD0EB1.png when a code for generating its set belongs to Image 100000000000000A0000000AA4CD0EB1.png. A property of theories is a non-trivial property when some theories have that property and some do not.

46Example 16. The followings are some non-trivial properties of re theories:

  • Universal Axiomatizability: theories axiomatizable by sentences of the form ∀x1…∀xnθ(x1, …, xn) for quantifier-free θ’s;

  • Finite Axiomatizability: being equivalent to a finite theory;

  • Decidability (of the set of the theorems of the theory);

  • Having a Finite Model;

  • Completeness;

  • Consistency.

Remark 17. For any non-trivial property Image 100000000000000A0000000AA4CD0EB1.png either (i) no inconsistent theory has the property Image 100000000000000A0000000AA4CD0EB1.png or (ii) all inconsistent theories have the property Image 100000000000000A0000000AA4CD0EB1.png. Because when an inconsistent theory breaks into Image 100000000000000A0000000AA4CD0EB1.png then all the other inconsistent theories (being equivalent to each other) come in.

Before proving Rice’s Theorem let us have a look at (a variant of) Craig’s trick. For an re theory T = {T1, T2, T3, ⋯} the proof predicate “p is a proof of φ in T”, for given sequence of sentences p and sentence φ, might not be decidable when the set {T1, T2, T3, ⋯} is not decidable. Note that “the sequence p is a proof of φ in T” when every element of p is either a (first order) logical axiom (which can be decided) or is an element of T or can be deduced from two previous elements by an inference rule, and the last element of p is φ. Thus decidability of the set T is essential for the decidability of the proof sequences of T. But if we consider the theory =\{1,2,3,⋯} where m=⋀i≤m}Ti then the set is decidable, because if Image 100000000000000B0000000AF9A1BC01.png is an algorithm that outputs (generates) the infinite sequence ⟨T1, T2, T3, ⋯⟩ in this order (in case T is finite the sequence is eventually constant), then for any given sentence ψ we can decide if ψ∈‎ or not by checking if ψ is a conjunction of some sentences ψ = ψ1 ∧ ⋯ ∧ ψm (if ψ is not of this form, then already ψ ) such that Image 100000000000000B0000000AF9A1BC01.png’s ith output is ψi for i = 1, …, m (if not then again ψ‎ ∉‎). Whence the predicate of being a proof of φ in , i.e., “the sequence p is a proof of sentence φ in ”, is decidable; moreover the theories T and are equivalent, and the theory can be algorithmically constructed from given theory T.

47Theorem 18 (Analogue of Rice’s Theorem) All the non-trivial properties of re theories are undecidable.

Proof. Assume a non-trivial property Image 100000000000000A0000000AA4CD0EB1.png of re theories is decidable, i.e., there exists an algorithm which on input n ∈ ℕ decides whether n ∈ Image 100000000000000A0000000AA4CD0EB1.png (i.e., whether the theory generated by the program with code n has the property Image 100000000000000A0000000AA4CD0EB1.png). Without loss of generality we can assume that no inconsistent theory has the property Image 100000000000000A0000000AA4CD0EB1.png (otherwise take the complement of Image 100000000000000A0000000AA4CD0EB1.png). Fix a consistent re theory, say, S = {S1, S2, S3, ⋯} that has the property Image 100000000000000A0000000AA4CD0EB1.png (S could be finite in which case the sequence {Si}i is eventually constant) and fix a sentence ψ. For any given re theory T we construct the theory T′ = {T1, T2, T3, ⋯} as follows: let Tk = Sk if k is not a (code of a) proof of ψ ∧ ¬ψ in T̂ (see above); otherwise let Tk = ψ ∧ ¬ψ. Note that this construction is algorithmic, since being a (code for a) proof of ψ ∧ ¬ψ in the decidable set T̂ is decidable (and the theory T̂ can be constructed algorithmically for a given re theory T); moreover, the theory T′ is re. Now, if T is consistent then T′ = S has the property Image 100000000000000A0000000AA4CD0EB1.png and if T is not consistent then T′ is an inconsistent theory (because then for some k, Tk = ψ ∧ ¬ψ) and so does not have the property Image 100000000000000A0000000AA4CD0EB1.png. Whence, for any re theory T we have the re theory T′ in such a way that

[T is consistent] ⇔ [T′ has the property Image 100000000000000A0000000AA4CD0EB1.png].

Now by Corollary [cor-con] the property Image 100000000000000A0000000AA4CD0EB1.png is not decidable.

48Finally, we note that as a corollary to the above theorem, finite axiomatizability of re theories is not a decidable property; and there exists a decidable non-trivial property for finite theories: for a fixed decidable theory (like the theory {A1, ⋯, A6} in Definition 7), say F, it is decidable whether a given finite theory T is included in F (i.e., if F can prove all the sentences of T).

The author is partially supported by grant №92030033 of the Institute for Research in Fundamental Sciences (Image 100000000000003A0000000F2419A9C7.png), Tehran, Iran.

Haut de page


Beklemishev, Lev D. [2010], Gödel incompleteness theorems and the limits of their applicability: I, Russian Mathematical Surveys, 65(5), 857–899, doi:10.1070/RM2010v065n05ABEH004703.

Berto, Francesco [2009], There’s Something about Gödel: The Complete Guide to the Incompleteness Theorem, Malden, MA: Wiley-Blackwell.

Boolos, George S., Burgess, John P., & Jeffrey, Richard C. [2007], Computability and Logic, Cambridge; New York: Cambridge University Press, 5th edn.

Chiswell, Ian & Hodges, Wilfrid [2007], Mathematical Logic, London; New York: Oxford University Press.

Craig, William [1953], On axiomatizability within a system, The Journal of Symbolic Logic, 18(1), 30–32, doi:10.2307/2266324.

Enderton, Herbert B. [2001], A Mathematical Introduction to Logic, San Diego: Academic Press, 2nd edn.

Epstein, Richard L. & Carnielli, Walter A. [2008], Computability: Computable Functions, Logic, and the Foundations of Mathematics, Pacific Grove: Advanced Reasoning Forum, 3rd edn.

Isaacson, Daniel [2011], Necessary and sufficient conditions for undecidability of the Gödel sentence and its truth, in: Logic, Mathematics, Philosophy, Vintage Enthusiasms: Essays in honour of John L. Bell, edited by D. DeVidi, M. Hallett, & P. Clark, Dordrecht; New York: Springer, 135–152, doi:10.1007/978-94-007-0214-1_7.

Kaye, Richard W. [2007], The Mathematics of Logic: A guide to completeness theorems and their applications, Cambridge; New York: Cambridge University Press.

Kleene, Stephen C. [1936], General recursive functions of natural numbers, Mathematische Annalen, 112(1), 727–742.

—— [1950], Symmetric form of Gödel’s theorem, Indagationes Mathematicae, 12, 244–246.

—— [1952], Introduction to Metamathematics, Amsterdam: North-Holland.

Lafitte, Grégory [2009], Busy beavers gone wild, in: Proceedings of the International Workshop on the Complexity of Simple Programs, edited by T. Neary, D. Woods, T. Seda, & N. Murphy, Cork, Ireland: Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, vol. 1, 123–129, doi:10.4204/EPTCS.1.12..

Li, Ming & Vitányi, Paul M. B. [2008], An Introduction to Kolmogorov Complexity and Its Applications, New York: Springer, 3rd edn.

Oliveira, Igor Carboni & Carnielli, Walter [2008], The Ricean objection: An analogue of Rice’s theorem for first–order theories, Logic Journal of the IGPL, 16(6), 585–590, doi:10.1093/jigpal/jzn023.

—— [2009], Erratum to “The Ricean objection: An analogue of Rice’s theorem for first–order theories”, Logic Journal of the IGPL, 17(6), 803–804, doi:10.1093/jigpal/jzp030.

Rosser, Barkley [1936], Extensions of some theorems of Gödel and Church, The Journal of Symbolic Logic, 1(3), 87–91, doi:10.2307/2269028.

Tarski, Alfred, Mostowski, Andrzej, & Robinson, Raphael M. [1953], Undecidable Theories, Amsterdam: North-Holland, reprinted by Dover Publications 2010.

van Dalen, Dirk [2013], Logic and Structure, London; New York: Springer, 5th edn.

Wasserman, Wayne U. [2008], It is “Pulling a rabbit out of the hat”: typical diagonal lemma “proofs” beg the question, doi:10.2139/ssrn.1129038.

Haut de page

Pour citer cet article

Référence électronique

Saeed Salehi, « Gödel’s Incompleteness Phenomenon—Computationally », Philosophia Scientiæ [En ligne], 18-3 | 2014, mis en ligne le 27 novembre 2014, consulté le 19 février 2018. URL : ; DOI : 10.4000/philosophiascientiae.968

Haut de page


Saeed Salehi

University of Tabriz & IPM (Iran)

Haut de page

Droits d’auteur

Tous droits réservés

Haut de page