Timeline for Dedekind-Peano axioms, but numbers have at most one successor
Current License: CC BY-SA 4.0
27 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 24, 2023 at 9:08 | comment | added | abo | @EmilJeřábek. Thank you Emil. Very clear and helpful as always. | |
| Jan 23, 2023 at 12:27 | comment | added | Emil Jeřábek | @abo Oh, and yes: if $\phi$ is any arithmetical sentence (in a relational language where the arithmetical operations are not necessarily total), then $T\vdash\phi$ iff $I\Delta_0\vdash\forall x\,\phi^{\le x}$ and $\mathrm{PA}\vdash\phi$, where $\phi^{\le x}$ is $\phi$ with all quantifiers bounded by $x$. | |
| Jan 23, 2023 at 12:21 | comment | added | Emil Jeřábek | @Joel Concerning references, you already got an answer from Ali. The result that every model of $\mathrm{PA^{top}}$ is an initial interval of a model of $I\Delta_0$ is also proved in Hájek&Pudlák (Theorem IV.2.2), again attributed to Paris. Let me add that some interesting properties of variants of $\mathrm{PA^{top}}$ related to the weak pigeonhole principle are in Neil Thapen’s Ph.D. thesis. | |
| Jan 23, 2023 at 12:15 | comment | added | Emil Jeřábek | @abo Yes, it does. This follows from the fact that every model of $T$ has an end-extension to a model of $I\Delta_0$, as mentioned by Joel. Consequently, $T$ and $I\Delta_0$ prove the same $\Pi_1$ sentences (formulated so that only variables can be used to bound quantifiers). | |
| Jan 23, 2023 at 9:02 | comment | added | abo | Thanks Emil. My question is does the 1st order theory with the usual axioms for successor, +, and $\times$, minus the axiom that every number has a successor (and so the other axioms suitably adjusted) prove EL. Call this theory $T$. $T$ provability is different from $I \Delta_0$ provability because $I \Delta_0$ proves $\forall x \exists y (y = x+1)$ but $T$ doesn't (right??). Is there an operation * (e.g. bounding the quantifiers??) s.t. $T$ proves $\phi$ iff $I \Delta_0$ proves $\phi^*$? In any case my question is whether $T$ proves EL. Sorry for being stupid so early in the morning ... | |
| Jan 22, 2023 at 18:54 | comment | added | Joel David Hamkins | Ah, that is helpful. | |
| Jan 22, 2023 at 18:18 | comment | added | Emil Jeřábek | @Joel If I recall correctly, the system abo works with is not a genuine second-order theory, but “axiomatic second-order”, i.e., a two-sorted first-order theory with full comprehension. Its models where the successor function is not total are intervals on models of $V^\infty$, or equivalently (up to the so-called RSUV isomorphism), intervals on models of $I\Delta_0+\Omega_1$ (where numbers represent sets, and logarithmically small numbers represent numbers; see mathoverflow.net/a/120106 for more details). | |
| Jan 22, 2023 at 17:29 | comment | added | Emil Jeřábek | Euclid's lema is quite easy to prove in $I\Delta_0$ (or even its weak fragment $IE_1$). Whether $I\Delta_0$ proves Bertrand's postulate, or even just the unboundedness of primes, is a well known open problem; by a result of Woods, Bertrand's postulate (and the slightly stronger Sylvester's theorem) is provable in $I\Delta_0+WPHP(\Delta_0)$ (weak pigeonhole principle), which is included in $I\Delta_0+\Omega_1$. | |
| Jan 22, 2023 at 16:04 | comment | added | Joel David Hamkins | One should think of it as a very weak theory, in which even exponentiation is problematic and induction is possible only for very local phenomena. | |
| Jan 22, 2023 at 15:54 | comment | added | Joel David Hamkins | Ah, I thought you were asking about the second order theory. Huge difference. Since the models of the first-order theory are exactly the cut-offs of models of $I\Delta_0$, as I explain in my answer, the question is whether those theorems are provable in $I\Delta_0$, and there are many open questions about that. For example, pigeon-hole principle scheme is open. | |
| Jan 22, 2023 at 15:20 | comment | added | abo | I'm asking if they (Euclid's Lemma, Bertrand's Postulate) are provable in the first-order theory from the usual axioms for successor, addition, and multiplication (minus the axiom that every number has a successor). Are they? | |
| Jan 22, 2023 at 14:59 | comment | added | Joel David Hamkins | It is problematic to speak of "provable" in a second-order theory, since we don't have a sound & complete proof system for second-order logic. | |
| Jan 22, 2023 at 14:56 | comment | added | Joel David Hamkins | Both of those will be provable in the second-order theory. For Bertrand, take the statement for every n, there is a prime between n and 2n. You interpret the numbers up to 2n using digit representation as in my answer. This is a valid consequence of PA2top because it is true in standard finite segments. Similarly with Euclid's lemma. What I am saying is that any true statement expressible in the PAtop language will be valid in PA2top. The difficult cases occur with fast-growing functions that are out of reach of the interpretability methods, making the statements themselves not expressible. | |
| Jan 22, 2023 at 14:44 | comment | added | abo | @JoelDavidHamkins. Thanks very much! I'm really looking for natural examples, the more basic the better, so not examples independent of PA. E.g. Euclid's Lemma. (Or Bertrand's Postulate.) | |
| Jan 22, 2023 at 14:01 | history | edited | Joel David Hamkins | CC BY-SA 4.0 |
added 281 characters in body
|
| Jan 22, 2023 at 14:00 | comment | added | Joel David Hamkins | @abo The second-order version is true only in standard finite models, and so any $\Pi_1$ statement that is independent of PA (and there are many) will be unprovable in fPA but provable in the second-order version. e.g. all true consistency statements, and more. | |
| Jan 22, 2023 at 13:28 | comment | added | abo | @EmilJeřábek. If this is an abuse of your good services, then please ignore it. Is there a simple example of a statement unprovable in first-order fPA but provable in second-order fPA (i.e. with comprehension)? $\forall x \exists y Sx,y \rightarrow Cons(PA)$, where S is the successorship relationship and Cons(PA) is an arithmetical statement of the consistency of first-order PA, would if I'm not mistaken be an example, but I'm interested in a natural example. Is e.g. even Euclid's Lemma ($p|ab \rightarrow p|a \lor p|b$) provable in fPA? fPA just seems to be very weak, but perhaps I err... | |
| Jan 22, 2023 at 13:13 | vote | accept | James Propp | ||
| Jan 21, 2023 at 11:04 | history | edited | Joel David Hamkins | CC BY-SA 4.0 |
deleted 37 characters in body
|
| Jan 21, 2023 at 9:59 | comment | added | Joel David Hamkins | No problem, take your time. | |
| Jan 21, 2023 at 9:48 | comment | added | Emil Jeřábek | I’ll look up something. But checking references is very time consuming, and I likely won’t be able to do it during weekend. | |
| Jan 20, 2023 at 23:19 | comment | added | Joel David Hamkins | @EmilJeřábek If you have a good reference, I shall add it to the post. | |
| Jan 20, 2023 at 22:37 | vote | accept | James Propp | ||
| Jan 21, 2023 at 13:19 | |||||
| Jan 20, 2023 at 21:53 | comment | added | Joel David Hamkins | Thanks Emil. We've seen some hints of that, but clearly haven't been looking in the right place. | |
| Jan 20, 2023 at 21:49 | comment | added | Emil Jeřábek | The established name for the theory fPA plus the existence of a largest element is $\mathrm{PA^{top}}$. The fact that all its models are intervals of models of $I\Delta_0$ is well known. | |
| Jan 20, 2023 at 21:13 | history | edited | Joel David Hamkins | CC BY-SA 4.0 |
added 32 characters in body
|
| Jan 20, 2023 at 19:55 | history | answered | Joel David Hamkins | CC BY-SA 4.0 |