Email Gateway (Aug 22 2022 at 13:44): Email Gateway (Aug 22 2022 at 13:44):From: Ken Kubota <mail@kenkubota.de>
Dear Members of the Research Community,
After a very fruitful debate with Russell O'Connor (who provided the proof of
Goedel's First Incompleteness Theorem in Coq) I would like to correct and
update some of my earlier publications.
Also, with the kind permission of Russell O'Connor, his definitions for
carrying out Goedel's First Incompleteness Theorem in Peter B. Andrews' logic
Q0, an improved variant of Church's type theory, including a sample proof for a
case of theorem V, are attached at the end of this e-mail. Andrews' logic Q0 is
specified in [Andrews, 2002, pp. 210-215; Andrews, 1986, pp. 161-165]. A short
description is available online at [Andrews, 2014]:
http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/#ForBasEqu
Finally, a comparison of the proofs of Goedel's First Incompleteness Theorem by
Russell O'Connor (in Coq) and Lawrence C. Paulson (in Isabelle) is undertaken
in order to foster the understanding of the proof. The type system implemented
by O'Connor is particularly well suited for demonstrating the three different
language levels in the proof.
Kind regards,
Ken Kubota
I. Corrections
The critique of a presentation of Goedel's First Incompleteness Theorem in
my 2013 article [Kubota, 2013] applies to that particular presentation only,
but not to the original publication of Goedel's First Incompleteness Theorem
[Gödel, 1931]. Since the work with the criticized presentation is a standard
work on higher-order logic, and the author of that work is usually extremely
precise and accurate, I did not expect the criticized presentation to
substantially differ from Goedel's original proof.
The hypothesis in my 2015 article [Kubota, 2015] that there is a significant
difference in the results between axiomatic (Hilbert-style) deductive systems
(called "object logics" in the article) and natural deduction systems (called
"meta-logics" in the article) cannot be upheld.
In summary, although some presentations of Goedel's First Incompleteness
Theorem fail, this doesn't seem to apply to Goedel's original proof, nor does
it apply to the formalized (mechanized) proofs provided by Russell O'Connor (in
Coq) and others. The result of the formal proof can be interpreted in the sense
that there is a formula (having the form of a sentence) that is neither
provable nor refutable, but calling this "incompleteness" depends on a specific
philosophical view, the semantic approach (model theory). If one doesn't share
the semantic view, Goedel's theorem, although it seems formally correct,
doesn't have the philosophical relevance often associated with it.
II. Summary of the Proof
a) Goedel begins with the introduction of a number of definitions supposed to
represent the form of a mathematical proof using mathematical (arithmetic)
means, up to the last definition "Bew" (for "beweisbare Formel", i.e.,
"provable formula").
b) In theorem V, Goedel shows that each relation R (with the property of being
primitive recursive) is definable within the logistic system by syntactical
means (i.e., provability) only, in other words, for each R, there is an r (with
the free variables u_1, ..., u_n), such that
R(x_1, ..., x_n) -> Bew( Sb(r, u_1, Z(x_1), ..., u_n, Z(x_n)) )
where Z is the numeral function, which returns the number in the language of
the embedded language when supplying a (natural) number of the logistic system
in which the proof is undertaken.
The proof is of a rather technical nature and quite lengthy, and,
unfortunately, in his presentation Goedel only sketched the idea. For an
example, see the attached presentation by Russell O'Connor.
c) Newer presentations refer to a fixed-point theorem called the diagonal lemma
(or diagonalization lemma), which is rather implicit in Goedel's original
proof. It can be used to construe a formula with the form of a sentence (a
boolean-valued well-formed formula with no free variables) g of the embedded
language, such that (simplified)
~Bew(g)
and
~Bew(not g).
For an excellent introduction to the diagonal lemma, see [Raatikainen, 2015],
available online at
http://plato.stanford.edu/archives/spr2015/entries/goedel-incompleteness/sup2.html
In order to use the least amount of prerequisites, one may consider Goedel's
proof of the (simplified) formula
~Bew(g) /\ ~Bew(not g)
as a purely formal proof, where the definition of "Bew" is simply an
abbreviation of a more complex number-theoretic well-formed formula.
However, for establishing the philosophical meaning associated with Goedel's
First Incompleteness Theorem, namely incompleteness, two philosophical
assumptions are necessary.
The first philosophical assumption is the correspondence of the definitions up
to "Bew" with the form of mathematical proofs. Although it is obvious that the
definitions do establish a proper representation of mathematical proofs, this
fact goes beyond the formal part. For example, a proof verification system (or
proof assistant) may prove
~Bew(g) /\ ~Bew(not g)
as a formal theorem, showing that, given the definitions, this theorem can be
obtained. But the software does not verify whether the definitions actually
match the form of mathematical proofs; this task is left to the reader. Goedel
himself emphasizes that the definability of (primitive) recursive relations in
the system P is expressed by theorem V "_without_ reference to any
interpretation of the formulas of P" [Gödel, 1931, p. 606, emphasis in the
original].
Goedel speaks of yielding "an isomorphic image of the system PM in the domain
of arithmetic, and all metamathematical arguments can just as well be carried
out in this isomorphic image." [Gödel, 1931, p. 597, fn. 9] The isomorphism
itself, however, can only be seen from top, from the meta-perspective, i.e.,
from outside of the logistic system in which the proof is undertaken. A direct
reference of the formal system to its own propositions is not possible.
Accordingly, O'Connor distinguishes between a Goedel quote function and a
Goedel numbering (or encoding) function, saying that propositions are "opaque".
The Goedel numbering (or encoding) function "G isn't a function from
propositions to natural numbers. It is supposed to be a function from
syntactic formulas to natural numbers and the type of syntactic formulas is
completely different from the type of propositions. Computations over
syntactic formulas can inspect the intension[al] structure of the formula, but
propositions are opaque and no such computation is possible." [Russell
O'Connor, e-mail to Ken Kubota, February 8, 2016]
The same consideration was made by the author when mentioning the
"non-definability of the Goedel encoding function" previously at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-January/msg00029.html
By verifying the definitions (which is not a purely mathematical / formal task)
one then can reasonably state that "Bew" can be interpreted as "provable", and
that there is a formula with the form of a sentence (a proposition with no free
variables) that is neither provable nor refutable.
Assuming
1. the correctness of the formal proof, and
2. the correctness of the definitions,
the result obtained so far is that a well-formed formula exists, or more
specifically, a formula of the form of an arithmetic proposition exists, which
can neither be proven nor refuted.
Following the semantic approach, according to which meaning is obtained by an
interpretation in some kind of meta-theory, either "g" or "not g" must be true,
hence there must be a true but unprovable theorem. This discrepancy between
syntax (provability) and semantics (truth, meaning) is what is commonly called
"incompleteness".
The implicit assumption made here and not discussed in the original publication
of Goedel's First Incompleteness Theorem in [Gödel, 1931] is the use of the
semantic approach (also called model-theoretic approach). In his completeness
essay published a year earlier, Goedel already makes use of the model-theoretic
approach in which semantic evaluation is performed by substitution at a
meta-level, without explicitly pointing out the use of a specific philosophical
assumption: "A formula of this kind is said to be valid (tautological) if a
true proposition results from every substitution of specific propositions and
functions for X, Y, Z, ... and F(x), G(x,y), ..., respectively [...]." [Gödel,
1930, p. 584, fn. 3]
In order to speak of "incompleteness", an expectation of "completeness" is
necessary, which is generally defined as the provability of all true
propositions. Hence, incompleteness is only possible if semantics (meaning)
differs from syntax, as is the case with model theory (the semantic approach).
But the semantic approach itself is a specific philosophical view and not
inherent in mathematics. If one, like the author, does not share the semantic
approach, but a purely syntactic approach, such that meaning in mathematics is
obtained by syntactical inference only (and the few rules of inference have
their legitimation in philosophy, outside of formal logic and mathematics),
then by definition there is no distinction between syntax and semantics.
In summary, if one assumes the philosophical assumption of the semantic
approach, then there is mathematical (arithmetic) incompleteness. But if one
doesn't, Goedel's First Incompleteness Theorem only shows that there is a
formula with the form of a well-formed (arithmetic) proposition which is
neither provable nor refutable, but may also be considered meaningless. Not
every well-formed formula (proposition) necessarily has to have a meaning, if
one doesn't follow the semantic approach. "Mathematics is liquid" is
grammatically corre
[message truncated]
Last updated: Apr 19 2024 at 12:27 UTC