Questions tagged [presburger-arithmetic]
Presburger arithmetic is the first-order theory of the natural numbers with addition.
40 questions
1
vote
1
answer
117
views
Complexity of $Th(\langle \mathbb{Z}; + , 1 \rangle)$ same as $Th(\langle \mathbb{Z}; + \rangle)$?
I want to know a lower bound for the complexity of the decision problem for $\langle \mathbb{Z}; + \rangle$. The below paper notes that Presburger arithmetic, originally $\langle \mathbb{N}; +\rangle$,...
- 287
3
votes
0
answers
60
views
Explicit bound for superexponential estimate for Presburger Arithmetic?
Fischer and Rabin proved a superexponential bound $2^{2^{cn}}$ for the worst-case length of a proof of a proposition of length $n$ in Presburger arithmetic. The result is in
Michael J. Fischer and ...
- 49.2k
0
votes
1
answer
41
views
Are functions $f: \{1,\ldots,m\} \times \{1,\ldots,n\} \to \{1,\ldots,n\}$ definable in Presburger arithmetic?
Given a function $f: \{1,\ldots,m\} \times \{1,\ldots,n\} \to \{1,\ldots,n\}$ where $m,n$ are strictly positive natural numbers. Is there a Presburger arithmetic formula that represents it?
- 6,377
5
votes
0
answers
98
views
What modifications to the axioms of primitive recursion would restrict its expressivity to that of Presburger arithmetic?
Inspired by reading through this page:
https://golem.ph.utexas.edu/category/2019/08/turing_categories.html
https://en.wikipedia.org/wiki/Primitive_recursive_function
Among the primitive recursive ...
- 61
1
vote
0
answers
96
views
Axioms of Linear Integer Arithmetic?
The slides I am reading don't give the axioms of LIA (linear integer arithmetic) instead only give it's signature. I looked on the internet and can't find the axioms of LIA. For the following ...
- 2,737
3
votes
1
answer
250
views
Presburger arithmetic is consistent, but relative to what?
In the Wikipedia article for (the first-order theory of) Presburger arithmetic, it is stated (among other properties) that Presburger arithmetic is consistent. What meta-theory does he rely on in ...
user923098
1
vote
1
answer
190
views
Is it possible to use order relation in Presburger arithmetic?
The signature of Presburger arithmetic contains only the addition
operation and equality, omitting the multiplication operation
entirely.
Is it possible to state and prove theorems in Presburger ...
- 443
7
votes
0
answers
139
views
Is Presburger arithmetic in "Ramsey logic" complete?
Let $\Sigma=\{+,<,0,1\}$ be the usual language of Presburger arithmetic - so we have addition but no multiplication (the additional symbols for $<,0,1$ are unnecessary but convenient). Given a &...
- 265k
1
vote
1
answer
188
views
What is the interpretation of Presburger Arithmetic in WS1S?
It’s my understanding that Julius Büchi showed that $WS1S$, the weak monadic second-order theory of one successor is decidable by a finite-state automaton, and that this implies that Presburger ...
6
votes
0
answers
360
views
Is it not possible to state the Collatz Conjecture in a decidable theory?
I believe that the answer is no (evidenced by the 80+ year "open" status of the conjecture), but I am self-taught in formal logic and decidability theory, so I would like to present my ...
- 7,626
1
vote
1
answer
349
views
Presburger arithmetic vs Linear Integer Arithmetic
I always work with these two and use it with no distinction, but I am probably wrong.
I mean, are their signatures the same? And their axioms? I know that, for instance, the quantifier elimination ...
- 247
1
vote
1
answer
248
views
Question concerning Presburger arithmetic
Context: Presburger arithmetic is the theory $\tau$ of structure $$ A = (\mathbb{N},0,1,+,\{c|\cdot\}_{c\in\mathbb{N}})$$ where for each integer $c > 1$, the unary predicate c|n holds if and only ...
- 47
3
votes
0
answers
161
views
Oracle for computing transitive closure of presburger arithmetic formula if it exists: Computable?
Let $Q(\vec x, \vec y) \subseteq \mathbb Z^n \times \mathbb Z^n$ be a relation which can be represented in presburger arithmetic.
Let $R(\vec x, \vec y) \equiv Q \cup (Q \circ Q) \cup (Q \circ Q \...
- 8,920
1
vote
1
answer
164
views
Graph planarity definability clarification in literature?
Here it says planarity is definable in first order.
http://jgaa.info/accepted/recent/Brandenburg.pdf
Here it says planarity testing of graphs is not a first order property.
Refer https://simons....
- 6,341
8
votes
3
answers
480
views
Are there "interesting" theorems in Peano arithmetic, that only use the addition operation?
More precisely, are there "interesting" theorems of Presburger arithmetic, other than the following four well-known "interesting" ones?
The commutativity of addition.
The theorem stating there are no ...
- 109