Presburger arithmetic

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 Fischer & Rabin (1974).

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 closures of the following:

  1. ¬(0 = x + 1)
  2. x + 1 = y + 1 → x = y
  3. x + 0 = x
  4. x + (y + 1) = (x + y) + 1
  5. 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.[1]

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. 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

Presburger (1929) proved Presburger arithmetic to be:

  • consistent: There is no statement in Presburger arithmetic that can be deduced from the axioms such that its negation can also be deduced.
  • complete: 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 that decides whether any given statement in Presburger arithmetic is a theorem or a nontheorem - note that a "nontheorem" is a formula that cannot be proved, not in general necessarily one whose negation can be proved, but in the case of a complete theory like here both definitions are equivalent.

The decidability of Presburger arithmetic can be shown using quantifier elimination, supplemented by reasoning about arithmetical congruence.[2][3][4][5][6] The steps used to justify a quantifier elimination algorithm can be used to define computable axiomatizations that do not necessarily contain the axiom schema of induction.[2][7]

In contrast, Peano arithmetic, which is Presburger arithmetic augmented with multiplication, is not decidable, as proved by Church alongside the negative answer to the Entscheidungsproblem. By Gödel's incompleteness theorem, Peano arithmetic is incomplete and its consistency is not internally provable (but see Gentzen's consistency proof).

Computational complexity

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 Fischer & Rabin (1974) 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. 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 Oppen (1978).

A more tight complexity bound was shown using alternating complexity classes by Berman (1980). 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.[8]
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.[9]

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.[10] Short (and thus ) PA is in P, and this extends to fixed-dimensional parametric integer linear programming.[11]

Applications

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 Nipkow (2010). 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: Nelson & Oppen (1978) 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.[12]

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.[13] This approach is the basis of at least five[citation needed] 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.

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.[14]

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 .[15][16] 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.[17] 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.

Muchnik's characterization

Presburger-definable relations admit another characterization: by Muchnik's theorem.[18] 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 -tuple 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 -periodic in if it is -periodic for some such that

Finally, for let

denote the cube of size whose lesser corner is .

Muchnik's Theorem —  is Presburger-definable if and only if:

  • if then all sections of are Presburger-definable and
  • there exists such that, for every , there exists such that for all with is -periodic in .

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 -ary predicate that 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 accepts a Presburger-definable set.

See also

References

  1. ^ Zoethout 2015, p. 8, Theorem 1.2.4..
  2. ^ a b Presburger 1929.
  3. ^ Büchi 1962.
  4. ^ Monk 2012, p. 240.
  5. ^ Nipkow 2010.
  6. ^ Enderton 2001, p. 188.
  7. ^ Stansifer 1984.
  8. ^ Nguyen Luu 2018, chapter 3.
  9. ^ Haase 2014, pp. 47:1-47:10.
  10. ^ Nguyen & Pak 2017.
  11. ^ Eisenbrand & Shmonin 2008.
  12. ^ King, Barrett & Tinelli 2014.
  13. ^ For example, in the C programming language, if a is an array of 4 bytes element size, the expression a[i] can be translated to abaseadr+i+i+i+i, which fits the restrictions of Presburger arithmetic.
  14. ^ Ginsburg & Spanier 1966, pp. 285–296.
  15. ^ Cobham 1969, pp. 186–192.
  16. ^ Semenov 1977, pp. 403–418.
  17. ^ Michaux & Villemaire 1996, pp. 251–277.
  18. ^ Muchnik 2003, pp. 1433–1444.

Bibliography

  • Berman, L. (1980). "The Complexity of Logical Theories". Theoretical Computer Science. 11 (1): 71–77. doi:10.1016/0304-3975(80)90037-7.
  • Monk, J. Donald (2012). Mathematical Logic (Graduate Texts in Mathematics (37)) (Softcover reprint of the original 1st ed. 1976 ed.). Springer. ISBN 9781468494549.
  • Nelson, Greg; Oppen, Derek C. (April 1978). "A simplifier based on efficient decision algorithms". Proc. 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages: 141–150. doi:10.1145/512760.512775. S2CID 6342372.
  • Presburger, Mojżesz (1929). "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt". Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa: 92–101., see Stansifer (1984) for an English translation
  • Reddy, C.R.; Loveland, D.W. (1978). "Presburger arithmetic with bounded quantifier alternation". Proceedings of the tenth annual ACM symposium on Theory of computing - STOC '78. pp. 320–325. doi:10.1145/800133.804361. S2CID 13966721.
  • Young, P. (1985). "Gödel theorems, exponential difficulty and undecidability of arithmetic theories: an exposition". In A. Nerode and R. Shore (ed.). Recursion Theory, American Mathematical Society. pp. 503–522.

Read other articles:

Lunar Prospector adalah misi ketiga yang dipilih oleh NASA untuk pengembangan penuh dan konstruksi sebagai bagian dari Program Discovery. Dengan biaya $ 62.800.000, misi 19 bulan dirancang untuk orbit polar investigasi rendah dari bulan, termasuk pemetaan komposisi permukaan dan kemungkinan deposito es di kutub, pengukuran medan magnet dan gravitasi, dan studi peristiwa outgassing lunar. Misi yang berakhir 31 Juli 1999, ketika pengorbit itu sengaja menabrak kawah di dekat kutub selatan bulan...

 

Indian politician (1941–2020) See also: Arjun Singh Sethi Arjun Charan SethiMember: 5th, 7th, 10th, 12th, 13th, 14th, 15th and 16th Lok SabhaConstituencyBhadrak Personal detailsBorn(1941-09-18)18 September 1941Odang, Bhadrak, OdishaDied8 June 2020(2020-06-08) (aged 78)Bhubaneswar, OdishaNationalityIndianPolitical partyBJPSpouseSubhadra SethiChildren3 Sons And 2 DaughtersResidence(s)Bhadrak, OdishaAs of 22 September, 2006 Arjun Charan Sethi ([ɔrd͡ʒunɔ t͡ʃɔɾɔɳɔ seʈʰi]...

 

American geophysicist and administrator (1902–1973) Arthur Compton, Werner Heisenberg, George Monk, Paul Dirac, Carl Eckart, Henry Gale, Robert Mulliken, Friedrich Hund, Frank C. Hoyt. Chicago 1929. Carl Henry Eckart (May 4, 1902 – October 23, 1973) was an American physicist, physical oceanographer, geophysicist, and administrator. He co-developed the Wigner–Eckart theorem and is also known for the Eckart conditions in quantum mechanics,[1] and the Eckart–Young theorem in line...

For the collection of the same name by Dean Koontz, see Strange Highways (story collection). 1993 studio album by DioStrange HighwaysStudio album by DioReleasedOctober 25, 1993RecordedRumbo Recorders (Los Angeles)GenreDoom metal, heavy metalLength53:36Label Reprise (North America) Vertigo (rest of the world) ProducerMike FraserDio chronology Lock Up the Wolves(1990) Strange Highways(1993) Angry Machines(1996) Ronnie James Dio chronology Dehumanizer(1992) Strange Highways(1993) Angry ...

 

This article does not cite any sources. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: Slayter Center of Performing Arts – news · newspapers · books · scholar · JSTOR (September 2009) (Learn how and when to remove this template message) Slayter Center of Performing Arts - June 2006 The Slayter Center of Performing Arts is located on the main campus of Purdue Unive...

 

River in New South Wales, AustraliaBrunswick RiverMiddle Arm of Brunswick RiverMain Arm of Brunswick River[1]Littoral rainforest & oyster farm at Brunswick Heads, Australia. The rainforest features a large Ficus macrophylla in the left centreLocation of the Brunswick River mouth in New South WalesEtymologyIn honour of Queen Caroline of Brunswick[2]Native nameDurangbil (undetermined)[1]LocationCountryAustraliaStateNew South WalesIBRANSW North CoastDistrictNort...

Teritori HawaiiPanalāʻau o HawaiʻiOrganized incorporated territory di Amerika Serikat1898–1959 Panji daerah Lambang Teritorial HawaiiIbu kotaHonoluluSejarahPemerintahan • JenisTeritorial kerjasama yang dirancangGubernur • 1900–1903 Sanford B. Dole• 1957–1959 William F. Quinn Gubernur Militer • 1941–1944 May. Jen. T. H. Green Sejarah • Keruntuhan monarki 17 Januari 1893• Dianeksasi oleh AS 4 Juli 1898• Un...

 

Military warship designed to patrol rivers River monitors are military craft designed to patrol rivers. Model of USS Monitor They are normally the largest of all riverine warships in river flotillas, and mount the heaviest weapons. The name originated from the US Navy's USS Monitor, which made her first appearance in the American Civil War, and being distinguished by the use of revolving gun turrets, which were particularly useful in rivers, whose narrow channels could severely limit the...

 

У этого термина существуют и другие значения, см. Западный округ. Западный внутригородской округ город Краснодар Дата основания 1936 год Дата упразднения 1994 Прежние имена Кагановичский, Ленинский районы Микрорайоны Дубинка, Черёмушки, Покровка Площадь 22[1]  км² Насе...

Mahmoud Mokhtar Nazionalità  Egitto Calcio Ruolo Attaccante CarrieraSquadre di club1 1920-1924 Al-Ahly? (?)Nazionale 1920-1928 Egitto0+ (0+) 1 I due numeri indicano le presenze e le reti segnate, per le sole partite di campionato.Il simbolo → indica un trasferimento in prestito.   Modifica dati su Wikidata · Manuale Mahmoud Mokhtar Saqr, in arabo محمود مختار صقر‎? (1899 – ...), è stato un calciatore egiziano, di ruolo attaccante. Indice 1 Ca...

 

  关于与「內閣總理大臣」標題相近或相同的条目页,請見「內閣總理大臣 (消歧義)」。 日本國內閣總理大臣內閣總理大臣紋章現任岸田文雄自2021年10月4日在任尊称總理、總理大臣、首相、阁下官邸總理大臣官邸提名者國會全體議員選出任命者天皇任期四年,無連任限制[註 1]設立法源日本國憲法先前职位太政大臣(太政官)首任伊藤博文设立1885年12月22日,...

 

Centro Universitario Regional del Este Sigla CURETipo PúblicaUniversidad Universidad de la RepúblicaLocalización en MaldonadoDirección Tacuarembó entre Bv. Artigas y Av. SaraviaMaldonado Uruguay UruguayCoordenadas 34°54′53″S 54°56′32″O / -34.91472, -54.94222Dirección Burnett entre Av. Acuña de Figueroa y Av. ChiossiMaldonado Uruguay UruguayCoordenadas 34°54′52″S 54°57′15″O / -34.91444, -54.95417Localización en RochaDirección Ruta 9 ...

Politics of Gabon Constitution Human rights Government President (transitional) Brice Oligui Nguema Vice President (transitional) Joseph Owondault Berre Prime Minister Raymond Ndong Sima (transitional) Parliament Senate President: Paulette Missambo National Assembly President: Jean-François Ndongou Administrative divisions Provinces Departments Cantons and communes Elections Recent elections Presidential: 20162023 Parliamentary: 20182023 Political parties Foreign relations Ministry of Forei...

 

Region in the Upper Peninsula of Michigan, US Map of the region. Miners pose with lunch pails in hand on a mine rock pile outside of the Tamarack mineshaft. This mine was one of the most productive mines in the Copper Country. The Copper Country is an area in the Upper Peninsula of Michigan in the United States, including Keweenaw County, Michigan, Houghton, Baraga and Ontonagon counties as well as part of Marquette County. The area is so named as copper mining was prevalent there from 1845 u...

 

  提示:此条目页的主题不是萧。 簫琴簫與洞簫木管樂器樂器別名豎吹、豎篴、通洞分類管樂器相關樂器 尺八 东汉时期的陶制箫奏者人像,出土於彭山江口汉崖墓,藏於南京博物院 箫又稱洞簫、簫管,是中國古老的吹管樂器,特徵為單管、豎吹、開管、邊稜音發聲[1]。「簫」字在唐代以前本指排簫,唐宋以來,由於單管豎吹的簫日漸流行,便稱編管簫爲排簫�...

Midway attraction operated by Merlin Entertainments in County Hall, London DreamWorks Tours: Shrek's Adventure!County Hall, LondonCoordinates51°30′7″N 0°7′8″W / 51.50194°N 0.11889°W / 51.50194; -0.11889StatusOperatingOpening dateJuly 2015 (2015-07) Ride statisticsThemeShrek DreamWorks Tours: Shrek's Adventure!, commonly referred to as Shrek's Adventure!,[1][2] is a tourist attraction located in the County Hall building, London. It ...

 

Unincorporated community in Pennsylvania, United StatesSecane, PennsylvaniaUnincorporated communitySecaneLocation within the U.S. state of PennsylvaniaShow map of PennsylvaniaSecaneSecane (the United States)Show map of the United StatesCoordinates: 39°54′50″N 75°18′08″W / 39.91389°N 75.30222°W / 39.91389; -75.30222CountryUnited StatesStatePennsylvaniaCountyDelawareTownshipsUpper Darby, RidleyTime zoneUTC-5 (Eastern (EST)) • Summer (DST)UTC-4 (E...

 

Android smartphone developed by Motorola Mobility Second-generation Moto GMoto G running Android 5.0.2 LollipopCodenameTitan,[1] Thea (LTE)[2]ManufacturerMotorola MobilitySloganMoto G – Exceptional Phone. Exceptional Price.SeriesMotorola MotoCompatible networksGSM/GPRS/EDGE (850, 900, 1800, 1900 MHz) UMTS/HSPA+ up to 21 Mb/s (850, 900, 1900, 2100 MHz) FDD LTE 2100/1800/2600/800 (Bands 1, 3, 7, 20) TDD LTE 1900/2300/2500/2600 (Bands 38, 39, 40, 41)First release...

Public transport not funded by fares from passengers This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: Free public transport – news · newspapers · books · scholar · JSTOR (January 2018) (Learn how and when to remove this message) In 2020, Luxembourg became the first country to provide free public transport acr...

 

Italian operatic soprano Lina CavalieriLina Cavalieri, c. 1900BornNatalina Cavalieri(1874-12-25)25 December 1874Viterbo, Kingdom of ItalyDied7 February 1944(1944-02-07) (aged 69)Firenze, Kingdom of ItalyOccupations Opera singer (dramatic soprano) actress monologist Spouse(s)Alexandre Bariatinsky(m. 1899–1900)Robert Winthrop Chanler(m. 1910–1912; divorced)Lucien Muratore(m. 1913–1927)Paolo d'Arvanni(m. 19??—1944; their deaths)ChildrenAlexandre Bariatinsky, Jr. Natalina Lina ...