In
mathematical logic
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 ...
,
computational complexity theory
In theoretical computer science and mathematics, computational complexity theory focuses on classifying computational problems according to their resource usage, and relating these classes to each other. A computational problem is a task solved ...
, and
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includi ...
, the existential theory of the reals is the set of all true sentences of the form
where the variables
are interpreted as having
real number
In mathematics, a real number is a number that can be used to measure a ''continuous'' one-dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Every ...
values, and where
is a
quantifier-free formula
In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language. A formal language can b ...
involving equalities and inequalities of real
polynomial
In mathematics, a polynomial is an expression consisting of indeterminates (also called variables) and coefficients, that involves only the operations of addition, subtraction, multiplication, and positive-integer powers of variables. An example ...
s. A sentence of this form is true if it is possible to find values for all of the variables that, when substituted into formula
, make it become true.
[.]
The
decision problem
In computability theory and computational complexity theory, a decision problem is a computational problem that can be posed as a yes–no question of the input values. An example of a decision problem is deciding by means of an algorithm wheth ...
for the existential theory of the reals is the problem of finding an
algorithm
In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...
that decides, for each such sentence, whether it is true or false. Equivalently, it is the problem of testing whether a given
semialgebraic set
In mathematics, a semialgebraic set is a subset ''S'' of ''Rn'' for some real closed field ''R'' (for example ''R'' could be the field of real numbers) defined by a finite sequence of polynomial equations (of the form P(x_1,...,x_n) = 0) and ine ...
is non-empty.
This decision problem is
NP-hard and lies in
PSPACE
In computational complexity theory, PSPACE is the set of all decision problems that can be solved by a Turing machine using a polynomial amount of space.
Formal definition
If we denote by SPACE(''t''(''n'')), the set of all problems that can b ...
.
Thus it has significantly lower complexity than
Alfred Tarski
Alfred Tarski (, born Alfred Teitelbaum;School of Mathematics and Statistics, University of St Andrews ''School of Mathematics and Statistics, University of St Andrews''. January 14, 1901 – October 26, 1983) was a Polish-American logician a ...
's
quantifier elimination Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. Informally, a quantified statement "\exists x such that \ldots" can be viewed as a question "When is there an x such t ...
procedure for deciding statements in the
first-order theory of the reals without the restriction to existential quantifiers.
However, in practice, general methods for the first-order theory remain the preferred choice for solving these problems.
Many natural problems in
geometric graph theory
Geometric graph theory in the broader sense is a large and amorphous subfield of graph theory, concerned with graphs defined by geometric means. In a stricter sense, geometric graph theory studies combinatorial and geometric properties of geome ...
, especially problems of recognizing geometric
intersection graph
In graph theory, an intersection graph is a graph that represents the pattern of intersections of a family of sets. Any graph can be represented as an intersection graph, but some important special classes of graphs can be defined by the types o ...
s and straightening the edges of
graph drawing
Graph drawing is an area of mathematics and computer science combining methods from geometric graph theory and information visualization to derive two-dimensional depictions of graphs arising from applications such as social network analysis, car ...
s with
crossings, may be solved by translating them into instances of the existential theory of the reals, and are
complete
Complete may refer to:
Logic
* Completeness (logic)
* Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable
Mathematics
* The completeness of the real numbers, which implies t ...
for this theory. The
complexity class
In computational complexity theory, a complexity class is a set (mathematics), set of computational problems of related resource-based computational complexity, complexity. The two most commonly analyzed resources are time complexity, time and spa ...
, which lies between
NP and PSPACE, has been defined to describe this class of problems.
Background
In
mathematical logic
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 ...
, a
theory
A theory is a rational type of abstract thinking about a phenomenon, or the results of such thinking. The process of contemplative and rational thinking is often associated with such processes as observational study or research. Theories may be ...
is a
formal language
In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules.
The alphabet of a formal language consists of sy ...
consisting of a set of
sentences
''The Four Books of Sentences'' (''Libri Quattuor Sententiarum'') is a book of theology written by Peter Lombard in the 12th century. It is a systematic compilation of theology, written around 1150; it derives its name from the '' sententiae'' ...
written using a fixed set of symbols. The
first-order theory of real closed fields has the following symbols:
*the constants 0 and 1,
*a countable collection of variables
,
*the addition, subtraction, multiplication, and (optionally) division operations,
*symbols <, ≤, =, ≥, >, and ≠ for comparisons of real values,
*the
logical connective
In logic, a logical connective (also called a logical operator, sentential connective, or sentential operator) is a logical constant. They can be used to connect logical formulas. For instance in the syntax of propositional logic, the binary ...
s ∧, ∨, ¬, and ⇔,
*parentheses, and
*the
universal quantifier ∀ and the
existential quantifier
In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". It is usually denoted by the logical operator symbol ∃, which, w ...
∃
A sequence of these symbols forms a sentence that belongs to the first-order theory of the reals if it is grammatically well formed, all its variables are properly quantified, and (when interpreted as a mathematical statement about the
real number
In mathematics, a real number is a number that can be used to measure a ''continuous'' one-dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Every ...
s) it is a true statement. As Tarski showed, this theory can be described by an
axiom schema In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom.
Formal definition
An axiom schema is a formula in the metalanguage of an axiomatic system, in which one or more schematic variables ap ...
and a decision procedure that is complete and effective: for every fully quantified and grammatical sentence, either the sentence or its negation (but not both) can be derived from the axioms. The same theory describes every
real closed field
In mathematics, a real closed field is a field ''F'' that has the same first-order properties as the field of real numbers. Some examples are the field of real numbers, the field of real algebraic numbers, and the field of hyperreal numbers.
D ...
, not just the real numbers.
However, there are other number systems that are not accurately described by these axioms; in particular, the theory defined in the same way for
integer
An integer is the number zero (), a positive natural number (, , , etc.) or a negative integer with a minus sign ( −1, −2, −3, etc.). The negative numbers are the additive inverses of the corresponding positive numbers. In the languag ...
s instead of real numbers is
undecidable, even for existential sentences (
Diophantine equations) by
Matiyasevich's theorem.
The existential theory of the reals is the subset of the first-order theory consisting of sentences in which all the quantifiers are existential and they appear before any of the other symbols. That is, it is the set of all true sentences of the form
where
is a
quantifier-free formula
In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language. A formal language can b ...
involving equalities and inequalities of
real
Real may refer to:
Currencies
* Brazilian real (R$)
* Central American Republic real
* Mexican real
* Portuguese real
* Spanish real
* Spanish colonial real
Music Albums
* ''Real'' (L'Arc-en-Ciel album) (2000)
* ''Real'' (Bright album) (2010) ...
polynomial
In mathematics, a polynomial is an expression consisting of indeterminates (also called variables) and coefficients, that involves only the operations of addition, subtraction, multiplication, and positive-integer powers of variables. An example ...
s. The
decision problem
In computability theory and computational complexity theory, a decision problem is a computational problem that can be posed as a yes–no question of the input values. An example of a decision problem is deciding by means of an algorithm wheth ...
for the existential theory of the reals is the algorithmic problem of testing whether a given sentence belongs to this theory; equivalently, for strings that pass the basic syntactical checks (they use the correct symbols with the correct syntax, and have no unquantified variables) it is the problem of testing whether the sentence is a true statement about the real numbers. The set of
-tuples of real numbers
for which
is true is called a
semialgebraic set
In mathematics, a semialgebraic set is a subset ''S'' of ''Rn'' for some real closed field ''R'' (for example ''R'' could be the field of real numbers) defined by a finite sequence of polynomial equations (of the form P(x_1,...,x_n) = 0) and ine ...
, so the decision problem for the existential theory of the reals can equivalently be rephrased as testing whether a given semialgebraic set is nonempty.
In determining the
time complexity
In computer science, the time complexity is the computational complexity that describes the amount of computer time it takes to run an algorithm. Time complexity is commonly estimated by counting the number of elementary operations performed by t ...
of
algorithm
In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...
s for the decision problem for the existential theory of the reals, it is important to have a measure of the size of the input. The simplest measure of this type is the length of a sentence: that is, the number of symbols it contains.
However, in order to achieve a more precise analysis of the behavior of algorithms for this problem, it is convenient to break down the input size into several variables, separating out the number of variables to be quantified, the number of polynomials within the sentence, and the degree of these polynomials.
Examples
The
golden ratio
In mathematics, two quantities are in the golden ratio if their ratio is the same as the ratio of their sum to the larger of the two quantities. Expressed algebraically, for quantities a and b with a > b > 0,
where the Greek letter phi ( ...
may be defined as the
root
In vascular plants, the roots are the organs of a plant that are modified to provide anchorage for the plant and take in water and nutrients into the plant body, which allows plants to grow taller and faster. They are most often below the su ...
of the
polynomial
In mathematics, a polynomial is an expression consisting of indeterminates (also called variables) and coefficients, that involves only the operations of addition, subtraction, multiplication, and positive-integer powers of variables. An example ...
. This polynomial has two roots, only one of which (the golden ratio) is greater than one. Thus, the existence of the golden ratio may be expressed by the sentence
Because the golden ratio does exist, this is a true sentence, and belongs to the existential theory of the reals. The answer to the decision problem for the existential theory of the reals, given this sentence as input, is the Boolean value true.
The
inequality of arithmetic and geometric means
In mathematics, the inequality of arithmetic and geometric means, or more briefly the AM–GM inequality, states that the arithmetic mean of a list of non-negative real numbers is greater than or equal to the geometric mean of the same list; and ...
states that, for every two non-negative numbers
and
, the following inequality holds:
As stated above, it is a first-order sentence about the real numbers, but one with universal rather than existential quantifiers, and one that uses extra symbols for division, square roots, and the number 2 that are not allowed in the first-order theory of the reals. However, by squaring both sides it can be transformed into the following existential statement that can be interpreted as asking whether the inequality has any counterexamples:
:
The answer to the decision problem for the existential theory of the reals, given this sentence as input, is the Boolean value false: there are no counterexamples. Therefore, this sentence does not belong to the existential theory of the reals, despite being of the correct grammatical form.
Algorithms
Alfred Tarski
Alfred Tarski (, born Alfred Teitelbaum;School of Mathematics and Statistics, University of St Andrews ''School of Mathematics and Statistics, University of St Andrews''. January 14, 1901 – October 26, 1983) was a Polish-American logician a ...
's method of
quantifier elimination Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. Informally, a quantified statement "\exists x such that \ldots" can be viewed as a question "When is there an x such t ...
(1948) showed the existential theory of the reals (and more generally the first order theory of the reals) to be algorithmically solvable, but without an
elementary
Elementary may refer to:
Arts, entertainment, and media Music
* ''Elementary'' (Cindy Morgan album), 2001
* ''Elementary'' (The End album), 2007
* ''Elementary'', a Melvin "Wah-Wah Watson" Ragin album, 1977
Other uses in arts, entertainment, a ...
bound on its complexity.
[.] The method of
cylindrical algebraic decomposition
In mathematics, cylindrical algebraic decomposition (CAD) is a notion, and an algorithm to compute it, that are fundamental for computer algebra and real algebraic geometry. Given a set ''S'' of polynomials in R''n'', a cylindrical algebraic decom ...
, by
George E. Collins
George E. Collins (January 10, 1928 in Stuart, Iowa – November 21, 2017 in Madison, Wisconsin) was an American mathematician and computer scientist. He is the inventor of Garbage collection (computer science), garbage collection by reference co ...
(1975), improved the time dependence to
doubly exponential,
of the form
where
is the number of bits needed to represent the coefficients in the sentence whose value is to be determined,
is the number of polynomials in the sentence,
is their total degree, and
is the number of variables.
[.]
By 1988,
Dima Grigoriev and Nicolai Vorobjov had shown the complexity to be exponential in a polynomial of
,
and in a sequence of papers published in 1992 James Renegar improved this to a singly exponential dependence
In the meantime, in 1988,
John Canny
John F. Canny (born in 1958) is an Australian computer scientist, and '' Paul E Jacobs and Stacy Jacobs Distinguished Professor of Engineering'' in the Computer Science Department of the University of California, Berkeley. He has made significant ...
described another algorithm that also has exponential time dependence, but only polynomial space complexity; that is, he showed that the problem could be solved in
PSPACE
In computational complexity theory, PSPACE is the set of all decision problems that can be solved by a Turing machine using a polynomial amount of space.
Formal definition
If we denote by SPACE(''t''(''n'')), the set of all problems that can b ...
.
The
asymptotic computational complexity In computational complexity theory, asymptotic computational complexity is the usage of asymptotic analysis for the estimation of computational complexity of algorithms and computational problems, commonly associated with the usage of the big O no ...
of these algorithms may be misleading, because in practice they can only be run on inputs of very small size. In a 1991 comparison, Hoon Hong estimated that Collins' doubly exponential procedure would be able to solve a problem whose size is described by setting all the above parameters to 2, in less than a second, whereas the algorithms of Grigoriev, Vorbjov, and Renegar would instead take more than a million years.
In 1993, Joos, Roy, and Solernó suggested that it should be possible to make small modifications to the exponential-time procedures to make them faster in practice than cylindrical algebraic decision, as well as faster in theory. However, as of 2009, it was still the case that general methods for the first-order theory of the reals remained superior in practice to the singly exponential algorithms specialized to the existential theory of the reals.
[.]
Complete problems
Several problems in computational complexity and
geometric graph theory
Geometric graph theory in the broader sense is a large and amorphous subfield of graph theory, concerned with graphs defined by geometric means. In a stricter sense, geometric graph theory studies combinatorial and geometric properties of geome ...
may be classified as
complete
Complete may refer to:
Logic
* Completeness (logic)
* Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable
Mathematics
* The completeness of the real numbers, which implies t ...
for the existential theory of the reals. That is, every problem in the existential theory of the reals has a
polynomial-time many-one reduction
In computational complexity theory, a polynomial-time reduction is a method for solving one problem using another. One shows that if a hypothetical subroutine solving the second problem exists, then the first problem can be solved by transforming ...
to an instance of one of these problems, and in turn these problems are reducible to the existential theory of the reals.
A number of problems of this type concern the recognition of
intersection graph
In graph theory, an intersection graph is a graph that represents the pattern of intersections of a family of sets. Any graph can be represented as an intersection graph, but some important special classes of graphs can be defined by the types o ...
s of a certain type. In these problems, the input is an
undirected graph
In discrete mathematics, and more specifically in graph theory, a graph is a structure amounting to a set of objects in which some pairs of the objects are in some sense "related". The objects correspond to mathematical abstractions called '' ve ...
; the goal is to determine whether geometric shapes from a certain class of shapes can be associated with the vertices of the graph in such a way that two vertices are adjacent in the graph if and only if their associated shapes have a non-empty intersection. Problems of this type that are complete for the existential theory of the reals include
recognition of
intersection graph
In graph theory, an intersection graph is a graph that represents the pattern of intersections of a family of sets. Any graph can be represented as an intersection graph, but some important special classes of graphs can be defined by the types o ...
s of
line segments in the plane,
recognition of
unit disk graph
In geometric graph theory, a unit disk graph is the intersection graph of a family of unit disks in the Euclidean plane. That is, it is a graph with one vertex for each disk in the family, and with an edge between two vertices whenever the corr ...
s,
and recognition of intersection graphs of convex sets in the plane.
For graphs drawn in the plane without crossings,
Fáry's theorem
In the mathematical field of graph theory, Fáry's theorem states that any simple, planar graph can be drawn without crossings so that its edges are straight line segments. That is, the ability to draw graph edges as curves instead of as straigh ...
states that one gets the same class of
planar graphs regardless of whether the edges of the graph are drawn as straight line segments or as arbitrary curves. But this equivalence does not hold true for other types of drawing. For instance, although the
crossing number of a graph (the minimum number of crossings in a drawing with arbitrarily curved edges) may be determined in NP, it is complete for the existential theory of the reals to determine whether there exists a drawing achieving a given bound on the rectilinear crossing number (the minimum number of pairs of edges that cross in any drawing with edges drawn as straight line segments in the plane).
It is also complete for the existential theory of the reals to test whether a given graph can be drawn in the plane with straight line edges and with a given set of edge pairs as its crossings, or equivalently, whether a curved drawing with crossings can be straightened in a way that preserves its crossings.
Other complete problems for the existential theory of the reals include:
* the
art gallery problem
The art gallery problem or museum problem is a well-studied visibility problem in computational geometry. It originates from the following real-world problem:
In the geometric version of the problem, the layout of the art gallery is represented ...
of finding the smallest number of points from which all points of a given polygon are visible.
* training neural networks.
* the
packing problem
Packing problems are a class of optimization problems in mathematics that involve attempting to pack objects together into containers. The goal is to either pack a single container as densely as possible or pack all objects using as few conta ...
of deciding whether a given set of polygons can fit in a given square container.
* recognition of
unit distance graph
In mathematics, particularly geometric graph theory, a unit distance graph is a graph formed from a collection of points in the Euclidean plane by connecting two points whenever the distance between them is exactly one. To distinguish these gra ...
s, and testing whether the
dimension
In physics and mathematics, the dimension of a mathematical space (or object) is informally defined as the minimum number of coordinates needed to specify any point within it. Thus, a line has a dimension of one (1D) because only one coor ...
or Euclidean dimension of a graph is at most a given value.
[.]
* stretchability of pseudolines (that is, given a family of curves in the plane, determining whether they are
homeomorphic to a
line arrangement);
* both weak and strong satisfiability of geometric
quantum logic
In the mathematical study of logic and the physical analysis of quantum foundations, quantum logic is a set of rules for manipulation of propositions inspired by the structure of quantum theory. The field takes as its starting point an observ ...
in any fixed dimension >2;
* Model checking interval Markov chains with respect to unambiguous automata.
* the algorithmic
Steinitz problem (given a
lattice
Lattice may refer to:
Arts and design
* Latticework, an ornamental criss-crossed framework, an arrangement of crossing laths or other thin strips of material
* Lattice (music), an organized grid model of pitch ratios
* Lattice (pastry), an orna ...
, determine whether it is the face lattice of a
convex polytope), even when restricted to 4-dimensional polytopes;
[.][.]
* realization spaces of arrangements of certain convex bodies
* various properties of
Nash equilibria
In game theory, the Nash equilibrium, named after the mathematician John Nash, is the most common way to define the solution of a non-cooperative game involving two or more players. In a Nash equilibrium, each player is assumed to know the equili ...
of multi-player games
[.][.][.]
* embedding a given abstract complex of triangles and quadrilaterals into three-dimensional Euclidean space;
[.]
* embedding multiple graphs on a shared vertex set into the plane so that all the graphs are drawn without crossings;
* recognizing the
visibility graph In computational geometry and robot motion planning, a visibility graph is a graph of intervisible locations, typically for a set of points and obstacles in the Euclidean plane. Each node in the graph represents a point location, and each edge rep ...
s of planar point sets;
* (projective or non-trivial affine) satisfiability of an equation between two terms over the
cross product;
* determining the minimum
slope number
In graph drawing and geometric graph theory, the slope number of a graph is the minimum possible number of distinct slopes of edges in a drawing of the graph in which vertices are represented as points in the Euclidean plane and edges are represe ...
of a non-crossing drawing of a
planar graph;
* recognizing
graphs that can be drawn with all crossings at right angles;
* the partial evaluation problem for the MATLANG+eigen matrix query language.
* the low-rank
matrix completion
Matrix completion is the task of filling in the missing entries of a partially observed matrix, which is equivalent to performing data imputation in statistics. A wide range of datasets are naturally organized in matrix form. One example is the mo ...
problem.
[.]
Based on this, the
complexity class
In computational complexity theory, a complexity class is a set (mathematics), set of computational problems of related resource-based computational complexity, complexity. The two most commonly analyzed resources are time complexity, time and spa ...
has been defined as the set of problems having a polynomial-time many-one reduction to the existential theory of the reals.
[.]
See also
*
Hilbert's tenth problem
Hilbert's tenth problem is the tenth on the list of mathematical problems that the German mathematician David Hilbert posed in 1900. It is the challenge to provide a general algorithm which, for any given Diophantine equation (a polynomial equa ...
, on the (undecidable) existential theory of the integers
References
{{reflist, colwidth=30em
Formal theories of arithmetic
Computational complexity theory
Real algebraic geometry