Systems of Logic Based on Ordinals

Last updated

Systems of Logic Based on Ordinals was the PhD dissertation of the mathematician Alan Turing. [1] [2]

Turing's thesis is not about a new type of formal logic, nor was he interested in so-called "ranked logic" systems derived from ordinal or relative numbering, in which comparisons can be made between truth-states on the basis of relative veracity. Instead, Turing investigated the possibility of resolving the Gödelian incompleteness condition using Cantor's method of infinites.

The thesis is an exploration of formal mathematical systems after Gödel's theorem. Gödel showed that for any formal system S powerful enough to represent arithmetic, there is a theorem G that is true but the system is unable to prove. G could be added as an additional axiom to the system in place of a proof. However this would create a new system S' with its own unprovable true theorem G', and so on. Turing's thesis looks at what happens if you simply iterate this process repeatedly, generating an infinite set of new axioms to add to the original theory, and even goes one step further in using transfinite recursion to go "past infinity", yielding a set of new theories Gα, one for each ordinal number α.

The thesis was completed at Princeton under Alonzo Church and was a classic work in mathematics that introduced the concept of ordinal logic. [3]

Martin Davis states that although Turing's use of a computing oracle is not a major focus of the dissertation, it has proven to be highly influential in theoretical computer science, e.g. in the polynomial-time hierarchy. [4]

Related Research Articles

In mathematics, specifically set theory, the continuum hypothesis is a hypothesis about the possible sizes of infinite sets. It states that

there is no set whose cardinality is strictly between that of the integers and the real numbers,

In computability theory, the Church–Turing thesis is a thesis about the nature of computable functions. It states that a function on the natural numbers can be calculated by an effective method if and only if it is computable by a Turing machine. The thesis is named after American mathematician Alonzo Church and the British mathematician Alan Turing. Before the precise definition of computable function, mathematicians often used the informal term effectively calculable to describe functions that are computable by paper-and-pencil methods. In the 1930s, several independent attempts were made to formalize the notion of computability:

<span class="mw-page-title-main">Kurt Gödel</span> Mathematical logician and philosopher (1906–1978)

Kurt Friedrich Gödel was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel profoundly influenced scientific and philosophical thinking in the 20th century, building on earlier work by Richard Dedekind, Georg Cantor and Gottlob Frege.

Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal systems of logic such as their expressive or deductive power. However, it can also include uses of logic to characterize correct mathematical reasoning or to establish foundations of mathematics.

In complexity theory and computability theory, an oracle machine is an abstract machine used to study decision problems. It can be visualized as a Turing machine with a black box, called an oracle, which is able to solve certain problems in a single operation. The problem can be of any complexity class. Even undecidable problems, such as the halting problem, can be used.

In computability theory, a system of data-manipulation rules is said to be Turing-complete or computationally universal if it can be used to simulate any Turing machine. This means that this system is able to recognize or decide other data-manipulation rule sets. Turing completeness is used as a way to express the power of such a data-manipulation rule set. Virtually all programming languages today are Turing-complete.

Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of provability in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of mathematics. The theorems are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible.

Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since expanded to include the study of generalized computability and definability. In these areas, computability theory overlaps with proof theory and effective descriptive set theory.

Hypercomputation or super-Turing computation is a set of hypothetical models of computation that can provide outputs that are not Turing-computable. For example, a machine that could solve the halting problem would be a hypercomputer; so too would one that could correctly evaluate every statement in Peano arithmetic.

Proof theory is a major branch of mathematical logic and theoretical computer science within which proofs are treated as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of a given logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.

<span class="mw-page-title-main">George Boolos</span> American philosopher and mathematical logician

George Stephen Boolos was an American philosopher and a mathematical logician who taught at the Massachusetts Institute of Technology.

The year 1938 in science and technology involved some significant events, listed below.

In mathematics, a proof of impossibility is a proof that demonstrates that a particular problem cannot be solved as described in the claim, or that a particular set of problems cannot be solved in general. Such a case is also known as a negative proof, proof of an impossibility theorem, or negative result. Proofs of impossibility often are the resolutions to decades or centuries of work attempting to find a solution, eventually proving that there is no solution. Proving that something is impossible is usually much harder than the opposite task, as it is often necessary to develop a proof that works in general, rather than to just show a particular example. Impossibility theorems are usually expressible as negative existential propositions or universal propositions in logic.

Gentzen's consistency proof is a result of proof theory in mathematical logic, published by Gerhard Gentzen in 1936. It shows that the Peano axioms of first-order arithmetic do not contain a contradiction, as long as a certain other system used in the proof does not contain any contradictions either. This other system, today called "primitive recursive arithmetic with the additional principle of quantifier-free transfinite induction up to the ordinal ε0", is neither weaker nor stronger than the system of Peano axioms. Gentzen argued that it avoids the questionable modes of inference contained in Peano arithmetic and that its consistency is therefore less controversial.

In the mathematical discipline of set theory, there are many ways of describing specific countable ordinals. The smallest ones can be usefully and non-circularly expressed in terms of their Cantor normal forms. Beyond that, many ordinals of relevance to proof theory still have computable ordinal notations. However, it is not possible to decide effectively whether a given putative ordinal notation is a notation or not ; various more-concrete ways of defining ordinals that definitely have notations are available.

The history of the Church–Turing thesis ("thesis") involves the history of the development of the study of the nature of functions whose values are effectively calculable; or, in more modern terms, functions whose values are algorithmically computable. It is an important topic in modern mathematical theory and computer science, particularly associated with the work of Alonzo Church and Alan Turing.

A timeline of mathematical logic; see also history of logic.

In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. The halting problem is undecidable, meaning that no general algorithm exists that solves the halting problem for all possible program–input pairs.

In mathematics, ordinal logic is a logic associated with an ordinal number by recursively adding elements to a sequence of previous logics. The concept was introduced in 1938 by Alan Turing in his PhD dissertation at Princeton in view of Gödel's incompleteness theorems.

References

  1. ↑ Turing, Alan (1938). Systems of Logic Based on Ordinals (PhD thesis). Princeton University. doi:10.1112/plms/s2-45.1.161. hdl: 21.11116/0000-0001-91CE-3 . ProQuest   301792588.
  2. ↑ Turing, A. M. (1939). "Systems of Logic Based on Ordinals". Proceedings of the London Mathematical Society : 161–228. doi:10.1112/plms/s2-45.1.161. hdl: 21.11116/0000-0001-91CE-3 .
  3. ↑ Solomon Feferman, Turing in the Land of O(z) in "The universal Turing machine: a half-century survey" by Rolf Herken 1995 ISBN   3-211-82637-8 page 111
  4. ↑ Martin Davis "Computability, Computation and the Real World", in Imagination and Rigor edited by Settimo Termini 2006 ISBN   88-470-0320-2 pages 63-66
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.