In the year 1900 the German Mathematician David Hilbert gave a curious address in Paris, at the meeting of the 2nd International Congress of Mathematicians - he titled his address "Mathematical Problems". In it, he emphasized the importance of taking on challenging problems for maintaining the progress and development of mathematics. The problems numbered 1, 2, and 10 which concern mathematical logic and which gave birth to what is called the entscheidungsproblem or the decision problem were eventually solved though in the negative by Alonzo Church and Alan Turing in their famous Church-Turing thesis. The later Turing and Gumanski's attempts are criticized as inadequate or doubtful. So the decision problem is still unsolved in the positive. This book provides a positive solution using what the author calls the General Theory of Effectively Provable Function (GEP). Tremendous insights on computer development and evolution also come to light in this research. Obviously, this book is an audacious attempt to solve a problem that has lasted for more than a century and defied the best minds of logic's greatest era!
PROOF IN ALONZO CHURCH'S AND ALAN TURING'S MATHEMATICAL LOGIC
UNDECIDABILITY OF FIRST-ORDER LOGICBy Jonathan O. Chimakonam AuthorHouse
Copyright © 2012 Jonathan O. Chimakonam (Ph.D)
All right reserved.ISBN: 978-1-4772-8670-8 Contents
Chapter One: Introduction..................................................................................................................1Chapter Two: Literature Review.............................................................................................................14Chapter Three: Background To Proof Theory, Decision Problem And The Church-Turing Thesis...................................................52Chapter Four: Undecidability Of First Order Logic..........................................................................................101Chapter Five: Towards A Resolution Of The Decision Problem: The General Theory Of Effectively Provable Functions (GEP).....................111Chapter Six: General Assessment, Recommendation And Conclusion.............................................................................124Works Cited................................................................................................................................133
Chapter One
Introduction
1.1 Background to the Study
To start with, this dissertation cuts across philosophy of mathematics and mathematical logic. One of the relationships between the two is that mathematical logic functions as instrument to philosophy of mathematics through (1) model theory which, studies the relation between formal languages and extralinguistic structures and (2) proof theory which, studies formal languages by verifying the implication/ consequence relations. It is therefore in finding the possibility of evaluating the proven formulae that the decision problem is called in. The decision problem for logical implication hence asks; is there an effective method that when applied to any finite set of statement Γ and a statement D, will in finite time tell us whether or not Γ implies D? Church-Turing thesis has it that the decision problem for logical implication is unsolvable. To prove it, we reduce the decision problem for logic to the halting problem. We show that if it is solvable, then the halting problem (problem of constructing proofs in finite sequences) is solvable. Actually, what we prove is: given any fixed machine M and input n, there are Γ (a set of statements) and D (a statement) such that;
M halts on input n [equivalent to] Γ implies D.
In other words:
Γ [contains] D = M [??] n
In the year 1900 the German Mathematician David Hilbert gave a curious address in Paris, at the meeting of the 2nd International Congress of Mathematicians—an address which, was to have lasting fame and importance. The title of this lecture was simply, "Mathematical Problems". In it, he emphasized the importance of taking on challenging problems for maintaining the progress and vitality of mathematics. And with this he expressed a remarkable conviction in the solvability of all mathematical problems, which, he even called an axiom. In his words:
Is the axiom of the solvability of every problem a peculiar characteristic of mathematical thought alone, or is it possibly a general law inherent in the nature of the mind, that all questions which, it asks must be answerable? ... this conviction of the solvability of every mathematical problem is a powerful incentive to the worker. We hear within us the perpetual call: there is the problem. Seek its solution. You can find it by pure reason, for in mathematics there is no ignoramibus. (Hilbert 437)
Feferman notes that some of these problems, one after another had been solved in the past by mathematicians, though sometimes only after considerable effort and only over a period of many years. And Hilbert's own experience was that he could eventually solve any problem he turned to. But it was rather daring to assert that there are no limits to the power of human thought, at least in logic and mathematics. This has been put to question by some results in logic, notably, the undecidability of first-order-logic.
Hilbert's paper proposed a list of twenty-three problems which, ran the gamut of the fields of mathematics of his day, from the pure to the applied, and from the most general to the most specific. Feferman writes that:
In 1975, a conference was held under the title, "Mathematical Developments Arising from Hilbert Problems", which summarized the advances made on each of them to date. In many cases, the solutions obtained thus far led to still further problems which, were being pursued vigorously, though no longer with the cachet of having Hilbert's name attached. (2)
The solutions of three of Hilbert's problems were to involve mathematical logic and the foundations of mathematics in an essential way, and it is these that we are in this work concerned with. They are the problems numbered 1, 2 and 10 in his list but for reasons that you will see, we shall discuss them in reverse order (we quote Hilbert's own statement of the three problems in chapter three of this work where we discuss the overview of the "Decision problem").
Problem 10 called for an algorithm to determine of any given Diophantine equation whether or not it has any integer solutions. By Diophantine equations are meant equations expressed entirely in terms of integers and operations on integers, whose unknowns are also to be solved for integers. And by integers, of course, we mean the whole numbers 1, 2, 3 ... extended to include 0 and the negative integers -1, -2, -3, ...
Contrary to Hilbert's expectations, problem 10 was eventually solved in the negative. This was accomplished in 1970 by a young Russian mathematician, Yuri Matiyasevich, who built on earlier work in the 1950's and 1960's by the American logicians, Martin Davis, Hilary Putnam and Julia Robinson (Feferman 2). The result of the Davis-Putnam-Robinson-Matiyasevich work, as it is described nowadays, is that the general problem of the existence of integer solutions of Diophantine equations is algorithmically undecidable (Davis, Yuri and Robinson 323-378) (we explained the term undecidability under definition of terms in chapter one and variously in both chapter three and four of this work).
Hilbert's second problem called for a proof of consistency of the arithmetical axioms. Hilbert placed strong restrictions on the methods to be applied in consistency proofs of these and other axiom systems for mathematics: namely, these methods were to be completely finitary in character. In his words:
The axioms so set up are at the same time the definitions of these elementary ideas; and no statement within the realm of the science whose foundation we are testing is held to be correct unless it can be derived from those axioms by means of a finite number of logical steps. (Hilbert 439)
According to Feferman the proposal to obtain finitary consistency proofs of axiom systems for mathematics came to be called Hilbert's program or Hilbert's consistency program for the foundations of mathematics. Hilbert himself initiated specific work in the 1920s on his formulation of problem 2. Here again, against Hilbert's expectations, there was a negative solution, namely through the stunning results of the emerging Austrian logician Kurt Gödel, whose incompleteness theorems in 1931 have become one of the most famous in mathematical logic. Gödel showed that for any such system (and even much more elementary ones), there will always be individual propositions in its language that are undecidable by the system, i.e. which, can neither be proved nor disproved from its axioms provided it is consistent (Gödel 187). Even more, Gödel showed that the consistency of such a system cannot be proved within the system itself (188), and so finitary methods cannot suffice. Though these results apparently knocked down Hilbert's consistency program, several questions remain which, reach to the very foundation of our subject: is incompleteness an essential barrier to the process of discovery in mathematics or is there some way that it can be overcome? (Feferman 3). In answer to that, Feferman continues Gödel himself proposed one way forward, in fact, a way that connects up with Hilbert's first problem, as we will see later. Also, the English logician and pioneer computer-scientist Alan Turing as well as the American logician Alonzo Church proposed another way to overcome incompleteness that will be explained in detail since the theory of these two popularly known as the Church-Turing Thesis is the centre-piece of this work. A second important question is whether Hilbert's consistency program is still viable in any way, either by restricting its scope or by somehow enlarging the methods of proof to be admitted. Research are still on-going on both aspects of this question specifically by some logicians who believe that a set of formula ψ in a first-order-logic could be consistent θ and also decidable D i.e. (ψ [equivalent to] θ) [contains] D. Note that Gödel in his paper, "On Formally Undecidable Propositions of Principia Mathematica and Related Systems" (174-176) had proved that if a formal system is consistent, then the consistency of its axioms cannot be proved within it, hence the halting problem.
According to Feferman Hilbert's first problem which, is the most technical of the three, the reason why it is left for last, called for a proof of Cantor's conjecture on the cardinal number of the continuum of real numbers, the so-called continuum hypothesis. This is part of an aspect of logic called set theory and all presently generally accepted facts in set theory have been derived from principles which, have been codified in a specific system of axioms for this subject, called the Zermelo-Fraenkel axioms (Sutner 58) for set theory including what is called axiom of choice. So naturally, one would also seek to decide the continuum hypothesis on the basis of these axioms, i.e. either prove or disprove it from them. According to Solomon Feferman, the latter possibility was shown to be excluded by Gödel's second outstanding result, in 1938: he showed that the Zermelo-Franenkel axioms cannot disprove the continuum hypothesis (4). It was Paul Cohen in his Set Theory and the Continuum Hypothesis (17-85), who in 1966 obtained a major result that these same axioms cannot prove the continuum hypothesis. In other words, Cantor's conjecture is undecidable on the basis of currently accepted principles for set theory, provided, of course, that the Zermelo Fraenkel axioms are consistent. There was also a second part to Hilbert's first problem; in that he called for the construction of a specific well-ordering of the continuum. The axiom of choice, which, we here count among the Zermelo-Fraenkel axioms, implies that for any set there exists a well-ordering of that set, but it does not tell you how to construct one. Feferman showed using Cohen's method in his "Infinity in Mathematics: is Cantor Necessary?" (151-209) that it is consistent with the Zermelo-Fraenkel axioms plus the continuum hypothesis, that there is no definable well-ordering of the continuum. Again, contrary to Hilbert's expectations.
Returning to Cantor's continuum problem itself, the first question to ask following the undecidability results of Gödel and Cohen is whether that situation could change by adding further axioms for set theory in some reasonable way. As it turns out, according to Feferman, their results apply to all plausible (and even not so plausible) extensions that have been considered so far. There are sharply divergent views as to whether it is still hopeful to obtain a reasonable extension of the Zermelo-Fraenkel axioms which will settle the continuum hypothesis. And, as in any subject, we have both optimists and pessimists: the direction one leans may be a matter of basic differences of temperament, but in this case, we believe it really comes down to basic differences in one's philosophy of mathematics, namely, as to whether one thinks mathematics in general, and set theory in particular, is about some independently existing abstract, "platonic" reality, or whether it is somehow the objective part of human conceptions and constructions. The Platonists say the continuum hypothesis must have a definite answer and so for them it is still hopeful to find that out by some means or other. But according to some pessimists or anti-Platonists like Feferman (Deciding the Undecidable 4), the continuum hypothesis problem is an inherently vague or indefinite one, as are the propositions of higher set theory more generally. Anyhow, if one agrees that the continuum hypothesis does not constitute a genuine, definite, mathematical, and logical problems, then its undecidability relative to any given axioms ceases to be an issue with which, to struggle; it simply evaporates as a problem. In this research however, we take a stand against all those who see the continuum hypothesis problem as an inherently vague or indefinite one. As a problem we believe it can have an answer. Hence by inventing an additional axiom, we shall construct in this dissertation a general theory of proof which, will be able to solve in the positive most of, and yet to be discovered mathematical problems involving syntax and semantics.
In each of these three cases, what Hilbert apparently took to be a fairly definite problem for which, he expected a positive solution, the outcome not only led in the opposite direction, but also to the very foundations of our subject where the results connect with the questions whether there are any essential limits to the power of human reasoning and whether mathematics and logic are actually as impregnable as we think.
As Feferman notes, if someone comes along with a proposed algorithm to settle a given decision problem in a positive way, one can check to see that it does the required work (or at least, tries to do so), without inquiring into the general nature of what constitutes an algorithm. But if it is to be shown that the problem is undecidable, one has to have a precise explanation of what algorithms can compute in general. Analogous situations had arisen earlier in mathematics, for example, to show that there is no possible construction by straight edge and compass which, will trisect any given angle, or that there is no possible explicit formula for finding the roots of any polynomial equation (in one unknown) of degree 5 or higher (we do have such formulae for degrees, 1, 2, 3 and 4). In each of these cases, one first needs a precise characterization of everything that can be constructed or defined in the specified way, before showing that certain problems cannot be solved by such constructions or definitions.
In just the same way, in order to establish undecidability results, one first needed to have a precise characterization of what in general can be computed by an algorithm. Several very different looking answers to this were offered by logicians-among whom are Kurt Gödel, Alonzo Church, Alan Turing, Stephen Kleene, John Lucas, Roger Penrose, Martin Davis, Yuri Matiyasevich, E. Post and so on. However, the contributions of Alonzo Church and Alan Turing are the concern of this dissertation. Their theories were eventually shown to be equivalent together with that of Kurt Gödel. The most familiar explanation is that due to Turing, who described what can be done by an ideal computer if no restrictions are placed on how much time or memory space is required to carry out a given computation. These are called Turing machines nowadays, and Turing's conception is the foundation of theoretical computer science, at least of what can be computed in principle. In his paper, "On Computable Numbers, with an Application to the Entscheidungsproblem", Turing states:
I propose, therefore, to show that there can be no general process for determining whether a given formular U of the functional calculus Z is provable, i.e. that there can be no machine which, supplied with any one U of these formulae, will eventually say whether U is provable. (259)
In his own paper "An Unsolvable Problem of Elementary Number Theory" (345-363), Alonzo Church proposed a definition of the commonly used term "effective calculability" and showed on the basis of this definition that the general case of the entscheidungsproblem is unsolvable in any system of symbolic logic which, is inadequate to a certain portion of arithmetic and is consistent. While Kurt Gödel in his paper, "On Formally Undecidable Propositions of Principia Mathematica and Related Systems" has shown that (in the formalism of Principia Mathematica) there are propositions U such that neither U nor ~ U is provable. As a consequence of this, it is shown that no proof of consistency of Principia Mathematica (or of Z) can be given within that formalism (174-176). As he puts it:
... the conclusion seems plausible that these deduction rules (systems of Principia Mathematica PM and the Zermelo-Fraenkelian axiom-system of set theory) are sufficient to decide all mathematical questions expressible in those systems. We will show that this is not true, but that there are even relatively easy problems in the theory of ordinary whole numbers that cannot be decided from the axioms. (173)
The above excerpts give a backing to our initial statements that Hilbert's problems 1 and 2 were also solved in the negative and that the theories of Alonzo Church and Alan Turing which, are usually treated as one are equivalent with that of Kurt Gödel.
Both Church and Turing however, applied their characterization of what is algorithmically computable, to show that the decision problem for (what is called) first-order-logic is undecidable i.e. that no possible algorithm can be used to determine of any given proposition formulated in the symbolism of that logic whether or not it is universally valid.
Our concern in this dissertation therefore, is on the more traditional question: how can we formulate a broader algorithm within which, first-order-logic can be made decidable? In response we shall develop an axiom and attempt an articulation of what we shall call a general theory of effective provability which would be able to solve in the positive and in a finite logical steps, most mathematical and logical problems pertaining to both syntax and semantics.
1.2 Statement of the Problem
The decision problem as it concerns the first-order-logic has defied any positive solution for over a century now. The negative solution offered by Alonzo Church and Alan Turing in their Church-Turing thesis has overtime magnified the despair as to the possibility of a positive solution. Only recently, the research question has begun to shift from "how can we make first-order-logic decidable"? to "could it be that first-order-logic is absolutely undecidable?"
Thus, if at the highest and purest development of mathematical logic we discover a problem that undermines the very foundation upon which, the principles of our subject are laid, then it means that logic has yet to deliver on its promises of consistency, provability, solvability, justifiability, satisfiability, derivability and, of course, decidability. It is therefore the attempt to falsify the claim to absolute undecidability and to devise an algorithm within which, the decision problem could be solved in the positive that form the core of our research problem.
(Continues...)
Excerpted from PROOF IN ALONZO CHURCH'S AND ALAN TURING'S MATHEMATICAL LOGICby Jonathan O. Chimakonam Copyright © 2012 by Jonathan O. Chimakonam (Ph.D). Excerpted by permission of AuthorHouse. All rights reserved. No part of this excerpt may be reproduced or reprinted without permission in writing from the publisher.
Excerpts are provided by Dial-A-Book Inc. solely for the personal use of visitors to this web site.
