Presburger arithmetic is the
first-order theory
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 quantif ...
of the
natural number
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called ''Cardinal n ...
s with
addition
Addition (usually signified by the Plus and minus signs#Plus sign, plus symbol ) is one of the four basic Operation (mathematics), operations of arithmetic, the other three being subtraction, multiplication and Division (mathematics), division. ...
, named in honor of
Mojżesz Presburger
Mojżesz Presburger, or Prezburger, (December 27, 1904 – 1943) was a Polish Jewish mathematician, logician, and philosopher. He was a student of Alfred Tarski, Jan Łukasiewicz, Kazimierz Ajdukiewicz, and Kazimierz Kuratowski. He is known fo ...
, who introduced it in 1929. The
signature
A signature (; from la, signare, "to sign") is a handwritten (and often stylized) depiction of someone's name, nickname, or even a simple "X" or other mark that a person writes on documents as a proof of identity and intent. The writer of a ...
of Presburger arithmetic contains only the addition operation and
equality
Equality may refer to:
Society
* Political equality, in which all members of a society are of equal standing
** Consociationalism, in which an ethnically, religiously, or linguistically divided state functions by cooperation of each group's elit ...
, omitting the
multiplication
Multiplication (often denoted by the cross symbol , by the mid-line dot operator , by juxtaposition, or, on computers, by an asterisk ) is one of the four elementary mathematical operations of arithmetic, with the other ones being additi ...
operation entirely. The axioms include a schema of
induction
Induction, Inducible or Inductive may refer to:
Biology and medicine
* Labor induction (birth/pregnancy)
* Induction chemotherapy, in medicine
* Induced stem cells, stem cells derived from somatic, reproductive, pluripotent or other cell t ...
.
Presburger arithmetic is much weaker than
Peano arithmetic
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
, which includes both addition and multiplication operations. Unlike Peano arithmetic, Presburger arithmetic is a
decidable theory. This means it is possible to algorithmically determine, for any sentence in the language of Presburger arithmetic, whether that sentence is provable from the axioms of Presburger arithmetic. The asymptotic running-time
computational complexity of this algorithm is at least
doubly exponential, however, as shown by .
Overview
The language of Presburger arithmetic contains constants 0 and 1 and a binary function +, interpreted as addition.
In this language, the axioms of Presburger arithmetic are the
universal closure
In mathematical logic, a universal quantification is a type of Quantification (logic), quantifier, a logical constant which is interpretation (logic), interpreted as "given any" or "for all". It expresses that a predicate (mathematical logic), pr ...
s of the following:
# ¬(0 = ''x'' + 1)
# ''x'' + 1 = ''y'' + 1 → ''x'' = ''y''
# ''x'' + 0 = ''x''
# ''x'' + (''y'' + 1) = (''x'' + ''y'') + 1
# Let ''P''(''x'') be a
first-order formula in the language of Presburger arithmetic with a free variable ''x'' (and possibly other free variables). Then the following formula is an axiom:(''P''(0) ∧ ∀''x''(''P''(''x'') → ''P''(''x'' + 1))) → ∀''y'' ''P''(''y'').
(5) is 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 ...
of
induction
Induction, Inducible or Inductive may refer to:
Biology and medicine
* Labor induction (birth/pregnancy)
* Induction chemotherapy, in medicine
* Induced stem cells, stem cells derived from somatic, reproductive, pluripotent or other cell t ...
, representing infinitely many axioms. These cannot be replaced by any finite number of axioms, that is, Presburger arithmetic is not finitely axiomatizable in first-order logic.
Presburger arithmetic can be viewed as a
first-order theory
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 quantif ...
with equality containing precisely all consequences of the above axioms. Alternatively, it can be defined as the set of those sentences that are true in the
intended interpretation
An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until ...
: the structure of non-negative integers with constants 0, 1, and the addition of non-negative integers.
Presburger arithmetic is designed to be complete and decidable. Therefore, it cannot formalize concepts such as
divisibility
In mathematics, a divisor of an integer n, also called a factor of n, is an integer m that may be multiplied by some integer to produce n. In this case, one also says that n is a multiple of m. An integer n is divisible or evenly divisible by ...
or
primality
A prime number (or a prime) is a natural number greater than 1 that is not a product of two smaller natural numbers. A natural number greater than 1 that is not prime is called a composite number. For example, 5 is prime because the only ways ...
, or, more generally, any number concept leading to multiplication of variables. However, it can formulate individual instances of divisibility; for example, it proves "for all ''x'', there exists ''y'' : (''y'' + ''y'' = ''x'') ∨ (''y'' + ''y'' + 1 = ''x'')". This states that every number is either even or odd.
Properties
Mojżesz Presburger
Mojżesz Presburger, or Prezburger, (December 27, 1904 – 1943) was a Polish Jewish mathematician, logician, and philosopher. He was a student of Alfred Tarski, Jan Łukasiewicz, Kazimierz Ajdukiewicz, and Kazimierz Kuratowski. He is known fo ...
proved Presburger arithmetic to be:
*
consistent
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 i ...
: There is no statement in Presburger arithmetic which can be deduced from the axioms such that its negation can also be deduced.
*
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 each statement in the language of Presburger arithmetic, either it is possible to deduce it from the axioms or it is possible to deduce its negation.
*
decidable: There exists an
algorithm
In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algorithms are used as specificat ...
which decides whether any given statement in Presburger arithmetic is a theorem or a nontheorem.
The decidability of Presburger arithmetic can be shown using
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 ...
, supplemented by reasoning about arithmetical congruence. The steps used to justify a quantifier elimination algorithm can be used to define recursive axiomatizations that do not necessarily contain the axiom schema of induction.
In contrast,
Peano arithmetic
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
, which is Presburger arithmetic augmented with multiplication, is not decidable, as a consequence of the negative answer to the
Entscheidungsproblem
In mathematics and computer science, the ' (, ) is a challenge posed by David Hilbert and Wilhelm Ackermann in 1928. The problem asks for an algorithm that considers, as input, a statement and answers "Yes" or "No" according to whether the state ...
. By
Gödel's incompleteness theorem, Peano arithmetic is incomplete and its consistency is not internally provable (but see
Gentzen's consistency proof
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 (i.e. are "consistent"), as long as a cer ...
).
Computational complexity
The decision problem for Presburger arithmetic is an interesting example in
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 by ...
and
computation
Computation is any type of arithmetic or non-arithmetic calculation that follows a well-defined model (e.g., an algorithm).
Mechanical or electronic devices (or, historically, people) that perform computations are known as ''computers''. An es ...
. Let ''n'' be the length of a statement in Presburger arithmetic. Then proved that, in the worst case, the proof of the statement in first order logic has length at least
, for some constant ''c''>0. Hence, their decision algorithm for Presburger arithmetic has runtime at least exponential. Fischer and Rabin also proved that for any reasonable axiomatization (defined precisely in their paper), there exist theorems of length ''n'' which have
doubly exponential length proofs. Intuitively, this suggests there are computational limits on what can be proven by computer programs. Fischer and Rabin's work also implies that Presburger arithmetic can be used to define formulas which correctly calculate any algorithm as long as the inputs are less than relatively large bounds. The bounds can be increased, but only by using new formulas. On the other hand, a triply exponential upper bound on a decision procedure for Presburger Arithmetic was proved by .
A more tight complexity bound was shown using alternating complexity classes by . The set of true statements in Presburger arithmetic (PA) is shown complete for
TimeAlternations(2
2nO(1), n). Thus, its complexity is between double exponential nondeterministic time (2-NEXP) and double exponential space (2-EXPSPACE). Completeness is under polynomial time many-to-one reductions. (Also, note that while Presburger arithmetic is commonly abbreviated PA, in mathematics in general PA usually means
Peano arithmetic
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
.)
For a more fine-grained result, let PA(i) be the set of true Σ
i PA statements, and PA(i, j) the set of true Σ
i PA statements with each quantifier block limited to j variables. '<' is considered to be quantifier-free; here, bounded quantifiers are counted as quantifiers.
PA(1, j) is in P, while PA(1) is NP-complete.
For i > 0 and j > 2, PA(i + 1, j) is
ΣiP-complete. The hardness result only needs j>2 (as opposed to j=1) in the last quantifier block.
For i>0, PA(i+1) is
ΣiEXP-complete (and is TimeAlternations(2
nO(i), i)-complete).
Short
Presburger Arithmetic (
) is
complete (and thus NP complete for
). Here, 'short' requires bounded (i.e.
) sentence size except that integer constants are unbounded (but their number of bits in binary counts against input size). Also,
two variable PA (without the restriction of being 'short') is NP-complete. Short
(and thus
) PA is in P, and this extends to fixed-dimensional parametric integer linear programming.
Applications
Because Presburger arithmetic is decidable,
automatic theorem prover
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...
s for Presburger arithmetic exist. For example, the
Coq
Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof ...
proof assistant system features the tactic omega for Presburger arithmetic and the
Isabelle proof assistant
The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs withou ...
contains a verified quantifier elimination procedure by . The double exponential complexity of the theory makes it infeasible to use the theorem provers on complicated formulas, but this behavior occurs only in the presence of nested quantifiers: describe an automatic theorem prover which uses the
simplex algorithm
In mathematical optimization, Dantzig's simplex algorithm (or simplex method) is a popular algorithm for linear programming.
The name of the algorithm is derived from the concept of a simplex and was suggested by T. S. Motzkin. Simplices are n ...
on an extended Presburger arithmetic without nested quantifiers to prove some of the instances of quantifier-free Presburger arithmetic formulas. More recent
satisfiability modulo theories
In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involvi ...
solvers use complete
integer programming
An integer programming problem is a mathematical optimization or Constraint satisfaction problem, feasibility program in which some or all of the variables are restricted to be integers. In many settings the term refers to integer linear programmin ...
techniques to handle quantifier-free fragment of Presburger arithmetic theory.
Presburger arithmetic can be extended to include multiplication by constants, since multiplication is repeated addition. Most array subscript calculations then fall within the region of decidable problems.
[For example, in the ]C programming language
''The C Programming Language'' (sometimes termed ''K&R'', after its authors' initials) is a computer programming book written by Brian Kernighan and Dennis Ritchie, the latter of whom originally designed and implemented the language, as well as ...
, if a
is an array of 4 bytes element size, the expression a /code> can be translated to abaseadr+i+i+i+i
which fits the restrictions of Presburger arithmetic.
This approach is the basis of at least five proof-of-
correctness systems for
computer programs
A computer program is a sequence or set of instructions in a programming language for a computer to execute. Computer programs are one component of software, which also includes documentation and other intangible components.
A computer program ...
, beginning with the
Stanford Pascal Verifier in the late 1970s and continuing through to Microsoft's Spec# system of 2005.
Presburger-definable integer relation
Some properties are now given about integer
relations definable in Presburger Arithmetic. For the sake of simplicity, all relations considered in this section are over non-negative integers.
A relation is Presburger-definable if and only if it is a
semilinear set.
A unary integer relation
, that is, a set of non-negative integers, is Presburger-definable if and only if it is ultimately periodic. That is, if there exists a threshold
and a positive period
such that, for all integer
such that
,
if and only if
.
By the
Cobham–Semenov theorem, a relation is Presburger-definable if and only if it is definable in
Büchi arithmetic Büchi arithmetic of base ''k'' is the first-order theory of the natural numbers with addition and the function V_k(x) which is defined as the largest power of ''k'' dividing ''x'', named in honor of the Swiss mathematician Julius Richard Büchi. T ...
of base
for all
. A relation definable in Büchi arithmetic of base
and
for
and
being
multiplicatively independent integers is Presburger definable.
An integer relation
is Presburger-definable if and only if all sets of integers which are definable in first order logic with addition and
(that is, Presburger Arithmetic plus a predicate for
) are Presburger-definable. Equivalently, for each relation
which is not Presburger-definable, there exists a first-order formula with addition and
which defines a set of integers which is not definable using only addition.
Muchnik's characterization
Presburger-definable relations admit another characterization: by Muchnik's theorem. It is more complicated to state, but led to the proof of the two former characterizations. Before Muchnik's theorem can be stated, some additional definitions must be introduced.
Let
be a set, the section
of
, for
and
is defined as
:
Given two sets
and a of integers
, the set
is called
-periodic in
if, for all
such that
then
if and only if
. For
, the set
is said to be in
if it is for some
such that
:
Finally, for
let
:
denote the cube of size
whose lesser corner is
.
Intuitively, the integer
represents the length of a shift, the integer
is the size of the cubes and
is the threshold before the periodicity. This result remains true when the condition
:
is replaced either by
or by
.
This characterization led to the so-called "definable criterion for definability in Presburger arithmetic", that is: there exists a first-order formula with addition and a predicate
which holds if and only if
is interpreted by a Presburger-definable relation. Muchnik's theorem also allows one to prove that it is decidable whether an
automatic sequence In mathematics and theoretical computer science, an automatic sequence (also called a ''k''-automatic sequence or a ''k''-recognizable sequence when one wants to indicate that the base of the numerals used is ''k'') is an infinite sequence of terms ...
accepts a Presburger-definable set.
See also
*
Robinson arithmetic
In mathematics, Robinson arithmetic is a finitely axiomatized fragment of first-order Peano arithmetic (PA), first set out by R. M. Robinson in 1950. It is usually denoted Q. Q is almost PA without the axiom schema of mathematical induction. Q is ...
*
Skolem arithmetic
References
Bibliography
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*
*, see for an English translation
*
*
*
*
*
*
{{Refend
External links
A complete Theorem Prover for Presburger Arithmeticby Philipp Rümmer
1929 introductions
Formal theories of arithmetic
Logic in computer science
Proof theory
Model theory