◄ Index 
◄
Main essay
How definitive is the standard interpretation of
Gödel's Incompleteness Theorem?
Bhupinder
Singh Anand[1]
(A
.pdf file of this essay before the
current update is available at http://arXiv.org/abs/math/0307074)
Standard interpretations of
Gödel's “undecidable” proposition, [(Ax)R(x)], argue that, although [~(Ax)R(x)] is PA-provable if [(Ax)R(x)] is PA-provable, we may not
conclude from this that [~(Ax)R(x)] is PA-provable. We show that such
interpretations are inconsistent with a standard Deduction Theorem of first
order theories.
1. Introduction
1.1 An overview
2. A
standard Deduction Theorem
2.1 A
number-theoretic corollary
2.2 An
extended Deduction Theorem
3. An additional deduction theorem
4. Conclusion
1. Introduction
In his
seminal 1931 paper [Go31a], Gödel meta-mathematically
argues that his “undecidable” proposition, [(Ax)R(x)][2], is such that (cf. [An02b],
§1.6(iv)):
If [(Ax)R(x)] is
PA-provable, then [~(Ax)R(x)] is PA-provable.
Now, a
standard Deduction Theorem of an arbitrary first order theory states that ([Me64], p61, Corollary 2.6):
If T is a set of well-formed formulas of an
arbitrary first order theory K, and if [A] is a closed well-formed
formula of K, and if (T, [A])|-K [B], then T|-K
([A => B]).
In an
earlier essay ([An02b], Appendix 1), we
implicitly assumed, without proof, that:
(T, [A])|-K [B] holds
if, and only if, T|-K [B] holds when we assume T|-K
[A]. (*)
In
other words, we assumed that [B] is a deduction from (T, [A])
in K if, and only if, whenever [A][3] is a hypothetical deduction from T in K, [B]
is a deduction from T in K.
We then
argued, that it should follow (essentially by the reasoning in §2.2 below), that:
[(Ax)R(x) => ~(Ax)R(x)] is PA-provable,
and,
therefore, that:
[~(Ax)R(x)] is
PA-provable.
We then
concluded that PA is omega-inconsistent.
However,
this conclusion is inconsistent with standard interpretations of Gödel’s
reasoning, which, firstly, assert both [(Ax)R(x)] and [~(Ax)R(x)] as PA-unprovable, and, secondly, assume that PA can
be omega-consistent. Such interpretations, therefore, implicitly deny that the
PA-provability of [~(Ax)R(x)] can be inferred from the above meta-argument; ipso
facto, they imply that (*) is false.
In the
following sections, we review the Deduction Theorems used in the earlier
argument, and give a meta-mathematical proof of (*). It follows that the standard interpretations
of Gödel’s reasoning are inconsistent with a standard Deduction Theorem of an
arbitrary first order theory ([Me64], p61,
Corollary 2.6). We conclude that such interpretations cannot be accepted as definitive.
1.1 An overview
We
first review, in Theorem 1, the proof of a
standard Deduction Theorem, if (T, [A])|-K [B],
then T|-K [A => B], where an explicit
deduction of [B] from (T, [A]) is known.
We then
show, in Corollary 1.2, that Theorem 1 can be constructively extended to cases
where (T, [A])|-K [B] is established
meta-mathematically, and where an explicit deduction of [B] from (T,
[A]) is not known.
We
finally prove (*) in Theorem 2.
2.
A standard Deduction Theorem
The
following is, essentially, Mendelson’s proof of a standard Deduction Theorem ([Me64], p61, Proposition 2.4) of an arbitrary
first order theory K:
Theorem 1: If T is a set
of well-formed formulas of an arbitrary first order theory K, and if [A]
is a closed well-formed formula of K, and if (T, [A])|-K
[B], then T|-K [A => B].
Proof: Let <[B1], [B2],
..., [Bn]>
be a deduction of [B] from (T,
[A]) in K.
Then,
by definition, [Bn] is [B] and, for each i, either [Bi] is an axiom of K, or [Bi] is in T, or [Bi] is [A], or [Bi] is a direct consequence by some rules of inference
of K of some of the preceding well-formed formulas in the sequence.
We now
show, by induction, that T|-K [A => Bi] for each i =< n. As
inductive hypothesis, we assume that the proposition is true for all deductions
of length less than n.
(i) If [Bi] is an axiom, or belongs to T, then T|-K
[A => Bi], since [Bi => (A => Bi)] is an axiom of K.
(ii) If [Bi] is [A], then T|-K [A
=> Bi],
since T|-K [A => A].
(iii) If there
exist j, k less than i such that [Bk] is [Bj => Bi], then, by the inductive hypothesis, T|-K
[A => Bj], and T|-K [A => (Bj => Bi)]. Hence, T|-K [A => Bi].
(iv) Finally,
suppose there is some j < i such that [Bi] is [(Ax)Bi],
where x is a variable in
K. By hypothesis, T|-K [A => Bj]. Since x is not a free variable of [A], we have that [(Ax)(A => Bj) => (A => (Ax)Bj] is PA-provable. Since T|-K [A
=> Bj], it
follows by Generalisation that T|-K [(Ax)(A => Bj)], and so T|-K [A => (Ax)Bj], i.e. T|-K [A => Bi].
This
completes the induction, and Theorem 1 follows as
the special case where i = n. ¶[4]
2.1 A number-theoretic corollary
Now,
Gödel has defined ([Go31a], p22, Definition 45(6)) a primitive
recursive number-theoretic relation xB(K, T)y that holds if, and only if, x is the Gödel-number of a deduction from T of the K-formula
whose Gödel-number is y.
We thus
have:
Corollary 1.1[5]: If the Gödel-number of the well-formed K-formula [B]
is b, and that of the
well-formed K-formula [A => B] is c, then Theorem 1 holds
if, and only if[6]:
(Ex)xB(K, T, [A])b => (Ez)zB(K, T)c
2.2 An
extended Deduction Theorem
We next
consider the proposition:
Corollary 1.2: If we assume
Church’s Thesis[7], then Theorem 1 holds
even if the premise (T, [A])|-K [B] is
established meta-mathematically, and a deduction <[B1], [B2],
..., [Bn]>
of [B] from (T, [A]) in K is not known explicitly.
Proof: Since Gödel’s number-theoretic relation xB(K, T)y is primitive recursive, it follows that, if we assume
Church’s Thesis - which implies that a number-theoretic relation is decidable
if, and only if, it is recursive - we can effectively determine some finite
natural number n for which the
assertion nB(K, T,
[A])b holds,
where the Gödel-number of the well-formed K-formula [B] is b.
Since n would then, by definition, be the Gödel-number of a
deduction <[B1], [B2], ..., [Bn]> of [B] from (T, [A]) in K,
we may thus constructively conclude, from the meta-mathematically determined assertion
(T, [A])|-K [B], that some deduction <[B1],
[B2], ..., [Bn]> of [B] from (T, [A]) in K
can, indeed, be effectively determined.
Theorem 1 follows. ¶
3.
An additional deduction theorem
We
finally prove (*) as an additional
deduction theorem, in an arbitrary first order theory K:
Theorem 2: If K is an arbitrary
first order theory, and if [A] is a closed well-formed formula of K,
then (T, [A])|-K [B] if, and only if, T|-K
[B] holds when we assume T|-K [A].
Proof: Firstly, if there is a deduction <[B1],
[B2], ..., [Bn]> of [B] from (T, [A]) in K,
and there is a deduction <[A1], [A2],
..., [Am]>
of [A] from T in K, then <[A1], [A2],
..., [Am], [B1],
[B2], ..., [Bn]> is a deduction of [B] from T in K.
Hence we have: if (T, [A])|-K [B], then T|-K
[B] holds when we assume T|-K [A].
Secondly,
if there is a deduction <[B1], [B2],
..., [Bn]>
of [B] from T in K, then we have, trivially, that: if T|-K
[B] holds when we assume T|-K [A], then (T,
[A])|-K [B].
Lastly,
we assume that there is no deduction <[B1], [B2],
..., [Bn]>
of [B] from T in K. If, now, T|-K' [B]
holds when we assume T|-K' [A] in any consistent
extension K' of K, then, if we assume that there is a sequence <[A1], [A2],
..., [Am]>
of well-formed K'-formulas such that [Am]
is [A] and, for each m >= i >= 1, either [Ai]
is an axiom of K', or [Ai]
is in T, or [Ai]
is a direct consequence by some rules of inference of K' of some of the
preceding well-formed formulas in the sequence, then we
can show, by induction on the deduction length n, that there is a sequence <[B1],
[B2], ..., [Bn]> of well-formed K-formulas such that [B1]
is [A][8], [Bn] is [B] and, for each i > 1, either [Bi] is an axiom of K, or [Bi] is in T, or [Bi] is a direct consequence by some rules of inference
of K of some of the preceding well-formed formulas in the sequence.
Hence,
if there is a deduction <[A1], [A2],
..., [Am]>
of [A] from T in K', then <[A1], [A2],
..., [Am], [B2],
..., [Bn]>
is a deduction of [B] from T in K'. By definition, it follows
that <[B2], ..., [Bn]> is a deduction of [B] from (T, [A])
in K. We thus have: if T|-K [B] holds when we assume
T|-K [A], then (T, [A])|-K [B]. This completes
the proof. ¶
In view
of Corollary 1.2, we thus have:
Corollary 2.1: If we assume
Church’s Thesis, and if [A] is a closed well-formed formula of K, then
we may conclude T|-K ([A] => [B]) if T|-K
[B] holds when we assume T|-K [A].[9]
We note
that, in the notation of Corollary 1.1, if
the Gödel-number of the well-formed K-formula [A] is a, then Corollary 2.1
holds if, and only if[10]:
Corollary 2.2: ((Ex)xB(K, T)a => (Eu)uB(K, T)b) => (Ez)zB(K, T)c.
4. Conclusion
Since
standard interpretations of Gödel’s reasoning and conclusions do not admit Theorem 2 as a valid inference, such interpretations
are inconsistent with the standard Deduction Theorem for an arbitrary first
order theory [Me64], p61, Proposition 2.4);
they cannot, therefore, be considered definitive.
[An02a] Anand, B. S.
2002. Reviewing
Gödel’s and Rosser’s meta-reasoning of undecidability. (Web essay)
<Preprint: http://alixcomsi.com/Constructivity_consider.htm>
[An02b] Anand, B. S.
2002. Omega-inconsistency in
Gödel’s formal system: a constructive proof of the Entscheidungsproblem.
(Web essay)
<Preprint: http://alixcomsi.com/CTG_00.htm>
[An02c] Anand, B. S.
2002. Some
consequences of a recursive number-theoretic relation that is not the standard interpretation
of any of its formal representations.
(Web essay)
<Preprint:
http://alixcomsi.com/CTG_06_Consequences.htm>
[An02d] Anand,
B. S. 2002. Is
a deterministic universe logically consistent with a probabilistic Quantum
Theory? (Web essay)
<Preprint:
http://alixcomsi.com/CTG_08_Quantum_consistency1.htm>
[An03a] Anand,
B. S. 2003. Is
there a duality in the classical acceptance of non-constructive, foundational,
concepts as axiomatic? (Web essay)
<Preprint: http://alixcomsi.com/CTG_06_Consequences_Bringsjord.htm>
[An03b] Anand,
B. S. 2003. Three beliefs
that lend illusory legitimacy to Cantor’s diagonal argument? (Web
essay)
<Preprint:
http://alixcomsi.com/Three_beliefs.htm>
[An03c] Anand,
B. S. 2003. Is there a
“loophole” in Gödel’s interpretation of his formal reasoning and its
consequences? (Web essay)
<Preprint: http://alixcomsi.com/Is_there_a_loophole.htm>
[An03d] Anand, B. S.
2003. Can Turing
machines capture everything we can compute? (Web essay)
<Preprint:
http://alixcomsi.com/Can_Turing_machines.htm>
[An03e] Anand, B. S.
2003. The
formal roots of Platonism (Web essay)
<Preprint: http://alixcomsi.com/The_formal_roots_of_Platonism.htm>
[An03f] Anand,
B. S. 2003. Can we express every transfinite
concept constructively? (Web
essay)
<Preprint: http://alixcomsi.com/Can_we_express_every_transfinite.htm>
[An03g] Anand, B. S. 2003. Is the Halting probability a
Dedekind real number? (Web
essay)
<Preprint:
http://alixcomsi.com/Is_the_Halting_probability.htm>
[An03h] Anand, B. S. 2003. Why we must heed Wittgenstein’s “notorious
paragraph”. (Web
essay)
<Preprint: http://alixcomsi.com/Why_we_must_heed.htm>
[Br93] Bringsjord,
S. 1993. The
Narrational Case Against Church's Thesis. Easter APA meetings,
<Web
page: http://www.rpi.edu/~brings/SELPAP/CT/ct/ct.html>
[Bu01] Budnik, Paul P. Jr. 2001. What is and what will be -
Integrating spirituality and science. Mountain Math Software,
<Preprint:
http://www.mtnmath.com/whatth/whatth.html>
[Ca01] Calude,
Cristian S., Calude, Elena, and Marcus, Solomon. 2001. Passages of Proof.
Workshop, Annual Conference of the Australasian Association of Philosophy (
<PDF
file: http://arXiv.org/abs/math.
HO/ 0305213>
[Da95]
<PDF
file: http://citeseer.nj.nec.com/davis90is.html>
[FP00] Floyd,
Juliet., Putnam, Hilary. 2000. A Note on Wittgenstein's ‘Notorious
Paragraph’ about the Gödel Theorem. The Journal of Philosophy 45,
11: 624-632.
<PDF file: http://staff.washington.edu/dalexand/Putnam%20Readings/Notorious.pdf>
[Go31a] Gödel,
Kurt. 1931. On formally undecidable propositions of Principia Mathematica
and related
[Go31b] Gödel, Kurt.
1931. On formally
undecidable propositions of Principia Mathematica and related systems I. Translated by B. Meltzer.
<Web
page: http://home.ddc.net/ygg/etext/godel/index.htm>
[Ha47] Hardy, G.H.
1947, 9th ed. Pure Mathematics.
[Ho00] Hodges, A.
2000. Uncomputability
in the work of Alan Turing and Roger Penrose.
<Unpublished
lecture: http://www.turing.org.uk/philosophy/lecture1.html>
[Ka59] Kalmár, L.
1959. An Argument Against the Plausibility of Church's Thesis. In
Heyting, A. (ed.) Constructivity in Mathematics. North-Holland,
[Kl36]
[La51] Landau,
E.G.H. 1951. Foundations of Analysis. Chelsea Publishing Co.,
[Me64] Mendelson,
Elliott. 1964. Introduction to Mathematical Logic. Van Norstrand,
[Me90] Mendelson, E.
1990. Second Thoughts About Church's Thesis and Mathematical Proofs.
Journal of Philosophy 87.5.
[Pe90] Penrose, R.
1990 (Vintage edition). The Emperor's
New Mind: Concerning Computers, Minds and the Laws of Physics.
[Pe94] Penrose, R.
1994. Shadows of the Mind: A Search for the Missing Science of Consciousness.
[Po01] Podnieks,
Karlis. 2001. Around Goedel's Theorem.
<e-Textbook:
http://www.ltn.lv/~podnieks/gt.html>
[RH01]
<
Web page: http://psy.ucsd.edu/chip/ramapubs.html>
[Ru53] Rudin,
Walter. 1953. Principles of Mathematical Analysis.
[Ti61] Titchmarsh,
E. C. 1961. The Theory of Functions.
[Tu36] Turing,
Alan. 1936. On
computable numbers, with an application to the Entscheidungsproblem.
Proceedings of the
<Web
version: http://www.abelard.org/turpap2/tp2-ie.asp#index>
[Wi78] Wittgenstein,
Ludwig. (1978 edition). Remarks on the Foundations of Mathematics. MIT Press,
Acknowledgement:
My thanks to
Author’s e-mail:
anandb@vsnl.com
(Updated: Saturday 5th June 2004 3:26:39
AM IST by re@alixcomsi.com)
◄ Index ▲ Top of page
