Post's theorem

Last updated

In computability theory Post's theorem, named after Emil Post, describes the connection between the arithmetical hierarchy and the Turing degrees.

Contents

Background

The statement of Post's theorem uses several concepts relating to definability and recursion theory. This section gives a brief overview of these concepts, which are covered in depth in their respective articles.

The arithmetical hierarchy classifies certain sets of natural numbers that are definable in the language of Peano arithmetic. A formula is said to be if it is an existential statement in prenex normal form (all quantifiers at the front) with alternations between existential and universal quantifiers applied to a formula with bounded quantifiers only. Formally a formula in the language of Peano arithmetic is a formula if it is of the form

where contains only bounded quantifiers and Q is if m is even and if m is odd.

A set of natural numbers is said to be if it is definable by a formula, that is, if there is a formula such that each number is in if and only if holds. It is known that if a set is then it is for any , but for each m there is a set that is not . Thus the number of quantifier alternations required to define a set gives a measure of the complexity of the set.

Post's theorem uses the relativized arithmetical hierarchy as well as the unrelativized hierarchy just defined. A set of natural numbers is said to be relative to a set , written , if is definable by a formula in an extended language that includes a predicate for membership in .

While the arithmetical hierarchy measures definability of sets of natural numbers, Turing degrees measure the level of uncomputability of sets of natural numbers. A set is said to be Turing reducible to a set , written , if there is an oracle Turing machine that, given an oracle for , computes the characteristic function of . The Turing jump of a set is a form of the Halting problem relative to . Given a set , the Turing jump is the set of indices of oracle Turing machines that halt on input when run with oracle . It is known that every set is Turing reducible to its Turing jump, but the Turing jump of a set is never Turing reducible to the original set.

Post's theorem uses finitely iterated Turing jumps. For any set of natural numbers, the notation indicates the fold iterated Turing jump of . Thus is just , and is the Turing jump of .

Post's theorem and corollaries

Post's theorem establishes a close connection between the arithmetical hierarchy and the Turing degrees of the form , that is, finitely iterated Turing jumps of the empty set. (The empty set could be replaced with any other computable set without changing the truth of the theorem.)

Post's theorem states:

  1. A set is if and only if is recursively enumerable by an oracle Turing machine with an oracle for , that is, if and only if is .
  2. The set is -complete for every . This means that every set is many-one reducible to .

Post's theorem has many corollaries that expose additional relationships between the arithmetical hierarchy and the Turing degrees. These include:

  1. Fix a set . A set is if and only if is . This is the relativization of the first part of Post's theorem to the oracle .
  2. A set is if and only if . More generally, is if and only if .
  3. A set is defined to be arithmetical if it is for some . Post's theorem shows that, equivalently, a set is arithmetical if and only if it is Turing reducible to for some m.

Proof of Post's theorem

Formalization of Turing machines in first-order arithmetic

The operation of a Turing machine on input can be formalized logically in first-order arithmetic. For example, we may use symbols , , and for the tape configuration, machine state and location along the tape after steps, respectively. 's transition system determines the relation between and ; their initial values (for ) are the input, the initial state and zero, respectively. The machine halts if and only if there is a number such that is the halting state.

The exact relation depends on the specific implementation of the notion of Turing machine (e.g. their alphabet, allowed mode of motion along the tape, etc.)

In case halts at time , the relation between and must be satisfied only for k bounded from above by .

Thus there is a formula in first-order arithmetic with no unbounded quantifiers, such that halts on input at time at most if and only if is satisfied.

Implementation example

For example, for a prefix-free Turing machine with binary alphabet and no blank symbol, we may use the following notations:

For a prefix-free Turing machine we may use, for input n, the initial tape configuration where cat stands for concatenation; thus is a length string of followed by and then by .

The operation of the Turing machine at the first steps can thus be written as the conjunction of the initial conditions and the following formulas, quantified over for all :

T halts on input at time at most if and only if is satisfied, where:

This is a first-order arithmetic formula with no unbounded quantifiers, i.e. it is in .

Recursively enumerable sets

Let be a set that can be recursively enumerated by a Turing machine. Then there is a Turing machine that for every in , halts when given as an input.

This can be formalized by the first-order arithmetical formula presented above. The members of are the numbers satisfying the following formula:

This formula is in . Therefore, is in . Thus every recursively enumerable set is in .

The converse is true as well: for every formula in with k existential quantifiers, we may enumerate the tuples of natural numbers and run a Turing machine that goes through all of them until it finds the formula is satisfied. This Turing machine halts on precisely the set of natural numbers satisfying , and thus enumerates its corresponding set.

Oracle machines

Similarly, the operation of an oracle machine with an oracle O that halts after at most steps on input can be described by a first-order formula , except that the formula now includes:

If the oracle is for a decision problem, is always "Yes" or "No", which we may formalize as 0 or 1. Suppose the decision problem itself can be formalized by a first-order arithmetic formula . Then halts on after at most steps if and only if the following formula is satisfied:

where is a first-order formula with no unbounded quantifiers.

Turing jump

If O is an oracle to the halting problem of a machine , then is the same as "there exists such that starting with input m is at the halting state after steps". Thus: where is a first-order formula that formalizes . If is a Turing machine (with no oracle), is in (i.e. it has no unbounded quantifiers).

Since there is a finite number of numbers m satisfying , we may choose the same number of steps for all of them: there is a number , such that halts after steps precisely on those inputs for which it halts at all.

Moving to prenex normal form, we get that the oracle machine halts on input if and only if the following formula is satisfied:

(informally, there is a "maximal number of steps" such every oracle that does not halt within the first steps does not stop at all; however, for every, each oracle that halts after steps does halt).

Note that we may replace both and by a single number - their maximum - without changing the truth value of . Thus we may write:

For the oracle to the halting problem over Turing machines, is in and is in . Thus every set that is recursively enumerable by an oracle machine with an oracle for , is in .

The converse is true as well: Suppose is a formula in with existential quantifiers followed by universal quantifiers. Equivalently, has > existential quantifiers followed by a negation of a formula in ; the latter formula can be enumerated by a Turing machine and can thus be checked immediately by an oracle for .

We may thus enumerate the tuples of natural numbers and run an oracle machine with an oracle for that goes through all of them until it finds a satisfaction for the formula. This oracle machine halts on precisely the set of natural numbers satisfying , and thus enumerates its corresponding set.

Higher Turing jumps

More generally, suppose every set that is recursively enumerable by an oracle machine with an oracle for is in . Then for an oracle machine with an oracle for , is in .

Since is the same as for the previous Turing jump, it can be constructed (as we have just done with above) so that in . After moving to prenex formal form the new is in .

By induction, every set that is recursively enumerable by an oracle machine with an oracle for , is in .

The other direction can be proven by induction as well: Suppose every formula in can be enumerated by an oracle machine with an oracle for .

Now Suppose is a formula in with existential quantifiers followed by universal quantifiers etc. Equivalently, has > existential quantifiers followed by a negation of a formula in ; the latter formula can be enumerated by an oracle machine with an oracle for and can thus be checked immediately by an oracle for .

We may thus enumerate the tuples of natural numbers and run an oracle machine with an oracle for that goes through all of them until it finds a satisfaction for the formula. This oracle machine halts on precisely the set of natural numbers satisfying , and thus enumerates its corresponding set.

Related Research Articles

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

<span class="mw-page-title-main">Original proof of Gödel's completeness theorem</span>

The proof of Gödel's completeness theorem given by Kurt Gödel in his doctoral dissertation of 1929 is not easy to read today; it uses concepts and formalisms that are no longer used and terminology that is often obscure. The version given below attempts to represent all the steps in the proof and all the important ideas faithfully, while restating the proof in the modern language of mathematical logic. This outline should not be considered a rigorous proof of the theorem.

<span class="mw-page-title-main">Ordered pair</span> Pair of mathematical objects

In mathematics, an ordered pair (a, b) is a pair of objects. The order in which the objects appear in the pair is significant: the ordered pair (a, b) is different from the ordered pair (b, a) unless a = b. (In contrast, the unordered pair {a, b} equals the unordered pair {b, a}.)

In classical deductive logic, a consistent theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if it has a model, i.e., there exists an interpretation under which all formulas in the theory are true. This is the sense used in traditional Aristotelian logic, although in contemporary mathematical logic the term satisfiable is used instead. The syntactic definition states a theory is consistent if there is no formula such that both and its negation are elements of the set of consequences of . Let be a set of closed sentences and the set of closed sentences provable from under some formal deductive system. The set of axioms is consistent when for no formula .

<span class="mw-page-title-main">Arithmetical hierarchy</span> Hierarchy of complexity classes for formulas defining sets

In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them. Any set that receives a classification is called arithmetical. The arithmetical hierarchy was invented independently by Kleene (1943) and Mostowski (1946).

In mathematical logic and descriptive set theory, the analytical hierarchy is an extension of the arithmetical hierarchy. The analytical hierarchy of formulas includes formulas in the language of second-order arithmetic, which can have quantifiers over both the set of natural numbers, , and over functions from to . The analytical hierarchy of sets classifies sets by the formulas that can be used to define them; it is the lightface version of the projective hierarchy.

In computational complexity theory, the polynomial hierarchy is a hierarchy of complexity classes that generalize the classes NP and co-NP. Each class in the hierarchy is contained within PSPACE. The hierarchy can be defined using oracle machines or alternating Turing machines. It is a resource-bounded counterpart to the arithmetical hierarchy and analytical hierarchy from mathematical logic. The union of the classes in the hierarchy is denoted PH.

<span class="mw-page-title-main">LSZ reduction formula</span> Connection between correlation functions and the S-matrix

In quantum field theory, the Lehmann–Symanzik–Zimmerman (LSZ) reduction formula is a method to calculate S-matrix elements from the time-ordered correlation functions of a quantum field theory. It is a step of the path that starts from the Lagrangian of some quantum field theory and leads to prediction of measurable quantities. It is named after the three German physicists Harry Lehmann, Kurt Symanzik and Wolfhart Zimmermann.

In computability theory, the Turing jump or Turing jump operator, named for Alan Turing, is an operation that assigns to each decision problem X a successively harder decision problem X with the property that X is not decidable by an oracle machine with an oracle for X.

Independence-friendly logic is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form and , where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic. This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second-order logic.

In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.

In complexity theory, the Karp–Lipton theorem states that if the Boolean satisfiability problem (SAT) can be solved by Boolean circuits with a polynomial number of logic gates, then

Effective descriptive set theory is the branch of descriptive set theory dealing with sets of reals having lightface definitions; that is, definitions that do not require an arbitrary real parameter. Thus effective descriptive set theory combines descriptive set theory with recursion theory.

In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.

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.

In constructive mathematics, Church's thesis is an axiom stating that all total functions are computable functions.

In computability theory, index sets describe classes of computable functions; specifically, they give all indices of functions in a certain class, according to a fixed Gödel numbering of partial computable functions.

In mathematical logic, true arithmetic is the set of all true first-order statements about the arithmetic of natural numbers. This is the theory associated with the standard model of the Peano axioms in the language of the first-order Peano axioms. True arithmetic is occasionally called Skolem arithmetic, though this term usually refers to the different theory of natural numbers with multiplication.

In first-order arithmetic, the induction principles, bounding principles, and least number principles are three related families of first-order principles, which may or may not hold in nonstandard models of arithmetic. These principles are often used in reverse mathematics to calibrate the axiomatic strength of theorems.

In set theory and logic, Buchholz's ID hierarchy is a hierarchy of subsystems of first-order arithmetic. The systems/theories are referred to as "the formal theories of ν-times iterated inductive definitions". IDν extends PA by ν iterated least fixed points of monotone operators.

References

Rogers, H. The Theory of Recursive Functions and Effective Computability, MIT Press. ISBN   0-262-68052-1; ISBN   0-07-053522-1

Soare, R. Recursively enumerable sets and degrees. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1987. ISBN   3-540-15299-7