**Are you an EPFL student looking for a semester project?**

Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.

Concept# Presburger arithmetic

Summary

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 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 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 closures 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 of induction, 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 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: 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 or primality, or, more generally, any number concept leading to multiplication of variables.

Official source

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related courses (5)

Related concepts (11)

Related publications (37)

Related people (8)

Related units (1)

Related lectures (25)

MATH-483: Gödel and recursivity

Gödel incompleteness theorems and mathematical foundations of computer science

MATH-337: Number theory I.c - Combinatorial number theory

This is an introductory course to combinatorial number theory. The main objective of this course is to learn how to use combinatorial, topological, and analytic methods to solve problems in number the

EE-110: Logic systems (for MT)

Ce cours couvre les fondements des systèmes numériques. Sur la base d'algèbre Booléenne et de circuitscombinatoires et séquentiels incluant les machines d'états finis, les methodes d'analyse et de syn

Ontological neighbourhood

Gödel's incompleteness theorems

Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of mathematics. The theorems are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible. The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.

Peano axioms

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 unchanged in a number of metamathematical investigations, including research into fundamental questions of whether number theory is consistent and complete.

Decidability (logic)

In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer. Zeroth-order logic (propositional logic) is decidable, whereas first-order and higher-order logic are not. Logical systems are decidable if membership in their set of logically valid formulas (or theorems) can be effectively determined. A theory (set of sentences closed under logical consequence) in a fixed logical system is decidable if there is an effective method for determining whether arbitrary formulas are included in the theory.

Introduces formal verification methodology and Presburger arithmetic for program verification and automated reasoning.

Covers Presburger arithmetic, quantifier elimination, and the transformation of formulas into disjunctive normal form.

Explores representations, arithmetic, and limitations in logic systems, including place-value notation and binary arithmetic.

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in orthologic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based pro ...

Devices based on the spin as the fundamental computing unit provide a promising beyond-complementary metal-oxide-semiconductor (CMOS) device option, thanks to their energy efficiency and compatibility with CMOS. One such option is a magnetoelectric spin-or ...

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in ortho- logic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based p ...

2024