Skip to main content
MathOverflow

Return to Answer

Removing the noise, in light of the other answers.
Source Link
Joel David Hamkins
Joel David Hamkins
  • 236.2k
  • 44
  • 777
  • 1.4k

Let me give half an answer.

Specifically, we can interpret your theory in PA via the Ackermann encoding. Namely, in any model of PA, define $m\in x$ if and only if the $m$th bit of $x$ is $1$. This fulfills all your axioms.

But conversely, I am unsure. Perhaps one can try to define the arithmetic from your axioms. We can certainly define the successor function from the order directly. But I am uncertain how to define $+$ or $\cdot$ from your system. One needs to have a pairing function. Perhaps one can hope to undertake coding via your set axiom, by describing sets with properties that would support increasing levels of coding, and then proving via induction that the coding always extends, and in this way getting the arithmetic as coded in bounded segments. But I am worried that perhaps the system is too weak to undertake this.

One partial step in this direction would be to look at the case where we start with a PA model and define $\in$ as I did with the Ackermann encoding. Using only $<$ and $\in$, can we definably recover $+$ and $\cdot$ from it? I wouldn't find this unreasonable, since the PA model would have all kinds of sets encoding big pieces of the arithmetic, and perhaps we could extract this information using $\in$. A difficult with this approach would be that the sets amount to a monodic set struture, whereas we really need binary encoding. So the first step would be to get a pair function. Perhaps it isn't possible...

Let me give half an answer.

Specifically, we can interpret your theory in PA via the Ackermann encoding. Namely, in any model of PA, define $m\in x$ if and only if the $m$th bit of $x$ is $1$. This fulfills all your axioms.

But conversely, I am unsure. Perhaps one can try to define the arithmetic from your axioms. We can certainly define the successor function from the order directly. But I am uncertain how to define $+$ or $\cdot$ from your system. One needs to have a pairing function. Perhaps one can hope to undertake coding via your set axiom, by describing sets with properties that would support increasing levels of coding, and then proving via induction that the coding always extends, and in this way getting the arithmetic as coded in bounded segments. But I am worried that perhaps the system is too weak to undertake this.

One partial step in this direction would be to look at the case where we start with a PA model and define $\in$ as I did with the Ackermann encoding. Using only $<$ and $\in$, can we definably recover $+$ and $\cdot$ from it? I wouldn't find this unreasonable, since the PA model would have all kinds of sets encoding big pieces of the arithmetic, and perhaps we could extract this information using $\in$. A difficult with this approach would be that the sets amount to a monodic set struture, whereas we really need binary encoding. So the first step would be to get a pair function. Perhaps it isn't possible...

Let me give half an answer.

Specifically, we can interpret your theory in PA via the Ackermann encoding. Namely, in any model of PA, define $m\in x$ if and only if the $m$th bit of $x$ is $1$. This fulfills all your axioms.

added 616 characters in body
Source Link
Joel David Hamkins
Joel David Hamkins
  • 236.2k
  • 44
  • 777
  • 1.4k

Let me give half an answer.

Specifically, we can interpret your theory in PA via the Ackermann encoding. Namely, in any model of PA, define $m\in x$ if and only if the $m$th bit of $x$ is $1$. This fulfills all your axioms.

But conversely, I am unsure. Perhaps one can try to define the arithmetic from your axioms. We can certainly define the successor function from the order directly. But I am uncertain how to define $+$ or $\cdot$ from your system. One needs to have a pairing function. Perhaps one can hope to undertake coding via your set axiom, by describing sets with properties that would support increasing levels of coding, and then proving via induction that the coding always extends, and in this way getting the arithmetic as coded in bounded segments. But I am worried that perhaps the system is too weak to undertake this.

One partial step in this direction would be to look at the case where we start with a PA model and define $\in$ as I did with the Ackermann encoding. Using only $<$ and $\in$, can we definably recover $+$ and $\cdot$ from it? I wouldn't find this unreasonable, since the PA model would have all kinds of sets encoding big pieces of the arithmetic, and perhaps we could extract this information using $\in$. A difficult with this approach would be that the sets amount to a monodic set struture, whereas we really need binary encoding. So the first step would be to get a pair function. Perhaps it isn't possible...

Let me give half an answer.

Specifically, we can interpret your theory in PA via the Ackermann encoding. Namely, in any model of PA, define $m\in x$ if and only if the $m$th bit of $x$ is $1$. This fulfills all your axioms.

But conversely, I am unsure. Perhaps one can try to define the arithmetic from your axioms. We can certainly define the successor function from the order directly. But I am uncertain how to define $+$ or $\cdot$ from your system. One needs to have a pairing function. Perhaps one can hope to undertake coding via your set axiom, by describing sets with properties that would support increasing levels of coding, and then proving via induction that the coding always extends, and in this way getting the arithmetic as coded in bounded segments. But I am worried that perhaps the system is too weak to undertake this.

Let me give half an answer.

Specifically, we can interpret your theory in PA via the Ackermann encoding. Namely, in any model of PA, define $m\in x$ if and only if the $m$th bit of $x$ is $1$. This fulfills all your axioms.

But conversely, I am unsure. Perhaps one can try to define the arithmetic from your axioms. We can certainly define the successor function from the order directly. But I am uncertain how to define $+$ or $\cdot$ from your system. One needs to have a pairing function. Perhaps one can hope to undertake coding via your set axiom, by describing sets with properties that would support increasing levels of coding, and then proving via induction that the coding always extends, and in this way getting the arithmetic as coded in bounded segments. But I am worried that perhaps the system is too weak to undertake this.

One partial step in this direction would be to look at the case where we start with a PA model and define $\in$ as I did with the Ackermann encoding. Using only $<$ and $\in$, can we definably recover $+$ and $\cdot$ from it? I wouldn't find this unreasonable, since the PA model would have all kinds of sets encoding big pieces of the arithmetic, and perhaps we could extract this information using $\in$. A difficult with this approach would be that the sets amount to a monodic set struture, whereas we really need binary encoding. So the first step would be to get a pair function. Perhaps it isn't possible...

Source Link
Joel David Hamkins
Joel David Hamkins
  • 236.2k
  • 44
  • 777
  • 1.4k

Let me give half an answer.

Specifically, we can interpret your theory in PA via the Ackermann encoding. Namely, in any model of PA, define $m\in x$ if and only if the $m$th bit of $x$ is $1$. This fulfills all your axioms.

But conversely, I am unsure. Perhaps one can try to define the arithmetic from your axioms. We can certainly define the successor function from the order directly. But I am uncertain how to define $+$ or $\cdot$ from your system. One needs to have a pairing function. Perhaps one can hope to undertake coding via your set axiom, by describing sets with properties that would support increasing levels of coding, and then proving via induction that the coding always extends, and in this way getting the arithmetic as coded in bounded segments. But I am worried that perhaps the system is too weak to undertake this.