Following my question about defining multiplication in terms of divisibility, can all of arithmetic be axiomatized with a single two-term relation? Asaf Karagila comments on my question that the three-term relation Remainder is sufficient. I have since discovered that a two-term relation suffices, and this Wikipedia article agrees ("first-order logic is undecidable [...] provided that the language has at least one predicate of arity at least 2"). What is the binary predicate? How can arithmetic be axiomatized in terms of it? I have already discovered the answer, so I have tagged this as a puzzle. However, my construction is difficult and I am wondering if there are any easier ways.
EDIT: No answers yet so I'm adding some more details about my own solution. A binary predicate that I believe suffices is: R(2x+1,y) := Divides(x,y), R(2x,y) := Testbit(x,y). A next step is defining equality as x=y := ∀z:R(z,x)↔R(z,y). Still missing are the definitions of 0, 1, addition, and multiplication.
EDIT: As requested I'll include the rest of my attempted solution and expand the question somewhat. Is my solution correct? Can it be simplified in any significant way? Are there other binary predicates that work? What is a more precise and correct way to state the problem? Sorry if that is too much. Anyway, here is my solution. Start with defining equality as:
x=y := ∀z:R(z,x)↔R(z,y)
which means equal things have the same divisors and also the same bits set. Next define 0 and 1:
x=0 := ∀y:R(x,y)↔R(y,x)
Odd(x) := ∃y:y=0∧R(y,x)
x=1 := Odd(x)∧∀y:¬Odd(y)∧R(y,x)↔y=0
Also with Odd, divisibility can be unzipped:
Divides(x,y) := ∀z:Odd(z)→(R(z,x)→R(z,y))
Now we can define 2:
PowerOf2(x) := ∃y:¬Odd(y)∧R(y,x)∧∀z:¬Odd(z)∧R(z,x)→y=z
Prime(x) := ¬(x=1)∧∀y:Divides(y,x)↔(y=x∨y=1)
x=2 := PowerOf2(x)∧Prime(x)
And also multiplication by 2:
F(x,y,w) := PowerOf2(w)∧Divides(w,x)∧¬Divides(w,y)
x=2*y := (∀z:Odd(z)→(Divides(z,y)↔Divides(z,x)))∧(∃w:F(x,y,w)∧∀z:F(x,y,z)→z=w)
Having multiplication by 2 allows Testbit to be unzipped:
Testbit(x,y) := ∃z:z=2*y∧R(z,x)
Testbit gives us powers of 2:
x=Power(2,y) := ∀z:Testbit(z,x)↔z=y
Which finally yields the successor function:
y=Successor(x) := ∃z:∃w:z=Power(2,x)∧w=Power(2,y)∧w=2*z
And also less-than:
x Now addition can be defined: a+b=c := ∀i:Testbit(i,c)↔(Testbit(i,a)⊕Testbit(i,b)⊕ ∃j:j Finally, with a definition of a+b=c and Divides(x,y), follow the same construction given in the accepted answer to my prior question to define multiplication in terms of divisibility and addition, then it is done.