Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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<y := ¬(x=y)∧∃z:∃w:z=Power(2,x)∧w=Power(2,y)∧Divides(z,w)

Now addition can be defined:

a+b=c := ∀i:Testbit(i,c)↔(Testbit(i,a)⊕Testbit(i,b)⊕ ∃j:j<i∧Testbit(j,a)∧Testbit(j,b)∧∀k:(k<i∧j<k)→(Testbit(k,a)⊕Testbit(k,b)))

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.

share|cite|improve this question
You could let the binary predicate be $\in$ and build just enough of set theory to be able to do arithmetic. – Henning Makholm Sep 30 '11 at 7:03
@Henning, I had thought of that, but how to prove that addition is a total function without the axiom of infinity? There is a different interpretation of the binary predicate that I had in mind. – Dan Brumleve Sep 30 '11 at 7:05
Um, are we supposed to be playing guess-what-it-is-he-has-in-mind? Life's too short for that, I'm afraid. – Henning Makholm Sep 30 '11 at 7:49
@Henning, am I using the "puzzle" tag inappropriately? Should I edit my question to include my own solution? – Dan Brumleve Sep 30 '11 at 7:57
Could the downvoter please explain the downvote? Please note the FAQ: "Add comments indicating what, specifically, is wrong." – joriki Sep 30 '11 at 8:03
up vote 1 down vote accepted

I think your result is actually a special case of ($\star$) given any (finite) number of arbitrary relations $R_1,R_2, \ldots R_r$ on $\mathbb Z$ (with arbitrary arities), there is a single two-term relation $A(x,y)$ on $\mathbb Z$ such that all the $R_i$ are definable in terms of $A$.

To prove ($\star$), it will suffice to show the weaker form ($\star\star$ ) : given any two two-term relations $R_1(x,y)$ and $R_2(x,y)$ on $\mathbb Z$, there is a two-term relation $A(x,y)$ on $\mathbb Z$ such that $R_1$ and $R_2$ are both definable in terms of $A$ (indeed, it follows from ($\star\star$) by induction that any finite number of two-terms relations can be generated by a single two-term relation, and if $\beta=(\beta_1,\beta_2)$ is any bijection ${\mathbb Z} \to {\mathbb Z}^2$, we may add the two-term relations $U_1(x,y):y=\beta_1(x)$ and $U_2(x,y):y=\beta_2(x)$. Then $\beta(z)=(x,y)$ can be defined as $U_1(z,x) \wedge U_2(z,y)$, so that $\beta$ is definable. This takes care of relations with larger arities).

So let us show ($\star\star$) : take two two-term relations $R_1(x,y)$ and $R_2(x,y)$ on $\mathbb Z$. Let $X=\lbrace 501,601,701,801, \ldots ,1401\rbrace$ and $Y=\lbrace 10;11;12;13;14 \rbrace$. Since $|X|=10$ and $|Y|=5$, we have $|X|<2^{|Y|}$ so there is an injection $\gamma : X \to {\cal P}(Y)$.

Define a two-term relation $A : {\mathbb Z}^2 \to \lbrace True,False \rbrace$ by the following eleven (disjoint and hence consistent) rules :

(1) For $x\in{\mathbb Z}$, set $A(x,x)=(x=5)$.

(2) For $x\in [|5(...)14|], y\in{\mathbb Z} \setminus \lbrace 5 \rbrace$ with $y \neq x$, set $A(x,y)=(y=x+1)$.

(3) For $x\in{\mathbb Z} \setminus [|5(...)15|], y \in [|5(...)8|]$, set $A(x,y)=( x \equiv y-4 \ ({\rm mod} \ 100))$.

(4) For $x\in{\mathbb Z} \setminus [|5(...)15|]$, set $A(x,9)=(x\in X)$.

(5) For $x\in X$ and $y\in Y$, set $A(x,y)=(y\in \gamma(x))$.

(6) For $x,y \in \mathbb Z$, set $A(100x+1,100y+2)=(x=y)$.

(7) For $x,y \in \mathbb Z$, set $A(100x+2,100y+1)=(R_1(x,y))$.

(8) For $x,y \in \mathbb Z$, set $A(100x+1,100y+3)=(x=y)$.

(9) For $x,y \in \mathbb Z$, set $A(100x+3,100y+1)=(R_2(x,y))$.

(10) For $x\not\in [|5(...)14|],y \in \mathbb Z$ with $x\neq 100y+4$, set $A(x,100y+4)=(y=x)$.

(11) For $x\in{\mathbb Z}, y\not\in [|x(...)14|], y\not\equiv 4 \ ({\rm mod} \ 100)$, set $A(100x+4,y)=(y=100x+1)$.

Then, using only $A$, we may successively define the one-term relations ‟$x=5$”, ‟$x=k$” for $2 \leq k \leq 14$, ‟x equals $k$ modulo 100” for $1\leq k \leq 4$,‟$x$ is in $X$”, and finally ‟$x=k$” for each individual $k\in X$ (using rule (5)).

Then the two-term relation $D(x,y):y=100x+1$ can be defined : this is $D_1(x,y) \vee D_2(x,y)$, where $D_1(x,y)$ is $$ (x=5 \wedge y=501)\vee(x=6 \wedge y=601) \ldots \vee (x=14 \wedge y=1401) $$ and $D_2(x,y)$ is $$ (y\not\in [| 5(...)15 |]) \wedge (y\not\equiv 4 \ ({\rm mod} \ 100)) \wedge (\exists z \ (z \equiv 4 \ ({\rm mod} \ 100)) \wedge A(x,z) \wedge A(z,y)). $$

Now we can define $R_1(x,y)$ as $$ \exists x' \ \exists y' \ \exists z \ (z \equiv 2 \ ({\rm mod} \ 100)) \wedge D(x,x') \wedge D(y,y') \wedge A(x',z) \wedge A(z,y') $$ and $R_2(x,y)$ as $$ \exists x' \ \exists y' \ \exists z \ (z \equiv 3 \ ({\rm mod} \ 100)) \wedge D(x,x') \wedge D(y,y') \wedge A(x',z) \wedge A(z,y'), $$ which finishes the proof.

share|cite|improve this answer
It is interesting to me that while this is more general than my solution, it has the same interleaved structure. Is mine more "natural" in some sense? I had thought that the definitions of 0, 1, etc. were vital to the construction but I guess you are saying that this is not the case! – Dan Brumleve Oct 9 '11 at 6:56

I'm going to turn my comment into an answer, just because I'm curious to see what, if anything, is wrong with this construction.

Let $S$ be a binary predicate. Informally, we want $S(x,y)$ to mean "$y$ is a successor of $x$". I will not assume that the underlying logic includes an equality predicate, but will rather define one as follows:

Definition 1: $\displaystyle x = y \ \overset{\operatorname{def}}\iff\ \forall z: (S(z,x) \iff S(z,y))$

That is, $x$ and $y$ are equal if and only if they have the same predecessor(s). I will strengthen this definition with the following axiom:

Axiom 2: $\displaystyle x = y \iff \forall z: (S(x,z) \iff S(y,z))$

That is, $x$ and $y$ are equal if and only if they have the same successor(s). Having defined an equality predicate, I will adopt axioms stating that each number has a unique successor (up to equality as defined above):

Axiom 3: $\displaystyle \forall x\; \exists y: S(x,y)$

Axiom 4: $\displaystyle (S(x,y) \wedge S(x,z)) \implies y=z$

From these axioms, we may prove that all predecessors of a number are equal:

Theorem 5: $\displaystyle (S(x,z) \wedge S(y,z)) \implies x=y$

Proof: Assume the opposite, i.e. that $\exists x,y,z: S(x,z) \wedge S(y,z) \wedge x \ne y$. Then by axiom 2 there exists $w$ such that either $S(x,w) \wedge \neg S(y,w)$ or $\neg S(x,w) \wedge S(y,w)$. Assume WLOG the former: then $S(x,z) \wedge S(x,w)$, which by axiom 4 implies $z=w$. But then by definition 1, $S(y,z) \iff S(y,w)$, which yields the contradiction $S(y,w) \wedge \neg S(y,w)$.

I'll adopt an axiom stating that there exists a number with no predecessors:

Axiom 6: $\displaystyle \exists y\; \forall x: \neg S(x,y)$

By definition 1, all $y$ satisfying this axiom are equal. For convenience, I will adopt the constant symbol $0$ to denote one of them. Thus:

Corollary 7: $\displaystyle y = 0 \iff \forall x: \neg S(x,y)$

In particular, theorem 5 together with this corollary implies that all numbers not equal to $0$ have a unique predecessor.

Finally, I will adopt an axiom schema for induction; namely, for each formula $\phi$ in the language of this theory which does not contain $a$ or $b$ as free variables, I will adopt the axiom:

Axiom schema 8: $\displaystyle (\phi(0) \wedge \forall a,b: (\phi(a) \wedge S(a,b)) \implies \phi(b)) \implies \forall x: \phi$

where $\phi(c)$ denotes $\phi$ with all free occurrences of the variable $x$ replaced by $c$.

It remains to define addition and multiplication, which I will do in more or less that usual manner. I will start by recursively defining the ternary predicate $A$ as:

Definition 9: $\displaystyle A(x,y,z) \ \overset{\operatorname{def}}\iff\ (x=0 \wedge y=z) \vee (\exists u,v: S(u,x) \wedge S(y,v) \wedge A(u,v,z))$

The next step is to prove that, for each $x$ and $y$, there exists a unique $z$ (which we may denote by $x+y$) such that $A(x,y,z)$:

Theorem 10: $\displaystyle \forall x,y\; \exists z: A(x,y,z)$

Proof: By definition 9, $\forall y: A(0,y,y)$. Assume that $\forall v\; \exists z: A(u,v,z)$ and $S(u,x)$; by axiom 3, $\forall y\;\exists v: S(y,v)$, and thus by definition 9 $\forall y\;\exists z: A(x,y,z)$. Thus, the conclusion follows by induction (axiom schema 8) on $\phi(x) = \forall y\;\exists z:A(x,y,z)$.

Theorem 11: $\displaystyle \forall y,z,w: A(x,y,z) \wedge A(x,y,w) \implies z = w$

Proof: Again follows from definition 9 and the uniqueness of successors (axiom 4) and predecessors (theorem 5) by induction on $x$; omitted because I'm getting too tired to write it out.

Similarly, multiplication can be defined via the recursive predicate $M$:

Definition 12: $\displaystyle M(x,y,z) \ \overset{\operatorname{def}}\iff\ (y=0 \wedge z=0) \vee (\exists u,v: S(u,y) \wedge M(x,u,v) \wedge A(x,v,z))$

Again, because I'm tired, I'll omit the proof that for each $x$ and $y$ there exists a unique $z = x \cdot y$ for which $M(x,y,z)$. It should be true, unless I've screwed up somewhere. It should also be possible to show that the addition and multiplication operators thus defined satisfy all the usual algebraic properties we want from the natural numbers, but I won't try to do that now.

share|cite|improve this answer
It is fine up to Definition 9, but the problem there is that A is defined recursively and we don't have the ability to do that until we can express the beta function in the same language. – Dan Brumleve Oct 2 '11 at 4:44
@Dan: There's nothing wrong with a recursive definition. Look at the axioms of PA, for example. – Zhen Lin Oct 2 '11 at 8:10
I think I see Dan's point now. I can certainly add $A$ to the language and take dfn. 9 as an axiom, but then I have an extra predicate in the language. What I can't do is just treat the LHS of dfn. 9 as a shorthand for the RHS, since trying to recursively expand the shorthand for arbitrary $x$ would yield an infinitely long formula. – Ilmari Karonen Oct 2 '11 at 16:22
@Ilmari: Yes, that is right. With every sentence of PA we want to associate some (finite) equivalent sentence in a new FOL theory whose non-logical signature contains just the one binary relation symbol. Also I'm interested in cases without induction (Robinson arithmetic) if it makes any difference. – Dan Brumleve Oct 2 '11 at 20:32

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.