In
computability theory
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 ...
Post's theorem, named after
Emil Post
Emil Leon Post (; February 11, 1897 – April 21, 1954) was an American mathematician and logician. He is best known for his work in the field that eventually became known as computability theory.
Life
Post was born in Augustów, Suwałki Gover ...
, describes the connection between the
arithmetical hierarchy
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy (after mathematicians Stephen Cole Kleene and Andrzej Mostowski) classifies certain sets based on the complexity of formulas that define th ...
and the
Turing degree
In computer science and mathematical logic the Turing degree (named after Alan Turing) or degree of unsolvability of a set of natural numbers measures the level of algorithmic unsolvability of the set.
Overview
The concept of Turing degree is fun ...
s.
Background
The statement of Post's theorem uses several concepts relating to
definability and
recursion theory
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 ...
. This section gives a brief overview of these concepts, which are covered in depth in their respective articles.
The
arithmetical hierarchy
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy (after mathematicians Stephen Cole Kleene and Andrzej Mostowski) classifies certain sets based on the complexity of formulas that define th ...
classifies certain sets of natural numbers that are definable in the language of Peano arithmetic. A
formula
In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwe ...
is said to be
if it is an existential statement in
prenex normal form
A formula of the predicate calculus is in prenex normal form (PNF) if it is written as a string of quantifiers and bound variables, called the prefix, followed by a quantifier-free part, called the matrix. Together with the normal forms in propo ...
(all quantifiers at the front) with
alternations between existential and universal quantifiers applied to a formula with
bounded quantifier
In the study of formal theories in mathematical logic, bounded quantifiers (a.k.a. restricted quantifiers) are often included in a formal language in addition to the standard quantifiers "∀" and "∃". Bounded quantifiers differ from "∀" and " ...
s only. Formally a formula
in the language of Peano arithmetic is a
formula if it is of the form
:
where
contains only
bounded quantifier
In the study of formal theories in mathematical logic, bounded quantifiers (a.k.a. restricted quantifiers) are often included in a formal language in addition to the standard quantifiers "∀" and "∃". Bounded quantifiers differ from "∀" and " ...
s 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
In computability theory, a Turing reduction from a decision problem A to a decision problem B is an oracle machine which decides problem A given an oracle for B (Rogers 1967, Soare 1987). It can be understood as an algorithm that could be used to s ...
to a set
, written
, if there is an
oracle Turing machine that, given an oracle for
, computes the
characteristic function In mathematics, the term "characteristic function" can refer to any of several distinct concepts:
* The indicator function of a subset, that is the function
::\mathbf_A\colon X \to \,
:which for a given subset ''A'' of ''X'', has value 1 at point ...
of
.
The
Turing jump
In computability theory, the Turing jump or Turing jump operator, named for Alan Turing, is an operation that assigns to each decision problem a successively harder decision problem with the property that is not decidable by an oracle machin ...
of a set
is a form of the
Halting problem
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. Alan Turing proved in 1936 that a g ...
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:
#A set
is
if and only if
is
recursively enumerable
In computability theory, a set ''S'' of natural numbers is called computably enumerable (c.e.), recursively enumerable (r.e.), semidecidable, partially decidable, listable, provable or Turing-recognizable if:
*There is an algorithm such that the ...
by an oracle Turing machine with an oracle for
, that is, if and only if
is
.
#The set
is
-complete for every
. This means that every
set is
many-one reducible
In computability theory and computational complexity theory, a many-one reduction (also called mapping reduction) is a reduction which converts instances of one decision problem L_1 into instances of a second decision problem L_2 where the instan ...
to
.
Post's theorem has many corollaries that expose additional relationships between the arithmetical
hierarchy and the Turing degrees. These include:
#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
.
#A set
is
if and only if
. More generally,
is
if and only if
.
#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
A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algo ...
on input
can be formalized logically in
first-order arithmetic
In first-order logic, a first-order theory is given by a set of axioms in some
language. This entry lists some of the more common examples used in model theory and some of their properties.
Preliminaries
For every natural mathematical structur ...
. For example, we may use
symbol
A symbol is a mark, sign, or word that indicates, signifies, or is understood as representing an idea, object, or relationship. Symbols allow people to go beyond what is known or seen by creating linkages between otherwise very different con ...
s
,
, and
for the tape configuration, machine state and location along the tape after
steps, respectively.
's
transition system
In theoretical computer science, a transition system is a concept used in the study of computation. It is used to describe the potential behavior of discrete systems. It consists of states and transitions between states, which may be labeled wit ...
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
In first-order logic, a first-order theory is given by a set of axioms in some
language. This entry lists some of the more common examples used in model theory and some of their properties.
Preliminaries
For every natural mathematical structur ...
with no un
bounded quantifier
In the study of formal theories in mathematical logic, bounded quantifiers (a.k.a. restricted quantifiers) are often included in a formal language in addition to the standard quantifiers "∀" and "∃". Bounded quantifiers differ from "∀" and " ...
s, 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:
*
is the 1-
ary ARY may stand for:
* Abdul Razzak Yaqoob, a Pakistani expatriate businessman
* Andre Romelle Young, real name of Dr. Dre
* Ary and the Secret of Seasons, an action adventure video game
* ARY Digital, a Pakistani television network
* ARY Digital N ...
symbol
A symbol is a mark, sign, or word that indicates, signifies, or is understood as representing an idea, object, or relationship. Symbols allow people to go beyond what is known or seen by creating linkages between otherwise very different con ...
for the configuration of the whole tape after
steps (which we may write as a number with
LSB first, the value of the m-th location on the tape being its m-th least significant bit). In particular
is the initial configuration of the tape, which corresponds the input to the machine.
*
is the 1-
ary ARY may stand for:
* Abdul Razzak Yaqoob, a Pakistani expatriate businessman
* Andre Romelle Young, real name of Dr. Dre
* Ary and the Secret of Seasons, an action adventure video game
* ARY Digital, a Pakistani television network
* ARY Digital N ...
symbol for the Turing machine state after
steps. In particular,
, the initial state of the Turing machine.
*
is the 1-
ary ARY may stand for:
* Abdul Razzak Yaqoob, a Pakistani expatriate businessman
* Andre Romelle Young, real name of Dr. Dre
* Ary and the Secret of Seasons, an action adventure video game
* ARY Digital, a Pakistani television network
* ARY Digital N ...
symbol for the Turing machine location on the tape after
steps. In particular
.
*
is the transition function of the Turing machine, written as a function from a doublet (machine state, bit read by the machine) to a triplet (new machine state, bit written by the machine, +1 or -1 machine movement along the tape).
*
is the j-th bit of a number
. This can be written as a first-order arithmetic formula with no unbounded quantifiers.
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