Search

The aim of this paper is to review some basic ideas, concepts, and questions of today's theoretical biology and stimulate reflection on them. Possible sources of misunderstanding, confusion, and disagreement in the discussion of the foundation of biology are outlined. Major attention is given to different interpretations (and implications) of the term “explanation” and “living system.” It is argued that the concepts of present day's physics are not general enough to describe biology. As examples of possible new concepts “complexity” and “creativity” are discussed. Different definitions of “living systems” and their flaws are reviewed. It is concluded that an explanation of a living system involves both, an understanding of its parts and of the organization of these parts. This leads to a discussion of the role of quantum mechanics and non-equilibrium statistical thermodynamics in biology. Finally, the implications of some philosophical points of view and the role of Godel's incompleteness theorem in a basic theory of biology are discussed.

Publisher Summary This chapter introduces the definitions of the notion of a random sequence using the three main ideas described that have dominated algorithmic randomness. There are three key approaches for defining randomness in sequences: unpredictability, typicality, and incompressibility. A notion is set up notation for strings and sequences, the Cantor Space, which forms the basic framework for carrying out further discussions, and contains a brief and informal introduction to Lebesgue measure on the unit interval and the Cantor space, which one treats as equivalent. Discussion of mathematical randomness defines a series of classical stochastic or frequency properties in an effort to distill out randomness. This chapter further forms the core material on algorithmic randomness: Von Mises randomness, Martin-Lof randomness, Kolmogorov complexity and randomness of finite strings, application to Godel incompleteness, and Schnorr's theorem. It forms an overview of other forms of related randomness notions that have been studied and indicates the current state of affairs.

Hilbert's program was an ambitious and wide-ranging project in the philosophy and foundations of mathematics. In order to "dispose of the foundational questions in mathematics once and for all, "Hilbert proposed a two-pronged approach in 1921: first, classical mathematics should be formalized in axiomatic systems; second, using only restricted, "finitary" means, one should give proofs of the consistency of these axiomatic systems. Although Godel's incompleteness theorems show that the program as originally conceived cannot be carried out, it had many partial successes, and generated important advances in logical theory and meta-theory, both at the time and since. The article discusses the historical background and development of Hilbert's program, its philosophical underpinnings and consequences, and its subsequent development and influences since the 1930s.

Publisher Summary This chapter describes Kurt Godel's paper on the incompleteness theorems. Godel's incompleteness results are two of the most fundamental and important contributions to logic and the foundations of mathematics. It had been assumed that first-order number theory is complete in the sense that any sentence in the language of number theory would be either provable from the axioms or refutable. Godel's first incompleteness theorem showed that this assumption was false: it states that there are sentences of number theory that are neither provable nor refutable. The first theorem is general in the sense that it applies to any axiomatic theory, which is ω-consistent, has an effective proof procedure, and is strong enough to represent basic arithmetic. Their importance lies in their generality: although proved specifically for extensions of system, the method Godel used is applicable in a wide variety of circumstances. Godel's results had a profound influence on the further development of the foundations of mathematics. It pointed the way to a reconceptualization of the view of axiomatic foundations.

Publisher Summary In the book Grundlagen Der Mathematik, Hilbert and Bernays systematically present their proof-theoretic investigations and a wide range of current results, such as Herbrand's theorems and Godel's incompleteness theorems. Some specialized topics are also discussed, such as the development of mathematical analysis and the unsolvability of the decision problem. Hilbert changed his basic attitude towards consistency proofs only around 1903 after the discovery of the elementary contradiction of Russell and Zermelo, which convinced him that there was a deep problem. The formalism F and the numbering are required to satisfy roughly two representability conditions: primitive recursive arithmetic is “contained in” F; and the syntactic properties and relations of F's expressions, as well as the processes that can be carried out on such expressions, are given by primitive recursive predicates and functions. Finally, it is to consider the stimulus his approach and questions provided to contemporaries outside the Hilbert school. There is no foundational enterprise with a more profound and far-reaching effect on the emergence and development of mathematical logic.

This chapter discusses the characteristics of the algorithms, the future of the art of optimization, and approaches to the problems. Although many managers might wish it otherwise, the writing of efficient computer programs will always be an art, not a science. Clarke's Law states that if a distinguished elderly scientist says that something is possible, he is almost always right; if he says that something is impossible, he is almost always wrong. As demonstrated by Goedel's Proof, no automatic procedure can discover all of the true statements in a consistent axiomatic system such as the behavior of a programmable computer. This implies that the development of new algorithms will always be an adventure. Software engineers, however, have a fundamentally different situation: Once solved a given problem, one should never need to solve it again, as one can reuse the solution already developed. In the development projects, one is always venturing into unexplored territory and one knows how to identify pioneers. On the other hand, the thought of going into the office to face the same problems every day would greatly reduce interest in this field.

Publisher Summary Godel's second incompleteness theorem can be obtained by purely proof-theoretic methods. This chapter describes Godel and Lobian principles in an abstract setting, which allows simultaneous description of first-order theories, modal logics, and the self-referential systems. It introduces the notion of a provability function—a mapping from sentences to sentences satisfying the analogue of the Hilbert–Bernays conditions. The chapter also considers Kripke's argument and its modifications and describes the modal system K4. The discovery of several facts about K4 is greatly facilitated by use of a basic principle—the translational theorem. The proof of translation theorem for K4 and also for the modal system G is presented. This essentially allows getting new principles of K4 from known ones, which when translated into metamathematical terms, yieldnew Lobian-type constructions from known Godelian-type constructions. The chapter describes metamathematical applications of the results about K4.

Two new theories for the direct formalization of meta-mathematics are introduced, FM o and FM . They are second-order theories of a pairing structure whose class construction axioms are for elementary comprehension (ECA) and finitary inductive generation (FIG). ECA is restricted to positive existential formulas in FM o , making FM o = PRA while FM = PA . The closed class terms of FM o are called inductive presentations of classes. Godel's 2nd incompleteness theorem is established in a natural and canonical way in FM o for inductively presented extensions S of FM o . A good deal of countable model theory can be formalized in FM .

Publisher Summary This chapter investigates a reasonably natural theorem of finitary combinatorics, a simple extension of the Finite Ramsey Theorem. The chapter demonstrates that this theorem, while true, is not provable in Peano arithmetic. The chapter works extensively with the partition calculus. In the proof of the main theorem, the chapter relies on various proof-theoretic results, in particular, on Godel's Second Incompleteness Theorem. It is possible, however, to prove the main theorem using only model-theoretic methods. This is the approach where a general model-theoretic methodology (called indicator functions) for producing such results is developed.

Publisher Summary This chapter illustrates Godel incompleteness theorem and proves the existence of free formulas not only for systems based on the usual rules of proof but also for systems based on the rule ω. The chapter discusses the systems based on the rule ω rests on the basis of the remark of J. R. Shoenfield that the decomposition of the ∏11 sets into constituents can on several occasions be exploited in the same way as the recursive enumerability of the Σ01sets.

Publisher Summary This chapter discusses Hilbert's program, Godel's theorems, and formalized completeness theorem. It also discusses the encoding and some related topics followed by some generalizations of the Incompleteness Theorems. The concern is regarding metamathematical properties other than consistency. Further, two applications of the notions and results are presented in the chapter. The Incompleteness Theorems are obtained by formalizing Syntax. The chapter also discusses what happens when one formalizes Semantics. The chapter discusses the First Incompleteness Theorem and the Second Incompleteness Theorem and presents proof of the Incompleteness Theorems.

Publisher Summary This chapter focuses on Jaśkowski's discussive propositional calculus to a higher-order discussive logic and presents a new axiomatization of discussive propositional calculus that constitutes a solution to Problems I and II of Costa 1975. The discussive propositional calculus has a logical and mathematical importance by itself and has originated several interesting problems. In an axiomatization for the discussive propositional calculus the primitive connectives are: → (discussive implication), Λ (left discussive conjunction), V (disjunction), and ┐ (negation). The formulas of the discussive propositional calculus are constructed with propositional variables, the connectives and parentheses. In order to facilitate the writing of formulas, small Latin letters is employed as syntactical variables. The usual rules of the positive propositional logic are valid in the discussive propositional calculus. The chapter discusses the deduction theorem, Godel's incompleteness theorem, various other theorem, axiom schemata, derivatives rules, and various lemmas.

Publisher Summary This chapter focuses on the length of proofs of finitistic consistency statements in first order theories. By the second incompleteness theorem of Godel, a sufficiently rich theory cannot prove its own consistency. The most interesting application of the lower bound is a more than elementary speed-up for the length of proofs in the Godel-Bernays (GB) relative to Zermelo–Fraenkel (ZF). The chapter discusses the length of formulas into the complexity. It is assumed that the proofs are coded by strings in a finite alphabet and the length of a proof is the length of the corresponding string. This is the most realistic measure. The weakest fragment of arithmetic that is used is Robinson's arithmetic. The chapter proves the lower bound on the length of proofs of finitistic consistency statements.

It is suggested that the technical work that has led to the solution of Hilbert's tenth problem can advantageously be used in teaching the incompleteness theorem.

Publisher Summary This chapter discusses the Cut-Elimination Theorem for first-order logic. The proof of Cut-Elimination Theorem is set up in such a way that it can be easily generalized to many other cases where a cut-elimination argument is applied. The chapter also discusses the provability and unprovability of initial cases of transfinite induction for arithmetic Z. The result is well known: given a natural well-ordering ɛ 0 , with respect to ɛ 0 , but not up to ɛ 0 itself. The underivability in Z of transfinite induction up to ɛ 0 will also follow from Godel's Second Incompleteness Theorem, together with the fact that transfinite induction up to ɛ 0 suffices to prove the reflection principle for Z and hence the consistency of Z. A direct proof of this underivability result is presented using a cut-elimination argument. Technically, this provides an easy and convincing example of the usefulness of infinite derivations and the strength of the cut-elimination method when applied to infinite derivations.

This chapter focuses on Hilbert's program and Godel's incompleteness theorems. A consistency proof of any system is an absolute proof of consistency if the proof is based on no stronger assumptions than the assumption that S is consistent. Certain simpler theorems of logic, such as the consistency of any predicate calculus, can be used in an absolute proof of consistency. It was Hilbert who originally formulated the discipline of metamathematics, by which he meant the study of formal systems by weak, number-theoretic methods, and with the goal of giving an absolute consistency proof of a system in which all of mathematics can be deduced. Hilbert's goal was to justify certain nonconstructive principles of mathematics, such as the axiom of choice or definition by transfinite induction. Intuitionism can be schematically—though in a somewhat oversimplified way—described as the position that only number-theoretic methods are valid mathematical tools. The rest, intuitionists would assert, is just a fiction.

Publisher Summary The method of formalizing mathematical proofs gives rise to various formal systems in which certain methods of derivation are delimited in a natural way. Within some of these systems, the chapter is able to formalize all demonstrations of classical number theory, analysis, and set theory. From Godel's incompleteness theorems, it is know that there is no consistent formal system that allows to derive every true arithmetic formula. This can be expressed also by saying that the set of Godel numbers is not recursively enumerable. In a less technical formulation, the number-theoretic concept of truth cannot be operatively defined—that is, the true arithmetic propositions cannot be characterized as those obtained from some explicitly stated propositions and propositional schemata by some rules of procedure given in advance. A complete system (a system that cannot consistently be extended by adding an axiom, which is expressible as a formula of the system) can admit different nonisomorphic models.

Publisher Summary This chapter provides the formalization of the theory of ordinal diagrams of infinite order. There is a discussion about a formal theory of some systems of ordinal diagrams, which have been used to prove the consistency of subsystems of classical analysis. By exhibiting a formal system in which the consistency proofs can be formalized, Godel's incompleteness theorem can be used (in the form that no system can prove its own consistency) to form an estimate of what the limits are of the power of such methods. The chapter presents a formal system that is constructive. The intuitionistic arithmetic, that is, Peano's axioms plus primitive recursive definitions plus the intuitionistic predicate calculus are described. The properties of primitive recursive functions can be used and predicates freely in terms of mathematical axioms.

Publisher Summary This chapter discusses three syntactic relations—models, translations, and interpretations— between formal systems from the following points of view: (1) their relation to the consistency problem, (2) their relation to each other, and (3) some of their uses in understanding informal mathematics. The chapter discusses axiomatizable systems—that is, those whose axioms form a (general) recursive set, along with certain non-axiomatizable systems because they are better formalizations of such branches of mathematics as arithmetic and set theory. The systems in which these syntactic relations are established are mentioned explicitly. Both the use of non-axiomatizable systems and explicit mention of metamathematical methods of proof may be regarded as a natural reaction to Godel's incompleteness theorems which shows (1) that axiomatizable systems are not satisfactory approximations to certain branches of mathematics, (2) that various formalizations of these branches of mathematics are of different strength, so that one may expect to learn essentially more from the particular proofs of a theorem than from its assertion.

Publisher Summary This chapter discusses the ultra-intuitionistic criticism and the antitraditional program for foundations of mathematics. The program aims to banish faith from the foundations of mathematics, faith being defined as any violation of the law of sufficient reason (for sentences). This law is defined as the identification (by definition) of truth with the result of a (present or feasible) proof, in spite of the traditional incompleteness theorem, which deals with very narrow kinds of proofs. The methods of traditional mathematical logic are not sufficient for this program: and the domains of means that are explicitly studied in logic have to be enlarged. The rejection of the axiomatic method does not mean the expulsion of the axioms and rules of inference.

Publisher Summary This chapter discusses the principles of proof and ordinals implicit in given concepts. The process of recognizing the validity of such principles (including principles for defining new concepts, that is, formally, of extending a given language) is conceived in the chapter. The informal notions of proof plausible are studied. A number of proof theoretic methods are available. Godel's incompleteness theorem, with an absolute minimum of assumptions on the details of the distinction, shows the existence of theorems stated in elementary terms that do not have an elementary proof. The process of building up the integers by a successor operation, with the property that is distinct from x and from all y built up before x . This process determines an ordering between the integers, and hence an abstract order type.