Timeline for The (un)decidability of Robinson-Arithmetic-without-Multiplication?
Current License: CC BY-SA 3.0
13 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
May 23, 2020 at 6:21 | comment | added | Emil Jeřábek | @user76284 It’s included in Presburger arithmetic. | |
Sep 24, 2018 at 8:31 | comment | added | user21820 | @ThomasBenjamin: This model satisfies the Q axioms, including axiom 2 (right-cancellation of "1"), and satisfies LC (left-cancellation), but fails RC (right-cancellation in general). It also fails commutativity. The reason is the same; $1+ω = 0+ω = ω \ne ω+1$. Commutativity follows (for TC or Q) if you add some amount of induction. | |
Sep 24, 2018 at 8:25 | comment | added | user21820 | @ThomasBenjamin: I suppose your "editor axiom" is my axiom 5 in this Math SE post? You may be interested in the models that fail left/right-cancellation or both. In particular, interpret $0$ as the empty string, $+$ as concatenation, and $S$ as appending a "1" to the right. Then unary strings are the standard model of the axioms of Robinson's Q. (Here we need unary because of Q's axiom 3, whereas in my post I needed binary because of my axiom 4.) And basically the same non-standard model works; well-orders shorter than $ω^2$ modulo isomorphism. | |
Dec 14, 2015 at 16:47 | comment | added | Emil Jeřábek | (1) What is the “Editor Axiom”? (2) Ax2 says that $1$ is a right-cancellative element. This has nothing to do with commutativity. (3) Presburger arithmetic is the complete theory of the commutative structure $(\mathbb N,0,1,+)$, hence it of course proves commutativity. (It’s even often included as an axiom, though likely not in your axiomatization if it includes the induction schema. In any case a proof from the axioms should not be difficult.) | |
Dec 14, 2015 at 12:29 | comment | added | Thomas Benjamin | By the way, can Presburger arithmetic (since it has an axiom schema for induction) prove commutativity of addition? | |
Dec 14, 2015 at 12:16 | comment | added | Thomas Benjamin | @EmilJeřábek: Interesting. If you interpreted '+' as concatenation and added the "Editor Axiom" to the list, could you prove commutativity then? Why don't the axioms of equality and Ax2 suffice? | |
Dec 14, 2015 at 10:32 | comment | added | Emil Jeřábek | @ThomasBenjamin: The most obvious one is commutativity of addition. | |
Dec 14, 2015 at 4:21 | comment | added | Thomas Benjamin | @EmilJerabek: Interesting. What would be an example of a wff $W$ definable in the language of this subtheory of $Q$ theory such that neither $W$ nor $\lnot $$W$ are provable in this subtheory? | |
Jul 26, 2014 at 7:29 | vote | accept | Peter Smith | ||
Jul 25, 2014 at 14:08 | history | edited | Emil Jeřábek | CC BY-SA 3.0 |
added 1503 characters in body
|
Jul 25, 2014 at 13:08 | history | edited | François G. Dorais | CC BY-SA 3.0 |
Added the original axiom 1 since it has been edited in the question.
|
Jul 25, 2014 at 12:01 | comment | added | Peter Smith | Apologies -- that original Axiom 1 was indeed a silly typo. (Talk about senior moments ....) | |
Jul 25, 2014 at 11:36 | history | answered | Emil Jeřábek | CC BY-SA 3.0 |