Microsoft Word goedel-duzi rtf
Yüklə 246,82 Kb. Pdf görüntüsü
|
- Bu səhifədəki naviqasiya:
- 4. Concluding remarks
- References
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
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(Sx))] → ∀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)
‘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
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.
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”.
Yüklə 246,82 Kb. Dostları ilə paylaş:
|