PROOF IN ALONZO CHURCH'S AND ALAN TURING'S MATHEMATICAL LOGIC

AuthorHouse

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

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...