|
|
|
|
Presburger arithmetic
|
(Definition)
|
|
|
Presburger arithmetic is a weakened form of arithmetic which includes the structure $\mathbb{N}$ , the constant $0$ , the unary function $S$ , the binary function $+$ , and the binary relation
$<$ . Essentially, it is Peano arithmetic without multiplication.
The axioms are:
- $0\not= Sx$
- $Sx=Sy\rightarrow x=y$
- $x+0=x$
- $x+Sy=S(x+y)$
- For each first order formula $P(x)$ , $P(0)\wedge\forall x[P(x)\rightarrow P(x+1)]\rightarrow\forall x P(x)$
Presburger arithmetic is decidable, but is consequently very limited in what it can express.
|
"Presburger arithmetic" is owned by Henry.
|
|
(view preamble | get metadata)
Cross-references: formula, first order, axioms, Peano arithmetic, binary relation, binary, function, unary, constant, structure, arithmetic
This is version 5 of Presburger arithmetic, born on 2002-07-22, modified 2009-09-04.
Object id is 3185, canonical name is PressburgerArithmetic.
Accessed 4076 times total.
Classification:
| AMS MSC: | 03B10 (Mathematical logic and foundations :: General logic :: Classical first-order logic) |
|
|
|
|
|
|
Pending Errata and Addenda
|
|
|
|
|
|
|
|
|
|
|
