Quelltext der Seite Presburger-Arithmetik

Die '''Presburger-Arithmetik''' ist eine in der [[Prädikatenlogik erster Stufe]] formulierte [[Mathematik|mathematische]] Theorie der [[natürliche Zahl|natürlichen Zahlen]] mit [[Addition]].
Sie ist benannt nach [[Mojżesz Presburger]], der sie im Jahre 1929 einführte.<ref name="Presburger" />
Die [[Signatur (Modelltheorie)|Signatur]] der Presburger-Arithmetik enthält nur Addition, nicht jedoch die Multiplikation.
Zum Axiomensystem gehört auch ein [[Axiomenschema]] der [[Vollständige Induktion|vollständigen Induktion]].

Die Presburger-Arithmetik ist erheblich schwächer als die [[Peano-Arithmetik]], in der sowohl Addition als auch Multiplikation formalisiert werden.
Im Gegensatz zur Peano-Arithmetik ist die Presburger-Arithmetik eine entscheidbare Theorie, d.&nbsp;h., es lässt sich für jede in der Sprache der Presburger-Arithmetik formulierte Aussage [[Berechenbarkeit|effektiv]] entscheiden, ob sie aus den Axiomen der Theorie beweisbar ist oder nicht.
Allerdings ist die asymptotische Laufzeit eines entsprechenden Algorithmus laut einer Arbeit von Fischer und Rabin doppelt exponentiell.<ref name="FischerRabin" />

== Definition ==
Die Sprache der Presburger-Arithmetik enthält Konstanten 0 und 1 sowie eine binäre Operation +, die als Addition zu interpretieren ist.
In dieser Sprache lauten die Axiome der Presburger-Arithmetik wie folgt:
# <math>0+1 = 1</math> <!--wird für Kommutativität benötigt.-->
# <math>\forall x\colon \neg(x+1=0)</math>
# <math>\forall x,y\colon (x+1=y+1\rightarrow x=y)</math>
# <math>\forall x\colon x+0 = x</math>
# <math>\forall x,y\colon (x+y)+1=x+(y+1)</math>
# Sei <math>P(x, y_1,\ldots, y_k)</math> eine Formel in der Sprache der Presburger-Arithmetik mit freien Variablen <math>x, y_1,\ldots, y_k</math>. Dann ist folgende Aussage ein Axiom:
::<math>\forall y_1,\ldots,y_k\colon ((P(0, y_1,\ldots, y_k) \land \forall x\colon (P(x, y_1,\ldots, y_k)\rightarrow P(x+1, y_1,\ldots, y_k)))\rightarrow \forall x\colon P(x, y_1,\ldots, y_k))</math>

Letzteres ist ein Axiomenschema der vollständigen Induktion und steht für unendlich viele Einzelaxiome. Diese dem Schema (6) entsprechenden Axiome lassen sich nicht durch endlich viele Axiome ersetzen, so dass die Presburger-Arithmetik insgesamt nicht endlich axiomatisierbar ist.

== Beschreibung ==
Die Presburger-Arithmetik kann Konzepte wie [[Teilbarkeit]] oder [[Primzahl]]en nicht formalisieren, geschweige denn die Multiplikation, denn dann müsste die Presburger-Arithmetik wie die Peano-Arithmetik unvollständig und unentscheidbar sein.
Individuelle Instanzen der Teilbarkeit können aber durchaus formalisiert werden, etwa „<math>x</math> ist gerade“ durch <math>G(x):\Leftrightarrow\exists z\colon z+z=x</math>; hiermit ausdrückbare wahre Aussagen wie
:<math>\forall x,y\colon (G(x)\land G(y) \rightarrow G(x+y))</math>
: („Die Summe zweier gerader Zahlen ist gerade“)
sind dann beweisbare Sätze.

== Eigenschaften ==
Mojżesz Presburger wies folgende Eigenschaften seiner Arithmetik nach:<ref name="Presburger" />
* [[Widerspruchsfreiheit|Konsistenz]]: Es gibt keine in ihrer Sprache formulierte Aussage <math>P</math>, für die sowohl <math>P</math> als auch <math>\neg P</math> aus den Axiomen hergeleitet werden kann.
* [[Vollständigkeit (Logik)|Vollständigkeit]]: Für jede in der Sprache der Presburger-Arithmetik formulierte Aussage <math>P</math> ist entweder <math>P</math> oder die Verneinung <math>\neg P</math> aus den Axiomen herleitbar.
* [[Entscheidbarkeit]]: Es gibt einen [[Algorithmus]], der zu jeder gegebenen Aussage der Presburger-Arithmetik entscheiden kann, ob sie wahr oder falsch ist.

Die Entscheidbarkeit der Presburger-Arithmetik lässt sich durch [[Quantorenelimination]] und die Betrachtung arithmetischer [[Kongruenz (Zahlentheorie)|Kongruenzen]] nachweisen.<ref name="Enderton" />

Die Peano-Arithmetik, also Presburger-Arithmetik zuzüglich Multiplikation, ist dagegen nicht entscheidbar.
Gemäß [[Gödelscher Unvollständigkeitssatz|Gödels Unvollständigkeitssatz]] ist sie auch unvollständig und ihre Konsistenz nicht (intern) beweisbar.

Das Entscheidungsproblem für die Presburger-Arithmetik ist ein interessantes Beispiel der [[Komplexitätstheorie]]. Sei <math>n</math> die Länge einer Aussage der Presburger-Arithmetik. Dann hat der Entscheidungsalgorithmus für die Presburger-Arithmetik laut einer Arbeit von Fischer und Rabin<ref name="FischerRabin" /> mindestens doppelt-exponentielle Laufzeit, d.&nbsp;h., im worst case beträgt die Laufzeit mindestens <math>2^{2^{cn}}</math> für eine gewisse positive Konstante <math>c</math>.
Andererseits gibt es eine dreifach-exponentielle obere Abschätzung für die Laufzeit.<ref name="Oppen" />
Es handelt sich also um ein Entscheidungsproblem, das nachweislich nicht in exponentieller (geschweige denn polynomieller) Zeit gelöst werden kann.
Fischer und Rabin zeigten auch, dass für jede (in einem von ihnen präzisierten Sinne) vernünftige Axiomatisierung Sätze beliebiger Länge existieren, deren kürzester Beweis von doppelt-exponentieller Länge ist. Intuitiv bedeutet dies, dass es praktische Grenzen für [[Computerbeweis]]e gibt.
Aus der Arbeit von Fischer und Rabin ergibt sich ferner, dass mit der Presburger-Arithmetik Formeln definiert werden können, die einen beliebigen Algorithmus korrekt nachbilden, solange die Eingaben gewisse –&nbsp;verhältnismäßig hohe&nbsp;– Grenzen nicht überschreiten. Diese Grenzen können durch den Übergang zu anderen Formeln jeweils noch erhöht werden.

== Anwendungen ==
Es existieren auch tatsächlich Computerbeweissysteme, die Algorithmen zur Entscheidung von Formeln in Presburger-Arithmetik gebrauchen.
Beispielsweise enthält [[Coq (Software)|Coq]] Beweistaktiken in dieser Richtung.
Die doppelt-exponentielle Komplexität begrenzt zwar die praktische Einsetzbarkeit für komplizierte Formeln, jedoch tritt dieses Verhalten nur bei verschachtelten [[Quantor]]en auf: Oppen und Nelson<ref name="Nelson-Oppen" /> beschreiben ein auf dem [[Simplex-Verfahren]] beruhendes automatisches Beweissystem für eine erweiterte Presburger-Arithmetik ohne verschachtelte Quantoren. Die Worst-case-Laufzeit des Simplexverfahrens ist (einfach) exponentiell. Tatsächlich wird exponentielle Laufzeit sogar nur für speziell konstruierte Fälle beobachtet, während es in Alltagsfällen erheblich effizienter arbeitet. Hierdurch ist dieser Ansatz durchaus für den praktischen Einsatz geeignet.

Die Presburger-Arithmetik lässt sich um die Multiplikation mit Konstanten erweitern, da es sich hierbei um wiederholte Addition handelt.
In der Programmiertechnik betrifft dies beispielsweise die Berechnung von Feldindizes.
Dieser Ansatz ist Grundlage von mindestens fünf Systemen für den Korrektheitsbeweis von Computerprogrammen, angefangen beim [[Stanford Pascal Verifier]] aus den späten 1970er Jahren bis hin zu [[Microsoft]]s [[Spec-Sharp|Spec#]] von 2005.

== Literatur ==
* {{Literatur
   |Autor=David C. Cooper
   |Hrsg=Bernhard Meltzer, Donald Michie
   |Titel={{lang|en|Theorem Proving in Arithmetic without Multiplication}}
   |Sammelwerk={{lang|en|Machine Intelligence}}
   |Band=7
   |Verlag=Edinburgh University Press
   |Ort=Edinburgh
   |Datum=1972
   |ISBN=978-0-470-60110-5
   |Seiten=91–99}}
* {{Literatur
   |Autor=Jeanne Ferrante, Charles W. Rackoff
   |Titel=The Computational Complexity of Logical Theories
   |Reihe=Lecture Notes in Mathematics
   |NummerReihe=718
   |Verlag=Springer-Verlag
   |Datum=1979
   |ISBN=3-540-09501-2
   |DOI=10.1007/BFb0062837}}
* {{Literatur
   |Autor=William Pugh
   |Titel=The Omega test
   |TitelErg=a fast and practical integer programming algorithm for dependence analysis
   |Sammelwerk=Proceedings of the 1991 ACM/IEEE conference on Supercomputing
   |Datum=1991
   |ISBN=0-89791-459-7
   |DOI=10.1145/125826.125848}}
* {{Literatur
   |Autor=Cattamanchi Ramalinga Reddy, Donald W. Loveland
   |Hrsg=
   |Titel=Presburger Arithmetic with Bounded Quantifier Alternation
   |Sammelwerk=ACM Symposium on Theory of Computing
   |Datum=1978
   |Seiten=320–325
   |DOI=10.1145/800133.804361}}
* {{Literatur
   |Autor=Paul Young
   |Hrsg=Anil Nerode, Richard A. Shore
   |Titel=Gödel theorems, exponential difficulty and undecidability of arithmetic theories. An exposition
   |Sammelwerk=Recursion Theory
   |Reihe=Proceedings of symposia in pure mathematics
   |Band=42
   |Verlag=American Mathematical Society
   |Datum=1985
   |ISBN=0-8218-1447-8
   |Seiten=503–522}}

== Weblinks ==
* Philipp Rümmer: [http://www.philipp.ruemmer.org/princess.shtml Princess], ein Computerbeweissystem für Presburger-Arithmetik (englisch).

== Einzelnachweise ==
<references>
<ref name="Enderton">
{{Literatur
 |Autor=Herbert B. Enderton
 |Titel={{lang|en|A mathematical introduction to logic}}
 |Auflage=2.
 |Verlag=Academic Press
 |Ort=Boston
 |Datum=2001
 |ISBN=0-12-238452-0
 |Seiten=188}}
</ref>
<ref name="FischerRabin">{{Literatur
 |Autor=Michael J. Fischer, Michael O. Rabin
 |Hrsg=
 |Titel={{lang|en|Super-Exponential Complexity of Presburger Arithmetic}}
 |Sammelwerk={{lang|en|Proceedings of the SIAM-AMS Symposium in Applied Mathematics}}
 |Band=7
 |Ort=
 |Datum=1974
 |Seiten=27–41
 |Online=http://www.lcs.mit.edu/publications/pubs/ps/MIT-LCS-TM-043.ps
 |Format=Postscript
 |KBytes=
 |Abruf=2012-02-26
 }}</ref>
<ref name="Nelson-Oppen">
{{Literatur
 |Autor=Greg Nelson, Derek C. Oppen
 |Hrsg=
 |Titel={{lang|en|A simplifier based on efficient decision algorithms}}
 |Sammelwerk={{lang|en|Proc. 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages}}
 |Ort=
 |Datum=1978-04
 |Seiten=141–150
 |DOI=10.1145/512760.512775}}
</ref>
<ref name="Oppen">
{{Literatur
 |Autor=Derek C. Oppen
 |Titel={{lang|en|A 2<sup>2<sup>2<sup>''pn''</sup></sup></sup> Upper Bound on the Complexity of Presburger Arithmetic}}
 |Sammelwerk=J. Comput. Syst. Sci.
 |Band=16
 |Nummer=3
 |Datum=1978
 |Seiten=323–332
 |DOI=10.1016/0022-0000(78)90021-1}}
</ref>
<ref name="Presburger">
{{Literatur
 |Autor=Mojżesz Presburger
 |Titel=Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt
 |Sammelwerk={{lang|fr|Comptes Rendus du I congrès de Mathématiciens des Pays Slaves}}
 |Ort=Warschau
 |Datum=1929
 |Seiten=92–101}}
</ref>
</references>

[[Kategorie:Zahl]]
[[Kategorie:Logik]]
[[Kategorie:Beweis (Mathematik)]]
[[Kategorie:Modelltheorie]]