Return to Question

I asked this over at math.stackexchange, and though a number of people were interested enough to vote up the question, I didn't get an answer -- which makes me wonder whether it isn't quite so trivial/dumb as I originally feared it was. So let me try again in this more turbo-charged forum ...

Take our old friend Robinson Arithmetic, and cut it down to a theory of successor and addition.

To spell that out (just to ensure that we are singing from the same hymn sheet), take the first-order theory with $\mathsf{0}$ as the sole constant, and $\mathsf{S}$ and $+$ as the built-in function signs, with the five axioms

1. $\mathsf{\forall x\ 0 \neq Sx}$
2. $\mathsf{\forall x\forall y\ Sx = Sy \to x = y}$
3. $\mathsf{\forall x(x \neq 0 \to \exists y\ x = Sy)}$
4. $\mathsf{\forall x\ (x + 0) = x}$
5. $\mathsf{\forall x\forall y\ (x + Sy) = S(x + y)}$

and whose deductive system is your favourite classical first-order logic with identity.

Since this cut-down theory doesn't represent the recursive functions, you can't use the usual proof of undecidability for an arithmetic. Since this cut-down theory doesn't even know that addition is commutative, you can't do the kind of manipulations inside the theory involved in a quantifier-elimination proof of decidability (cf. what happens when we add induction to this theory to get Presburger arithmetic, i.e. Peano Arithmetic minus multiplication).

Ermmmm .... so .... Drat it, I ought to know how to prove that this cut-down theory is decidable or that it is undecidable. But I seem to have forgotten, assuming I ever knew, and searching around hasn't helped me out. OK folks, I'm more than likely to be having a senior moment here [well, given the lack of answers on math.se maybe a forgivable senior moment?] -- so be gentle! -- but how do we show the theory is (un)decidable? [My bet is on undecidable, for what little that it is worth ...]

I asked this over at math.stackexchange, and though a number of people were interested enough to vote up the question, I didn't get an answer -- which makes me wonder whether it isn't quite so trivial/dumb as I originally feared it was. So let me try again in this more turbo-charged forum ...

Take our old friend Robinson Arithmetic, and cut it down to a theory of successor and addition.

To spell that out (just to ensure that we are singing from the same hymn sheet), take the first-order theory with $\mathsf{0}$ as the sole constant, and $\mathsf{S}$ and $+$ as the built-in function signs, with the five axioms

1. $\mathsf{\forall x\ 0 \neq Sx}$
2. $\mathsf{\forall x\forall y\ Sx = Sy \to x = y}$
3. $\mathsf{\forall x(x \neq 0 \to \exists y\ x = Sy)}$
4. $\mathsf{\forall x\ (x + 0) = x}$
5. $\mathsf{\forall x\forall y\ (x + Sy) = S(x + y)}$

and whose deductive system is your favourite classical first-order logic with identity.

Since this cut-down theory doesn't represent the recursive functions, you can't use the usual proof of undecidability for an arithmetic. Since this cut-down theory doesn't even know that addition is commutative, you can't do the kind of manipulations inside the theory involved in a quantifier-elimination proof of decidability (cf. what happens when we add induction to this theory to get Presburger arithmetic, i.e. Peano Arithmetic minus multiplication).

Ermmmm .... so .... Drat it, I ought to know how to prove that this cut-down theory is decidable or that it is undecidable. But I seem to have forgotten, assuming I ever knew, and searching around hasn't helped me out. OK folks, I'm more than likely to be having a senior moment here [well, given the lack of answers on math.se maybe a forgivable senior moment?] -- so be gentle! -- but how do we show the theory is (un)decidable? [My bet is on undecidable, for what little that it is worth ...]

I asked this over at math.stackexchange, and though a number of people were interested enough to vote up the question, I didn't get an answer -- which makes me wonder whether it isn't quite so trivial/dumb as I originally feared it was. So let me try again in this more turbo-charged forum ...

Take our old friend Robinson Arithmetic, and cut it down to a theory of successor and addition.

To spell that out (just to ensure that we are singing from the same hymn sheet), take the first-order theory with $\mathsf{0}$ as the sole constant, and $\mathsf{S}$ and $+$ as the built-in function signs, with the five axioms

1. $\mathsf{\forall x\ x \neq Sx}$
2. $\mathsf{\forall x\forall y\ Sx = Sy \to x = y}$
3. $\mathsf{\forall x(x \neq 0 \to \exists y\ x = Sy)}$
4. $\mathsf{\forall x\ (x + 0) = x}$
5. $\mathsf{\forall x\forall y\ (x + Sy) = S(x + y)}$

and whose deductive system is your favourite classical first-order logic with identity.

Since this cut-down theory doesn't represent the recursive functions, you can't use the usual proof of undecidability for an arithmetic. Since this cut-down theory doesn't even know that addition is commutative, you can't do the kind of manipulations inside the theory involved in a quantifier-elimination proof of decidability (cf. what happens when we add induction to this theory to get Presburger arithmetic, i.e. Peano Arithmetic minus multiplication).

Ermmmm .... so .... Drat it, I ought to know how to prove that this cut-down theory is decidable or that it is undecidable. But I seem to have forgotten, assuming I ever knew, and searching around hasn't helped me out. OK folks, I'm more than likely to be having a senior moment here [well, given the lack of answers on math.se maybe a forgivable senior moment?] -- so be gentle! -- but how do we show the theory is (un)decidable? [My bet is on undecidable, for what little that it is worth ...]

I asked this over at math.stackexchange, and though a number of people were interested enough to vote up the question, I didn't get an answer -- which makes me wonder whether it isn't quite so trivial/dumb as I originally feared it was. So let me try again in this more turbo-charged forum ...

Take our old friend Robinson Arithmetic, and cut it down to a theory of successor and addition.

To spell that out (just to ensure that we are singing from the same hymn sheet), take the first-order theory with $\mathsf{0}$ as the sole constant, and $\mathsf{S}$ and $+$ as the built-in function signs, with the five axioms

1. $\mathsf{\forall x\ 0 \neq Sx}$
2. $\mathsf{\forall x\forall y\ Sx = Sy \to x = y}$
3. $\mathsf{\forall x(x \neq 0 \to \exists y\ x = Sy)}$
4. $\mathsf{\forall x\ (x + 0) = x}$
5. $\mathsf{\forall x\forall y\ (x + Sy) = S(x + y)}$

and whose deductive system is your favourite classical first-order logic with identity.

Since this cut-down theory doesn't represent the recursive functions, you can't use the usual proof of undecidability for an arithmetic. Since this cut-down theory doesn't even know that addition is commutative, you can't do the kind of manipulations inside the theory involved in a quantifier-elimination proof of decidability (cf. what happens when we add induction to this theory to get Presburger arithmetic, i.e. Peano Arithmetic minus multiplication).

Ermmmm .... so .... Drat it, I ought to know how to prove that this cut-down theory is decidable or that it is undecidable. But I seem to have forgotten, assuming I ever knew, and searching around hasn't helped me out. OK folks, I'm more than likely to be having a senior moment here [well, given the lack of answers on math.se maybe a forgivable senior moment?] -- so be gentle! -- but how do we show the theory is (un)decidable? [My bet is on undecidable, for what little that it is worth ...]

I asked this over that math.stackexchange, and though a number of people were interested enough to vote up the question, I didn't get an answer -- which makes me wonder whether it isn't quite so trivial/dumb as I originally feared it was. So let me try again in this more turbo-charged forum ...

Take our old friend Robinson Arithmetic, and cut it down to a theory of successor and addition.

To spell that out (just to ensure that we are singing from the same hymn sheet), take the first-order theory with $\mathsf{0}$ as the sole constant, and $\mathsf{S}$ and $+$ as the built-in function signs, with the five axioms

1. $\mathsf{\forall x\ x \neq Sx}$
2. $\mathsf{\forall x\forall y\ Sx = Sy \to x = y}$
3. $\mathsf{\forall x(x \neq 0 \to \exists y\ x = Sy)}$
4. $\mathsf{\forall x\ (x + 0) = x}$
5. $\mathsf{\forall x\forall y\ (x + Sy) = S(x + y)}$

and whose deductive system is your favourite classical first-order logic with identity.

Since this cut-down theory doesn't represent the recursive functions, you can't use the usual proof of undecidability for an arithmetic. Since this cut-down theory doesn't even know that addition is commutative, you can't do the kind of manipulations inside the theory involved in a quantifier-elimination proof of decidability (cf. what happens when we add induction to this theory to get Presburger arithmetic, i.e. Peano Arithmetic minus multiplication).

Ermmmm .... so .... Drat it, I ought to know how to prove that this cut-down theory is decidable or that it is undecidable. But I seem to have forgotten, assuming I ever knew, and searching around hasn't helped me out. OK folks, I'm more than likely to be having a senior moment here [well, given the lack of answers on math.se maybe a forgivable senior moment?] -- so be gentle! -- but how do we show the theory is (un)decidable? [My bet is on undecidable, for what little that it is worth ...]

I asked this over at math.stackexchange, and though a number of people were interested enough to vote up the question, I didn't get an answer -- which makes me wonder whether it isn't quite so trivial/dumb as I originally feared it was. So let me try again in this more turbo-charged forum ...

Take our old friend Robinson Arithmetic, and cut it down to a theory of successor and addition.

To spell that out (just to ensure that we are singing from the same hymn sheet), take the first-order theory with $\mathsf{0}$ as the sole constant, and $\mathsf{S}$ and $+$ as the built-in function signs, with the five axioms

1. $\mathsf{\forall x\ x \neq Sx}$
2. $\mathsf{\forall x\forall y\ Sx = Sy \to x = y}$
3. $\mathsf{\forall x(x \neq 0 \to \exists y\ x = Sy)}$
4. $\mathsf{\forall x\ (x + 0) = x}$
5. $\mathsf{\forall x\forall y\ (x + Sy) = S(x + y)}$

and whose deductive system is your favourite classical first-order logic with identity.

Since this cut-down theory doesn't represent the recursive functions, you can't use the usual proof of undecidability for an arithmetic. Since this cut-down theory doesn't even know that addition is commutative, you can't do the kind of manipulations inside the theory involved in a quantifier-elimination proof of decidability (cf. what happens when we add induction to this theory to get Presburger arithmetic, i.e. Peano Arithmetic minus multiplication).

Ermmmm .... so .... Drat it, I ought to know how to prove that this cut-down theory is decidable or that it is undecidable. But I seem to have forgotten, assuming I ever knew, and searching around hasn't helped me out. OK folks, I'm more than likely to be having a senior moment here [well, given the lack of answers on math.se maybe a forgivable senior moment?] -- so be gentle! -- but how do we show the theory is (un)decidable? [My bet is on undecidable, for what little that it is worth ...]