Табиғи сандардың қосылуымен бірінші реттік теориясының шешімділігі

Decidable first order theory of the natural numbers with addition
Presburger arithmetic is the first order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitting the multiplication operation entirely. The theory is computably axiomatizable; the axioms include a schema of induction. Presburger arithmetic is much weaker than Peano arithmetic, 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 .

The decision problem for Presburger arithmetic is an interesting example in computational complexity theory and computation. 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 that 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 that 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(22nO(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.) 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. 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.

Because Presburger arithmetic is decidable, automatic theorem provers for Presburger arithmetic exist. For example, the Coq proof assistant system features the tactic omega for Presburger arithmetic and the Isabelle proof assistant 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 that uses the simplex algorithm 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 solvers use complete integer programming 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. This approach is the basis of at least five proof of correctness systems for computer programs, beginning with the Stanford Pascal Verifier in the late 1970s and continuing through to Microsoft's Spec# system of 2005.

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 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 that are definable in first order logic with addition and (that is, Presburger arithmetic plus a predicate for ) are Presburger definable. Equivalently, for each relation that is not Presburger definable, there exists a first order formula with addition and that defines a set of integers that is not definable using only addition.