Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [presburger-arithmetic]

Presburger arithmetic is the first-order theory of the natural numbers with addition.

5
votes
0answers
60 views

How much arithmetic is required to formalize quantifier elimination in Presburger arithmetic?

As we know, Presburger arithmetic can be proved decidable by demonstrating that it admits quantifier elimination, i.e. that there is an algorithm that reduces any sentence in the language to some ...
0
votes
0answers
71 views

Why Presburger arithmetic cannot prove pigeonhole principle

The pigeonhole principle is the scheme $\forall \bar{a},s \{\forall x\!<\!s\!+\!1 \exists y\!<\!s\psi(x,y,\bar{a}) \to \exists x_1,x_2\!<\!s\!+\!1\exists y\!<\!s[x_1\neq x_2 \wedge \psi(...
1
vote
1answer
88 views

Do induction axioms of Peano Arithmetic have other simple equivalent forms?

For the example of Presburger Arithmetic, which consists of basic axioms for successor, addition, as well as an infinite set of induction axioms. However, it is well known that Presburger Arithmetic ...
4
votes
1answer
82 views

Systems of arithmetic models [closed]

Presburger Arithmetic is decidable theory but weaker than Peano Arithmetic. Are there systems in some sense that are: stronger than Presburger but weaker than Peano and remain decidable? weaker than ...
1
vote
0answers
41 views

Strongest decidable system of arithmetics

I have taken no formal mathematics logic course yet, I'm sorry for unclear parts of this question. I've learned about Presburger Arithmetics few days ago, it seemed really interesting. But since then,...
3
votes
1answer
107 views

Showing that Presburger arithmetic is decidable by deciding if $\mathbb N \models \varphi$, but does it give provability in the axioms?

Here Presburger arithemtic is given by a set of axioms over the signature with binary operation $+$ and two constants $0$ and $1$. Similarly in Presburgers original paper he gives the arithmetic in ...
1
vote
1answer
112 views

Decision procedure in Presburger arithmetic

Suppose I want to decide whether the statement $$\exists x.(x+x+x+1+1+1=1+1+1+1+1)$$ is part of the set of consequences of Presburger arithmetic. In more readable language, this is saying that $$...
6
votes
1answer
611 views

Presburger arithmetic

In discovering that Presburger's arithmetic is one of the weaker systems in PA that does not violate Godel's first incompleteness theorem. Upon reading the wiki article, it said that Presburger proved ...
5
votes
1answer
131 views

Pairing in Presburger arithmetic

Is it possible to define pairing function (and the inverses) in Presburger arithmetic? I would guess no but I can't locate a reference nor construct a proof to one way or another.
0
votes
0answers
82 views

Lemma for quantifier elimination over Presburger arithmetic.

I want to proof the following lemma taken from the book "The calculus of Computation": Let F be a quantifier-free $\sum_{\mathbb{Z}}$-formula with $free(F) = \{y\}$ representing the set $$S: \{n \...
2
votes
2answers
98 views

Peano/Presburger axioms - “find” numbers lower or equal than another number

[EDIT/CONCLUSION] It turns out it was actually working.. I was just like too stupid to let the prover run for more time and assumed it would take a lot / not be able to prove with what I've provided ...
1
vote
0answers
46 views

Doubly exponential complexity of Presburger arithmetics

I am trying to understand the proof of the aforementioned fact. For context, here's a rough outline of [what I am understanding to be] the idea behind the proof: in the language we construct a formula ...
1
vote
2answers
358 views

Can there exist a definition of 'multiplication' in Presberger Arithmetic?

According to Wikipedia, Presberger Arithmetic is the first-order theory of the natural numbers with addition. It can be proved to be consistent, complete, and decidable. Though it contains no axioms ...
3
votes
1answer
279 views

Why doesn't the decision problem for Presburger arithmetic demonstrate that $\mathsf{P} \neq \mathsf{NP}$

From Wikipedia's article on Presburger arithmetic: Then Fischer and Rabin (1974) proved that any decision algorithm for Presburger arithmetic has a worst-case runtime of at least $2^{2^{cn}}$, for ...
1
vote
0answers
183 views

Why does a definition of multiplication in Presburger Arithmetic result in an undecidable theory? [duplicate]

Presburger Arithmetic is a decidable theory but if multiplication is added to it would that theory remain decidable? UPDATE: I began to write out the axioms that would distinguish Presburger ...
0
votes
0answers
148 views

Presburger arithmetic and finite model property

I'm learning about model theory and first order logic. Recently, I read about finite model property and Presburger arithmetic, and I have two questions about them: Does Presburger arithmetic has ...
1
vote
1answer
379 views

Is there a difference between induction in Peano Arithmetic and Presburger Arithmetic?

Following this question I still do not get clearly the difference between defining exponentiation in PA but impossiblity of recursively define multiplication in Presburger Arithmetics I was thinking ...
3
votes
1answer
149 views

Why is it impossible to define multiplication in Presburger arithmetic yet possible to define exponentiation in Peano Arithmethic?

Hello my question is related to Why is it impossible to define multiplication in Presburger arithmetic? and to How is exponentiation defined in Peano arithmetic?. I would have preferred to add it as a ...
1
vote
1answer
189 views

An impressive fact expressible in Presburger arithmetic?

Is there anything expressible in Presburger arithmetic that would seem impressive to students at an undergraduate level?
0
votes
2answers
56 views

Different arithmetics

The original Peano axioms were based on a single unary operator $\operatorname{succ}$ and one second-order induction axiom: $\lbrace \operatorname{succ} \rbrace + \operatorname{IND}_2$ Peano ...
0
votes
0answers
54 views

Finding simpler implied formulas while preserving contradiction

I have two Presburger formulas A and B such that $A\land B \equiv \text{False}$. From these I need to find shorter formula $A'$ such that $A \rightarrow A'$ and $A' \land B \equiv \text{False}.$ The ...
2
votes
1answer
207 views

Nonstandard structure of Presburger arithmetic

Let $\mathfrak {R}_A = (\Bbb {N}; 0, S,<,+)$. What can we say about ${}^{\ast}\Bbb N$, the universe of non-standard structure of the first order theory of $\mathfrak {R}_A$? Firstly, because of ...
1
vote
1answer
171 views

Where do I go wrong with Presburger “multiplication”?

This is a speculation about the Presburger arithmetics, the Peano axioms with only addition added, vis-à-vis the same axioms with both addition and multiplication added. In the first case I understand ...
9
votes
3answers
1k views

Why is it impossible to define multiplication in Presburger arithmetic?

Peano arithmetic defines multiplication recursivly as: $$\begin{gather}a\cdot0=a\\a\cdot S(b)=a+(a\cdot b)\end{gather}$$ Why is this not possible in Presburger arithmetic?
7
votes
1answer
541 views

Nonstandard models of Presburger Arithmetic

I have a question about nonstandard models of Presburger Arithmetic. I read that an example of a nonstandard model is the set of polynomials with rational coefficients with positive leading ...