20
a non-tautology of provability logic. Since
¬ False is a formula equivalent to False → False
(provable False implies False), this example also shows that the scheme A
→ A is not an
acceptable axiom scheme for provability logic. On the other hand, the formula
¬ False →
¬ ¬ False (“if a contradiction is not provable then the statement that a contradiction is
unprovable is unprovable”) is an example of a tautology of provability logic. Provability logic
was investigated in parallel by several researchers (in Amsterdam, Italy, U.S.A., Sweden). Its
arithmetical completeness theorem was proved by R. Solovay in 1975. Provability logic is
interesting for both mathematicians and philosophers; it combines metamathematical
investigations with modal-logical tools like Kripke semantics. Out of several papers dealing
with provability logic I can recommend Švejdar’s (2000), from which some explanations and
symbolism above are taken.
There are some extensions of provability logic obtained by employing additional
“modalities”. For example, interpretability logic uses, besides for “proves”, a binary
modality operator ► for “interprets”. It is designed for research on (syntactic) interpretability
of axiomatic theories. The concept of syntactic interpretability is distinct from the concept of
semantic interpretation introduced above. Slightly simplified, a theory T is said to be
interpretable in a theory S iff the language of T can be translated into the language of S in
such a way that S proves the translation of every theorem of T. Of course, there are some
natural conditions on admissible translations here, such as the necessity for a translation to
preserve the logical structure of formulas. This concept, together with weak interpretability,
was introduced by Alfred Tarski in 1953. However, intensive research has been pursued in
Prague; one of the important results that stimulated the interest in interpretability was Petr
Hájek’s observation that Zermelo-Fraenkel set theory ZF and Gödel-Bernays set theory GB,
though identical as to provability of set sentences, differ in interpretability.
Connections of Gödel theorems to interpretability logic are given by the following two
facts. First, there is a generalization of the Second Incompleteness Theorem saying that a
consistent theory T can interpret no theory S such that S is an extension of T and S proves
consistency of T. Second, if S proves consistency of T then S interprets T. This second fact
can be obtained by formalizing Gödel completeness theorem in S.
Now I would like to mention some properties of arithmetic models. From the
Compactness theorem
26
it can be easily derived that there are non-standard models
27
of a
recursively-formalized arithmetic. A non-standard model is one that constitutes a structural
interpretation of the formal theory that is admittedly different from the intended one. By
structural interpretation I mean interpretation where isomorphic models count as the same
interpretation.
The existence of non-standard models can be also derived from the stronger version of the
Completeness theorem. Roughly: a formula
ϕ is provable in a theory T iff ϕ is logically
entailed by its special axioms; T |=
ϕ iff T |– ϕ. Now the sentence ν is not provable in T,
hence
ν is not valid in every model of T. It is however valid in the standard model
N,
which
is a model of T. Every model isomorphic to
N
is also a model of T;
ν is however not valid in
every model of T. Hence T must have a non-standard model.
26
If a formula
ϕ is logically entailed by a theory T (T |= ϕ), then there is a finite subset F of T such that ϕ is
entailed by F (F |=
ϕ).
27
See a nice exposition on non-standard models by Haim Gaifman (2003)
21
From the point of view of capturing the intended interpretation, i.e., characterizing the set
of natural numbers completely, the existence of non-standard models counts as a failure of the
formal language to capture the semantics fully. The special axioms of the theory do not
“implicitly define” the intended model, the consistency problem becomes crucial. Ordinary
mathematical practice amounts to a study of the ‘intended interpretation’. But if mathematics
is not only a “science of quantity” but a fully formalized discipline that draws conclusions
logically implied by any given set of axioms, and if a mathematical inference in no sense
depends upon any special meaning that may be associated with the terms and formulas, the
question whether the given set of axioms is internally consistent so that no contradictory
theorems can be derived, becomes crucial. If the axioms are simultaneously true of some
sequences of numbers, they cannot be incompatible. But the models of arithmetic are
composed of infinite number of elements, which makes it impossible to encompass the
models in a finite number of observations; hence the truth of the axioms themselves is a
subject of doubt. Using the axiom of induction we can only check that a finite number of
objects are in the agreement with the axiom. But the conclusion involves an extrapolation
from a finite to an infinite set of objects. Hence Hilbert sought an ‘absolute’ proof of
consistency. Unfortunately no such absolute proof will ever be at hand.
You may pose another question: Which of the models is the standard one? Which
sequence of objects constitutes the subject matter of the inquiry, “what is it all about”? It can
be characterized by a minimality condition
28
: it is the smallest model, included as an initial
segment in any other model. If the model is non-standard, then it will be revealed by a proper
initial segment that is closed under the successor function. Formally, the characterization is
expressed by the inductive scheme:
(I)
[P(0) &
∀ x (N( x) → (P( x) → P(S x))] → ∀ x [N( x) → P( x)],
where N(x) stands for ‘x is a natural number’, and ‘P( )’ stands for any predicate. Any wff of
the language can be substituted for ‘P( )’. The concept of the natural number sequence is
however not language dependent. The absoluteness of the concept can be secured, if we help
ourselves to the standard power set of some infinite set; for then we can treat ‘P’ as a variable
ranging over that power set. In other words, we shift the system into the 2
nd
order. But this is
highly unsatisfactory. Quoting from Gaifman (2003):
[…] it bases the standard number sequence on the much more problematic shaky
concept of the standard power set. It is, to use a metaphor of Edward Nelson, like
establishing the credibility of a person through the evidence of a much less credible
character witness. The inductive scheme should be therefore interpreted as an open-
ended meta-commitment:
(II)
Any non-vague (crisp) predicate, in whatever language, can be substituted for
‘P’ in (I).
As Van McGee expresses it, if God himself creates a predicate, then this predicate can
be substituted for ‘P’. One, who has reservations about actual infinities, can still doubt
the conception of the standard number sequence, but these doubts do not gain
additional support from the existence of non-standard models.
The second-order theories (of real numbers, of complex numbers, and of Euclidean
geometry) do have complete axiomatizations. Hence these theories have no true but
unprovable sentences. The reason they escape the incompleteness is their inadequacy: they
can’t encode and computably deal with finite sequences. The price we pay for the 2
nd
-order
completeness is high; the second-order calculus is not (even partially) decidable. We cannot
28
Now I refer to H.Gaifman (2003).
22
algorithmically generate all the 2
nd
-order logical truths, thus not all the logical truths are
provable, the 2
nd
-order calculus is not semantically complete.
The consequences of Gödel’s two theorems are clear and generally accepted. First of all,
the formalist belief in identifying truth with provability is destroyed by the first
incompleteness theorem. Second, the impossibility of an absolute (acceptable from the finitist
point of view) consistency proof is even more destructive for Hilbert’s program. The second
Gödel’s theorem makes the notion of a finitist statement and finitist proof highly problematic.
If the notion of a finitist proof is identified with a proof formalized in an axiomatic theory T,
then the theory T is a very week theory. If T satisfies simple requirements, then T is suspected
of inconsistency. In other words, if the notion of finitist proof means something that is non-
trivial and at the same time non-questionable and consistent, there is no such thing.
Though it is almost universally believed that Gödel’s results destroyed Hilbert’s program,
the program was very inspiring for mathematicians, philosophers and logicians. Some
thinkers claimed that we should be formalists anyway
29
. Others, like Brouwer, the father of
modern constructive mathematics, believe that mathematics is first and foremost an activity:
mathematicians do not discover pre-existing things, as the Platonist holds and they do not
manipulate symbols, as the formalist holds. Mathematicians, according to Brouwer, make
things. Some recent intuitionists seem to stay somewhere in between: being ontological
realists they admit that there are abstract entities we discover in mathematics, but at the same
time being semantic intuitionists they claim that these abstract entities “do not exist” unless
they are well defined by a constructive
30
formal proof, as a sequence of judgements
31
.
Possible impact of Gödel’s results on the philosophy of mind, artificial intelligence, and
on Platonism might be a matter of dispute. Gödel himself suggested that the human mind
cannot be a machine and that Platonism is correct. Most recently Roger Penrose has argued
that “the Gödel’s results show that the whole programme of artificial intelligence is wrong,
that creative mathematicians do not think in a mechanic way, but that they often have a kind
of insight into the Platonic realm which exists independently from us”
32
. Gödel’s doubts about
the limits of formalism were certainly influenced by Brouwer who criticized formalism in the
lecture presented at the University of Vienna in 1928. Gödel however did not share Brouwer’s
intuitionism based on the assumption that mathematical objects are created by our activities.
For Gödel as a Platonic realist mathematical objects exist independently and we discover
them. On the other hand he claims that our intuition cannot be reduced to Hilbert’s concrete
intuition on finitary symbols, but we have to accept abstract concepts like well defined
mathematical procedures that have a clear meaning without further explication. His proofs
are constructive and therefore acceptable from the intuitionist point of view.
In fact, Gödel’s results are based on the two fundamental concepts: truth for formal
languages and effective computability. Concerning the former, Gödel stated in his lectures in
Princeton that he was led to the incompleteness of arithmetic via his recognition of the non-
definability of arithmetic truth in its own language. In the same lectures he offered the notion
of general recursiveness in connection with the idea of effective computability; this was based
on a modification of a definition proposed by Herbrand. In the meantime, Church was making
a proposal of his thesis, which identified the effectively computable functions with the
λ-
definable functions. Gödel was not convinced by Church’s thesis, because it was not based on
a conceptual analysis of the notion of finite algorithmic procedure. It was only when Turing,
29
See, e.g., Robinson, A. (1964) ‘Formalism 64’, or more recently Detlefsen, M. (1992) ‘On an Alleged
Refutation of Hilbert’s Program Using Gödel’s first incompleteness theorem’
30
The notion of constructive proof is central for intuitionistic logic.
31
The above is a slightly reformulated remark made by Peter Fletcher in an e-mail correspondence.
32
See, Brown (1999. p. 78)
23
in 1937, offered the definition in terms of his machines that Gödel was ready to accept the
identification of the various classes of functions:
λ-definable, general recursive, Turing
computable.
Pursuit of Hilbert’s program had thus an unexpected side effect: it gave rise to the realistic
research on the theory of recursive functions and algorithms. John Von Neumann, for
instance, along with being a great mathematician and logician, was an early pioneer in the
field of modern computing, though it was a difficult task because computing was not yet a
respected science. His conception of computer architecture has actually not been surpassed till
now. Gödel’s first theorem has another interpretation in the language of computer science. In
first-order logic, theorems are recursively enumerable: you can write a computer program that
will eventually generate any valid proof. You can ask if they satisfy the stronger property of
being recursive: can you write a computer program to definitively determine if a statement is
true or false? Gödel’s theorem says that in general you cannot; a computer can never be as
smart as a human being because the extent of its knowledge is limited by a fixed set of
axioms, whereas people can discover unexpected truths.
The greatness of a great thinker is measured by the influence his work has on future
generations. One can fairly say that Gödel’s results changed the face of meta-mathematics and
influenced all aspects of modern mathematics, artificial intelligence and philosophy of mind.
Marie Duží
VSB-Technical University Ostrava
Department of Computer Science FEI
17. listopadu 15
708 33 Ostrava
marie.duzi@vsb.cz
References
Brown, J. (1999): Philosophy of Mathematics. Routlege, London, New York.
Dawson, J.W. (1984): Kurt Gödel in Sharper Focus. The Mathematical Intelligencer, 4.
Feferman, S. (1960): Arithmetization of metamathematics in a general setting, Foundations of
Math., vol. 49, pp. 35-92.
Feferman, S., ed. (1986): Kurt Gödel: Collected Works. Oxford University Press.
Gaifman, H. (2003): Non-Standard Models in a Broader Perspective. Manuscript.
Hájek, P (1996): Matematik a logik. In Malina, Novotný.
Köhler, E. (1991): Gödel und der Wiener Kreis. In: Jour fixe der Vernunft, edited by
Kruntorad, P. with the aid of Haller, R. and Hochkeppel, W, Verlag Hölder-Pichler-
Tempsky, Vienna.
Köhler, E. (2002): Gödels Jahre in Princeton. In: Kurt Gödel. Wahrheit & Beweisbarkeit,
Volume I, edited by Köhler, E., Weibel, P., Stöltzner, M., Buldt, B., Klein, C.,
DePauli-Schimanovich-Göttig, W., Vienna.
Köhler, E. (2002a): Gödel’s Platonismus. In: Kurt Gödel. Wahrheit & Beweisbarkeit, Volume
II, edited by Buldt, B., Köhler, E., Stöltzner, M., Weibel, P., Klein, C., DePauli-
Schimanovich-Göttig, W. Vienna.
Malina, J.,
− Novotný, J., ed. (1996): Kurt Gödel. Nadace Universitas Masarykiana, Brno.
Mendelson, E. (1997): Introduction to Mathematical Logic. Chapman & Hall.
Nagel, E.
− Newman, J.R. (1958): Gödel‘s Proof. New York University Press.
24
Švejdar, V. (2000): On Provability Logic. Nordic Journal of Philosophical Logic, Vol. 4, No.
2, December 1999.
Švejdar, V. (2002): Logika, neúplnost, složitost a nutnost. Academia Praha.
Acknowledgements
I am deeply grateful to Vítězslav Švejdar for his valuable comments on the manuscript of the
paper, which improved the quality of the survey. Vítězslav also contributed the concluding
remarks on provability and interpretability logics. I am also grateful to Bjorn Jespersen and
Andrew Holster for their careful proof reading and improving the English, and to Eckehard
Köhler for providing relevant references.
This work has been supported by the program “Information Society” of the Czech Academy
of Sciences, project No. 1ET101940420 “Logic and Artificial Intelligence for multi-agent
systems”.
Dostları ilə paylaş: |