Skip to main content

All Questions

Filter by
Sorted by
Tagged with
16 votes
2 answers
714 views

Is (Z,+,0,1,P2,P3) decidable?

Is Presburger arithmetic, augmented with two unary predicates P2, P3, for powers of 2 and powers of 3 respectively, decidable? I know that adding just one of P2, P3 to Presburger keeps it decidable, ...
7 votes
1 answer
262 views

What is known about first order logic of $\mathbb{N}$ with + and a unary predicate?

In "Weak Second-Order Arithmetic and Finite Automata", Büchi claims that the first order theory of $\mathbb{N}$ with + and a predicate for recognizing powers of 2 ($Pw_2$) is expressively ...
3 votes
0 answers
165 views

Why is the proof of decidability of arithmetic (Theorem 2.1) in Hamkins & Lewis (2000) enough?

Recently, I was reading the paper "Infinite Time Turing Machines" by Hamkins & Lewis. And one of the first theorems (Theorem 2.1) is about decidability of arithmetic. The proof is quite ...
0 votes
0 answers
104 views

Multivariate polynomial with infinite but discrete roots on one variable

I want to know if there exists a polynomial $ P(z, x_1,x_2,\ldots,x_n)$ over the rationals such that the set $$ Z_P = \{z | \exists x_1,\ldots,x_n. P(z, x_1,x_2,\ldots,x_n) = 0 \} \subsetneq \mathbb Q ...
17 votes
7 answers
2k views

Non-constructive proofs of decidability?

Are there examples of sets of natural numbers that are proven to be decidable but by non-constructive proofs only?
6 votes
2 answers
1k views

Are omega-consistent extensions of PA always consistent with each other?

The question is as in the title. In the edit history you can find my attempt to formalise the question, but that was a failure, for reasons stated clearly in the comments. Thus, my question is just: ...
5 votes
0 answers
287 views

Is the two variable fragment of arithmetic, i.e., theory of ($\mathbb{N}, + ,\times$), decidable?

Any references would be appreciated. Most places only address different vocabularies (e.g. a survey of arithmetical definability by Bes).
27 votes
1 answer
678 views

Decidability of equality of expressions built using 1,+,-,*,/,^

Consider expressions built using number $1$, arithmetical operators $+, -, *, /$ and exponentiation ^ (in case of multiple values, the principal value is assumed, the same way as it implemented in ...