A Universe of Sorts

We know that the first order theory of the 2-adics as a field (so with +, -, *, /, 0, 1) is decidable.
This decidability result is classical Diophantine Problems Over Local Fields: III. Decidable Fields .
More recently, there is even a quantifier elimination result for the 2-adics as a field, via a cylindrical algebraic decomposition: Quantifier elimination in p-adic fields .
A natural question is: what if we add bitwise operations such as AND, OR, XOR to the 2-adics, interpreted as infinite streams of bitvectors? Does the theory remain decidable?
We first show that if we have bitwise AND (henceforth, &&), then we can define the set of natural numbers N inside the 2-adics.
If N is definable, then we can encode Hilbert's 10th problem in our fragment, as it asks if there exists a natural number solution to a multivariate polynomial equation with integer coefficients.
This can be written as ∃ x1, x2, ..., xn ∈ N : P(x1, x2, ..., xn) = 0, where we encode x ∈ N using our definition of N in the 2-adics.

Key idea: a natural number is a number x whose 2-adic expansion becomes eventually all zeroes.
This is the same as having some bitmask M = ..0001111..1 such that x & M = x.
For every such bitmask M, see that M + 1 = P is a power of 2.
We can check if a number is a power of 2 with the bit-fiddling trick: P & (P - 1) = 0.
Thus, we can write x ∈ N iff ∃ M, P : (M + 1 = P) ∧ (P & (P - 1) = 0) ∧ (x & M = x).
This makes the natural numbers definable in the existential theory of the 2-adics with &&, and hence we can encode Hilbert's 10th problem as above, which is undecidable.

Recall that !x = -1 - x, which means bitwise NOT is definable in the 2-adics.
Proof: See that x + !x = -1 since -1 is the all-ones string, and in !x + x, at every bit location, either x[1] = 1 and !x[1] = 0, or vice versa. This means that x + !x = x || !x = -1.
Now, since x && y = !(!x || !y), we can define && in terms of || and !.
Thus, if || is definable, then so is &&, and 2-adics with AND is undecidable as above.

Recall that x + y = (x XOR y) + 2 * (x AND y).
Proof: This can be seen by thinking about the addition of numbers. We compute the carry bits as 2 (x AND y), and we compute the bits in the current place as x XOR y. We add these two up to get x + y.
This means that x AND y = ((x + y) - (x XOR y)) / 2.
Since the 2-adics are a field, we can divide by 2.
Alternatively, we can perform division by two by using an existential quantifier.
So given a predicate ∀ x, P(x/2), we can replace this with ∀ x y, 2*y = x → P(y).
Thus, if XOR is definable, then so is AND, and 2-adics with XOR is undecidable as above.

Recall that there are 16 boolean functions on 2 bits.
We use the table from wolfram mathworld .
F[0](x, y) := 0 is all zeroes, which adds no expressive power.
F[1](x, y) := x & y is AND, which is undecidable as above.
F[2](x, y) := x & !y is undecidable since we can get AND by x AND y = F[2](x, !y).
F[3](x, y) := x is projection, which adds no expressive power.
F[4](x, y) := !x & y is undecidable since we can get AND by x AND y = F[4](!x, y).
F[5](x, y) := y is projection, which adds no expressive power.
F[6](x, y) := x XOR y is undecidable as above.
F[7](x, y) := x OR y is undecidable as above.
F[8](x, y) := !(x OR y) is undecidable since we can get OR by x OR y = !F[8](x, y).
F[9](x, y) := !(x XOR y) is undecidable since we can get XOR by x XOR y = !F[9](x, y).
F[10](x, y) := !y adds no expressive power.
F[11](x, y) := x OR !y is undecidable since we can get OR by x OR y = F[11](x, !y).
F[12](x, y) := !x adds no expressive power.
F[13](x, y) := !x OR y is undecidable since we can get OR by x OR y = F[13](!x, y).
F[14](x, y) := !(x & y) is undecidable since we can get AND by x AND y = !F[14](x, y).
F[15](x, y) := 1 is all ones, which adds no expressive power.
Thus, all boolean functions except projections and constants lead to undecidability when added to the 2-adics.

§ Non Linear Theory of 2-Adics Does Not Mix with Bitwise Operations