1
$\begingroup$

In his answer to the following mathoverflow question, The (un)decidability of Robinson Arithmetic without multiplication, Emil Jerabek proved that the following fragment:

  1. $\forall$x(Sx$\neq$0)

  2. $\forall$x$\forall$y(Sx=Sy $\Rightarrow$ x=y)

  3. $\forall$x(x$\neq$0 $\Rightarrow$ ($\exists$y)(x=Sy)

  4. $\forall$x(x+0=x)

  5. $\forall$x$\forall$y (x+Sy)=S(x+y)

"with '0' as the sole constant and 'S' [successor] and '+' as the built-in function signs...and whose deductive system is your favourite classical first-order logic with identity." (Quote from Peter Smith, the OP in question.)

is undecidable, and in fact hereditarily undecidable.

Question: What would be an example of a true but undecidable well-formed formula definable in the language of this fragment?

Improve this question
$\endgroup$
11
  • 1
    $\begingroup$ In your language you can say that every element is even or odd. This is true in the non-negative integers under addition but false for the set of polynomials with non-negative leading coefficients (under addition, with successor defined in the obvious way.) $\endgroup$
    – Sidney Raffer
    Commented Dec 14, 2015 at 13:24
  • $\begingroup$ I added a link to the previous question. Also, @SJR, why not post your comment as an answer? $\endgroup$
    – Joel David Hamkins
    Commented Dec 14, 2015 at 14:08
  • 3
    $\begingroup$ I also sense there is some confusion going on, since the question uses the word “undecidable” in two different senses, almost adjacent to each other. So let me stress that the linked question concerned the algorithmic undecidability of the Robinson arithmetic without multiplication, not its incompleteness (which should be obvious, as the theory does not include the Presburger division axioms such as the one mentioned by SJR). $\endgroup$
    – Emil Jeřábek
    Commented Dec 14, 2015 at 17:17
  • 1
    $\begingroup$ Oh, of course: the theory does not prove $\forall x\,(0+x=x)$, because full Robinson arithmetic does not. $\endgroup$
    – Emil Jeřábek
    Commented Dec 14, 2015 at 17:28
  • 1
    $\begingroup$ ??? That axiom is a tautology (take $x$ for $z$ and $y$ for $w$). $\endgroup$
    – Emil Jeřábek
    Commented Dec 15, 2015 at 10:39

1 Answer 1

Reset to default
1
$\begingroup$

Just turning what SJR wrote to an answer: the true but undecidable sentence is:

$$ \forall x((\exists y(x=y+y))\lor(\exists y(x=S(y+y)))). $$

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks (also to SJR who had the original idea). Question: How do you show that the consistency of this fragment of Robinson Arithmetic cannot be proven in this fragment of Robinson Arithmetic (seeing as how it cannot represent the recursive functions)? $\endgroup$
    – Thomas Benjamin
    Commented Dec 16, 2015 at 1:18
  • 1
    $\begingroup$ I am highly suspect that such a weak system even has a proof predicate. $\endgroup$
    – Fan Zheng
    Commented Dec 16, 2015 at 1:29

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .