Timeline for Can Robinson arithmetic prove any interesting theorems?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 9, 2020 at 8:48 | comment | added | Emil Jeřábek | Robinson’s arithmetic is Robinson’s arithmetic. Other theories of the form “a variant axiomatization of PA minus the induction schema” are not called and should not be called Robinson’s arithmetic. There is no need to confuse the OP on this front. | |
| Dec 9, 2020 at 8:12 | comment | added | Emil Jeřábek | I don’t know what counts as interesting, but Robinson’s arithmetic proves all kinds of things of the form “Bertrand’s postulate and Sylvester’s theorem hold for all numbers from this and this definable cut”. (The definition of the cut may be fairly long, sure.) | |
| Dec 9, 2020 at 0:12 | comment | added | Noah Schweber | @DavidRoberts I think he is referring to the following. If I'm defining $\mathsf{PA}$ to an audience not interested in Robinson arithmetic, I'll say it's the nonnegative discrete ordered semiring axioms + the induction scheme. Throwing away induction then amounts to axioms saying that you're the nonnegative part of a discrete ordered ring. However, this is much stronger than Robinson arithmetic, which e.g. doesn't even prove that addition is commutative. The issue is that there are lots of ways to write $\mathsf{PA}=T+IndScheme$, which the slogan "$\mathsf{PA}-IndScheme=\mathsf{Q}$" ignores. | |
| Dec 8, 2020 at 23:41 | comment | added | David Roberts♦ | @FrançoisG.Dorais what's the semiring trap? Does it pin down things super tightly? | |
| Dec 8, 2020 at 23:12 | comment | added | François G. Dorais | "Those of PA" is the ambiguous part. If you're more specific you will see that there are lots and lots of models! (Especially if you stick to the basics and don't fall into the semiring trap.) I think they're interesting but I can only remember a couple of uses, both would perhaps seem sketchy to you. | |
| Dec 8, 2020 at 23:00 | comment | added | BPP | As far as I understand, its original usage was for proving theorems about it, not for proving theorems within it. I'm thinking of the first-order theory whose axioms are those of PA without induction with the axiom that every number is either 0 or the successor of some number. | |
| Dec 8, 2020 at 22:38 | comment | added | François G. Dorais | Other than it's original usage and derivatives? Which version of Robinson arithmetic are you thinking of? | |
| Dec 8, 2020 at 22:30 | history | asked | BPP | CC BY-SA 4.0 |