Skip to main content
added 544 characters in body
Source Link
Emil Jeřábek
  • 47.9k
  • 4
  • 151
  • 210

The theory of $(\let\ep\varepsilon\ep_0,+,\omega^-)$ is undecidable (I will not mention $0$, $1$, or $<$ in the signature as they are definable). More generally, the same holds for any nonempty class of structures of the form $(\ep_\alpha,+,\omega^-)$, and even $(\mathrm{Ord},+,\omega^-)$, if you can make sense of the theory of the latter structure.

The reason is that it interprets Vaught’s set theory (VS), axiomatized by the schema $$\forall x_1,\dots,x_k\:\exists z\:\forall t\:(t\in z\let\eq\leftrightarrow\eq t=x_1\lor\dots\lor t=x_k)$$ for $k\ge0$ that just says “$\{x_1,\dots,x_k\}$ exists” ($k=0$ gives the empty set). VS is essentially undecidable; see [1] for a discussion of this and related theories.

VS is interpreted in the theory of $(\ep_\alpha,+,\omega^-)$ by taking for $x\in y$ the predicate “$\omega^x$ occurs as one of the terms of the Cantor normal form (CNF) of $y$”, which can be defined by $$x\in y\iff\exists u,v\:(y=u+\omega^x+v\land v<\omega^x).$$ In fact, this gives a direct (i.e., 1-dimensional, unrelativized, with absolute equality) interpretation of the stronger adjunctive set theory (AST) with axioms $$\begin{align*} &\exists z\:\forall t\:t\notin z,\\ &\forall x,y\:\exists z\:\forall t\:(t\in z\eq t\in x\lor t=y), \end{align*}$$ stating that $\varnothing$ and $x\cup\{y\}$ exist. This makes the theory of $(\ep_\alpha,+,\omega^-)$ sequential (see [1] for what that means), and it interprets Robinson’s arithmetic $Q$.

Even better, $(\ep_\alpha,+,\omega^-)$ interprets $(V_\omega,\in)$, and therefore the true arithmetic $(\mathbb N,0,1,+,\cdot,<)$. To see this, let us say $x$ is extensional if no summand in its CNF occurs twice, which can be defined as $$E(x)\iff\neg\exists t,u,v\:(x=u+\omega^t+\omega^t+v\land v<\omega^t),$$ and hereditarily extensional if all ordinals in its recursively expanded CNF are extensional and if it is smaller than $\ep_0$: $$\mathit{HE}(x)\iff\exists z\:\bigl(x\in z\land\forall u\in z\:(E(u)\land u<\omega^u\land\forall v\in u\:v\in z)\bigr)$$ (the formula says “$x$ belongs to a transitive set of non-epsilon extensional elements”). Then the structure of hereditarily extensional elements of $(\ep_\alpha,+,\omega^-)$ with $\in$ is easily seen to be isomorphic to $(V_\omega,\in)$.

Finally, I will not try to write this down formally, but I believe ordinal multiplication is actually definable in $(\ep_\alpha,+,\omega^-)$. The point is that an algorithm for mutiplication of ordinals given in CNF by a finite computation can be described by a formula, using an encoding of finite sets and sequences that we already have. To make this explicit, observe that we can define a pairing function by $\def\p#1{\langle#1\rangle}\p{x,y}=\omega^{x+y}+\omega^x$; then $x\cdot y=z$ can be defined by the formula $$\begin{align*} (x=0\land{}&z=0)\lor{}\\ \exists w\:\bigl[\p{y,z}&\in w\land\forall u,v\:\bigl(\p{u,v}\in w\to\\ &(u=0\land v=0)\\ {}\lor{}&(u=1\land v=x)\\ {}\lor{}&\exists s,t\:(\omega^s\le x<\omega^{s+1}\land t\ne0\land u=\omega^t\land v=\omega^{s+t})\\ {}\lor{}&\exists u',u''<u\:\exists v',v''\\ &\quad(\p{u',v'}\in w\land\p{u'',v''}\in w\land u=u'+u''\land v=v'+v'')\bigr)\bigr] \end{align*}$$

Reference:

[1] Albert Visser, Pairs, sets and sequences in first-order theories, Archive for Mathematical Logic 47 (2008), no. 4, pp. 299–326, doi 10.1007/s00153-008-0087-1.

The theory of $(\let\ep\varepsilon\ep_0,+,\omega^-)$ is undecidable (I will not mention $0$, $1$, or $<$ in the signature as they are definable). More generally, the same holds for any nonempty class of structures of the form $(\ep_\alpha,+,\omega^-)$, and even $(\mathrm{Ord},+,\omega^-)$, if you can make sense of the theory of the latter structure.

The reason is that it interprets Vaught’s set theory (VS), axiomatized by the schema $$\forall x_1,\dots,x_k\:\exists z\:\forall t\:(t\in z\let\eq\leftrightarrow\eq t=x_1\lor\dots\lor t=x_k)$$ for $k\ge0$ that just says “$\{x_1,\dots,x_k\}$ exists” ($k=0$ gives the empty set). VS is essentially undecidable; see [1] for a discussion of this and related theories.

VS is interpreted in the theory of $(\ep_\alpha,+,\omega^-)$ by taking for $x\in y$ the predicate “$\omega^x$ occurs as one of the terms of the Cantor normal form (CNF) of $y$”, which can be defined by $$x\in y\iff\exists u,v\:(y=u+\omega^x+v\land v<\omega^x).$$ In fact, this gives a direct (i.e., 1-dimensional, unrelativized, with absolute equality) interpretation of the stronger adjunctive set theory (AST) with axioms $$\begin{align*} &\exists z\:\forall t\:t\notin z,\\ &\forall x,y\:\exists z\:\forall t\:(t\in z\eq t\in x\lor t=y), \end{align*}$$ stating that $\varnothing$ and $x\cup\{y\}$ exist. This makes the theory of $(\ep_\alpha,+,\omega^-)$ sequential (see [1] for what that means), and it interprets Robinson’s arithmetic $Q$.

Even better, $(\ep_\alpha,+,\omega^-)$ interprets $(V_\omega,\in)$, and therefore the true arithmetic $(\mathbb N,0,1,+,\cdot,<)$. To see this, let us say $x$ is extensional if no summand in its CNF occurs twice, which can be defined as $$E(x)\iff\neg\exists t,u,v\:(x=u+\omega^t+\omega^t+v\land v<\omega^t),$$ and hereditarily extensional if all ordinals in its recursively expanded CNF are extensional and if it is smaller than $\ep_0$: $$\mathit{HE}(x)\iff\exists z\:\bigl(x\in z\land\forall u\in z\:(E(u)\land u<\omega^u\land\forall v\in u\:v\in z)\bigr)$$ (the formula says “$x$ belongs to a transitive set of non-epsilon extensional elements”). Then the structure of hereditarily extensional elements of $(\ep_\alpha,+,\omega^-)$ with $\in$ is easily seen to be isomorphic to $(V_\omega,\in)$.

Finally, I will not try to write this down formally, but I believe ordinal multiplication is definable in $(\ep_\alpha,+,\omega^-)$. The point is that an algorithm for mutiplication of ordinals given in CNF by a finite computation can be described by a formula, using an encoding of finite sets and sequences that we already have.

Reference:

[1] Albert Visser, Pairs, sets and sequences in first-order theories, Archive for Mathematical Logic 47 (2008), no. 4, pp. 299–326, doi 10.1007/s00153-008-0087-1.

The theory of $(\let\ep\varepsilon\ep_0,+,\omega^-)$ is undecidable (I will not mention $0$, $1$, or $<$ in the signature as they are definable). More generally, the same holds for any nonempty class of structures of the form $(\ep_\alpha,+,\omega^-)$, and even $(\mathrm{Ord},+,\omega^-)$, if you can make sense of the theory of the latter structure.

The reason is that it interprets Vaught’s set theory (VS), axiomatized by the schema $$\forall x_1,\dots,x_k\:\exists z\:\forall t\:(t\in z\let\eq\leftrightarrow\eq t=x_1\lor\dots\lor t=x_k)$$ for $k\ge0$ that just says “$\{x_1,\dots,x_k\}$ exists” ($k=0$ gives the empty set). VS is essentially undecidable; see [1] for a discussion of this and related theories.

VS is interpreted in the theory of $(\ep_\alpha,+,\omega^-)$ by taking for $x\in y$ the predicate “$\omega^x$ occurs as one of the terms of the Cantor normal form (CNF) of $y$”, which can be defined by $$x\in y\iff\exists u,v\:(y=u+\omega^x+v\land v<\omega^x).$$ In fact, this gives a direct (i.e., 1-dimensional, unrelativized, with absolute equality) interpretation of the stronger adjunctive set theory (AST) with axioms $$\begin{align*} &\exists z\:\forall t\:t\notin z,\\ &\forall x,y\:\exists z\:\forall t\:(t\in z\eq t\in x\lor t=y), \end{align*}$$ stating that $\varnothing$ and $x\cup\{y\}$ exist. This makes the theory of $(\ep_\alpha,+,\omega^-)$ sequential (see [1] for what that means), and it interprets Robinson’s arithmetic $Q$.

Even better, $(\ep_\alpha,+,\omega^-)$ interprets $(V_\omega,\in)$, and therefore the true arithmetic $(\mathbb N,0,1,+,\cdot,<)$. To see this, let us say $x$ is extensional if no summand in its CNF occurs twice, which can be defined as $$E(x)\iff\neg\exists t,u,v\:(x=u+\omega^t+\omega^t+v\land v<\omega^t),$$ and hereditarily extensional if all ordinals in its recursively expanded CNF are extensional and if it is smaller than $\ep_0$: $$\mathit{HE}(x)\iff\exists z\:\bigl(x\in z\land\forall u\in z\:(E(u)\land u<\omega^u\land\forall v\in u\:v\in z)\bigr)$$ (the formula says “$x$ belongs to a transitive set of non-epsilon extensional elements”). Then the structure of hereditarily extensional elements of $(\ep_\alpha,+,\omega^-)$ with $\in$ is easily seen to be isomorphic to $(V_\omega,\in)$.

Finally, ordinal multiplication is actually definable in $(\ep_\alpha,+,\omega^-)$. The point is that an algorithm for mutiplication of ordinals given in CNF by a finite computation can be described by a formula, using an encoding of finite sets and sequences that we already have. To make this explicit, observe that we can define a pairing function by $\def\p#1{\langle#1\rangle}\p{x,y}=\omega^{x+y}+\omega^x$; then $x\cdot y=z$ can be defined by the formula $$\begin{align*} (x=0\land{}&z=0)\lor{}\\ \exists w\:\bigl[\p{y,z}&\in w\land\forall u,v\:\bigl(\p{u,v}\in w\to\\ &(u=0\land v=0)\\ {}\lor{}&(u=1\land v=x)\\ {}\lor{}&\exists s,t\:(\omega^s\le x<\omega^{s+1}\land t\ne0\land u=\omega^t\land v=\omega^{s+t})\\ {}\lor{}&\exists u',u''<u\:\exists v',v''\\ &\quad(\p{u',v'}\in w\land\p{u'',v''}\in w\land u=u'+u''\land v=v'+v'')\bigr)\bigr] \end{align*}$$

Reference:

[1] Albert Visser, Pairs, sets and sequences in first-order theories, Archive for Mathematical Logic 47 (2008), no. 4, pp. 299–326, doi 10.1007/s00153-008-0087-1.

added 3 characters in body
Source Link
Emil Jeřábek
  • 47.9k
  • 4
  • 151
  • 210

The theory of $(\let\ep\epsilon\ep_0,+,\omega^-)$$(\let\ep\varepsilon\ep_0,+,\omega^-)$ is undecidable (I will not mention $0$, $1$, or $<$ in the signature as they are definable). More generally, the same holds for any nonempty class of structures of the form $(\ep_\alpha,+,\omega^-)$, and even $(\mathrm{Ord},+,\omega^-)$, if you can make sense of the theory of the latter structure.

The reason is that it interprets Vaught’s set theory (VS), axiomatized by the schema $$\forall x_1,\dots,x_k\:\exists z\:\forall t\:(t\in z\let\eq\leftrightarrow\eq t=x_1\lor\dots\lor t=x_k)$$ for $k\ge0$ that just says “$\{x_1,\dots,x_k\}$ exists” ($k=0$ gives the empty set). VS is essentially undecidable; see [1] for a discussion of this and related theories.

VS is interpreted in the theory of $(\ep_\alpha,+,\omega^-)$ by taking for $x\in y$ the predicate “$\omega^x$ occurs as one of the terms of the Cantor normal form (CNF) of $y$”, which can be defined by $$x\in y\iff\exists u,v\:(y=u+\omega^x+v\land v<\omega^x).$$ In fact, this gives a direct (i.e., 1-dimensional, unrelativized, with absolute equality) interpretation of the stronger adjunctive set theory (AST) with axioms $$\begin{align*} &\exists z\:\forall t\:t\notin z,\\ &\forall x,y\:\exists z\:\forall t\:(t\in z\eq t\in x\lor t=y), \end{align*}$$ stating that $\varnothing$ and $x\cup\{y\}$ exist. This makes the theory of $(\ep_\alpha,+,\omega^-)$ sequential (see [1] for what that means), and it interprets Robinson’s arithmetic $Q$.

Even better, $(\ep_\alpha,+,\omega^-)$ interprets $(V_\omega,\in)$, and therefore the true arithmetic $(\mathbb N,0,1,+,\cdot,<)$. To see this, let us say $x$ is extensional if no summand in its CNF occurs twice, which can be defined as $$E(x)\iff\neg\exists t,u,v\:(x=u+\omega^t+\omega^t+v\land v<\omega^t),$$ and hereditarily extensional if all ordinals in its recursively expanded CNF are extensional and if it is smaller than $\ep_0$: $$\mathit{HE}(x)\iff\exists z\:\bigl(x\in z\land\forall u\in z\:(E(u)\land u<\omega^u\land\forall v\in u\:v\in z)\bigr)$$ (the formula says “$x$ belongs to a transitive set of non-epsilon extensional elements”). Then the structure of hereditarily extensional elements of $(\ep_\alpha,+,\omega^-)$ with $\in$ is easily seen to be isomorphic to $(V_\omega,\in)$.

Finally, I will not try to write this down formally, but I believe ordinal multiplication is definable in $(\ep_\alpha,+,\omega^-)$. The point is that an algorithm for mutiplication of ordinals given in CNF by a finite computation can be described by a formula, using an encoding of finite sets and sequences that we already have.

Reference:

[1] Albert Visser, Pairs, sets and sequences in first-order theories, Archive for Mathematical Logic 47 (2008), no. 4, pp. 299–326, doi 10.1007/s00153-008-0087-1.

The theory of $(\let\ep\epsilon\ep_0,+,\omega^-)$ is undecidable (I will not mention $0$, $1$, or $<$ in the signature as they are definable). More generally, the same holds for any nonempty class of structures of the form $(\ep_\alpha,+,\omega^-)$, and even $(\mathrm{Ord},+,\omega^-)$, if you can make sense of the theory of the latter structure.

The reason is that it interprets Vaught’s set theory (VS), axiomatized by the schema $$\forall x_1,\dots,x_k\:\exists z\:\forall t\:(t\in z\let\eq\leftrightarrow\eq t=x_1\lor\dots\lor t=x_k)$$ for $k\ge0$ that just says “$\{x_1,\dots,x_k\}$ exists” ($k=0$ gives the empty set). VS is essentially undecidable; see [1] for a discussion of this and related theories.

VS is interpreted in the theory of $(\ep_\alpha,+,\omega^-)$ by taking for $x\in y$ the predicate “$\omega^x$ occurs as one of the terms of the Cantor normal form (CNF) of $y$”, which can be defined by $$x\in y\iff\exists u,v\:(y=u+\omega^x+v\land v<\omega^x).$$ In fact, this gives a direct (i.e., 1-dimensional, unrelativized, with absolute equality) interpretation of the stronger adjunctive set theory (AST) with axioms $$\begin{align*} &\exists z\:\forall t\:t\notin z,\\ &\forall x,y\:\exists z\:\forall t\:(t\in z\eq t\in x\lor t=y), \end{align*}$$ stating that $\varnothing$ and $x\cup\{y\}$ exist. This makes the theory of $(\ep_\alpha,+,\omega^-)$ sequential (see [1] for what that means), and it interprets Robinson’s arithmetic $Q$.

Even better, $(\ep_\alpha,+,\omega^-)$ interprets $(V_\omega,\in)$, and therefore the true arithmetic $(\mathbb N,0,1,+,\cdot,<)$. To see this, let us say $x$ is extensional if no summand in its CNF occurs twice, which can be defined as $$E(x)\iff\neg\exists t,u,v\:(x=u+\omega^t+\omega^t+v\land v<\omega^t),$$ and hereditarily extensional if all ordinals in its recursively expanded CNF are extensional and if it is smaller than $\ep_0$: $$\mathit{HE}(x)\iff\exists z\:\bigl(x\in z\land\forall u\in z\:(E(u)\land u<\omega^u\land\forall v\in u\:v\in z)\bigr)$$ (the formula says “$x$ belongs to a transitive set of non-epsilon extensional elements”). Then the structure of hereditarily extensional elements of $(\ep_\alpha,+,\omega^-)$ with $\in$ is easily seen to be isomorphic to $(V_\omega,\in)$.

Finally, I will not try to write this down formally, but believe ordinal multiplication is definable in $(\ep_\alpha,+,\omega^-)$. The point is that an algorithm for mutiplication of ordinals given in CNF by a finite computation can be described by a formula, using an encoding of finite sets and sequences that we already have.

Reference:

[1] Albert Visser, Pairs, sets and sequences in first-order theories, Archive for Mathematical Logic 47 (2008), no. 4, pp. 299–326, doi 10.1007/s00153-008-0087-1.

The theory of $(\let\ep\varepsilon\ep_0,+,\omega^-)$ is undecidable (I will not mention $0$, $1$, or $<$ in the signature as they are definable). More generally, the same holds for any nonempty class of structures of the form $(\ep_\alpha,+,\omega^-)$, and even $(\mathrm{Ord},+,\omega^-)$, if you can make sense of the theory of the latter structure.

The reason is that it interprets Vaught’s set theory (VS), axiomatized by the schema $$\forall x_1,\dots,x_k\:\exists z\:\forall t\:(t\in z\let\eq\leftrightarrow\eq t=x_1\lor\dots\lor t=x_k)$$ for $k\ge0$ that just says “$\{x_1,\dots,x_k\}$ exists” ($k=0$ gives the empty set). VS is essentially undecidable; see [1] for a discussion of this and related theories.

VS is interpreted in the theory of $(\ep_\alpha,+,\omega^-)$ by taking for $x\in y$ the predicate “$\omega^x$ occurs as one of the terms of the Cantor normal form (CNF) of $y$”, which can be defined by $$x\in y\iff\exists u,v\:(y=u+\omega^x+v\land v<\omega^x).$$ In fact, this gives a direct (i.e., 1-dimensional, unrelativized, with absolute equality) interpretation of the stronger adjunctive set theory (AST) with axioms $$\begin{align*} &\exists z\:\forall t\:t\notin z,\\ &\forall x,y\:\exists z\:\forall t\:(t\in z\eq t\in x\lor t=y), \end{align*}$$ stating that $\varnothing$ and $x\cup\{y\}$ exist. This makes the theory of $(\ep_\alpha,+,\omega^-)$ sequential (see [1] for what that means), and it interprets Robinson’s arithmetic $Q$.

Even better, $(\ep_\alpha,+,\omega^-)$ interprets $(V_\omega,\in)$, and therefore the true arithmetic $(\mathbb N,0,1,+,\cdot,<)$. To see this, let us say $x$ is extensional if no summand in its CNF occurs twice, which can be defined as $$E(x)\iff\neg\exists t,u,v\:(x=u+\omega^t+\omega^t+v\land v<\omega^t),$$ and hereditarily extensional if all ordinals in its recursively expanded CNF are extensional and if it is smaller than $\ep_0$: $$\mathit{HE}(x)\iff\exists z\:\bigl(x\in z\land\forall u\in z\:(E(u)\land u<\omega^u\land\forall v\in u\:v\in z)\bigr)$$ (the formula says “$x$ belongs to a transitive set of non-epsilon extensional elements”). Then the structure of hereditarily extensional elements of $(\ep_\alpha,+,\omega^-)$ with $\in$ is easily seen to be isomorphic to $(V_\omega,\in)$.

Finally, I will not try to write this down formally, but I believe ordinal multiplication is definable in $(\ep_\alpha,+,\omega^-)$. The point is that an algorithm for mutiplication of ordinals given in CNF by a finite computation can be described by a formula, using an encoding of finite sets and sequences that we already have.

Reference:

[1] Albert Visser, Pairs, sets and sequences in first-order theories, Archive for Mathematical Logic 47 (2008), no. 4, pp. 299–326, doi 10.1007/s00153-008-0087-1.

Source Link
Emil Jeřábek
  • 47.9k
  • 4
  • 151
  • 210

The theory of $(\let\ep\epsilon\ep_0,+,\omega^-)$ is undecidable (I will not mention $0$, $1$, or $<$ in the signature as they are definable). More generally, the same holds for any nonempty class of structures of the form $(\ep_\alpha,+,\omega^-)$, and even $(\mathrm{Ord},+,\omega^-)$, if you can make sense of the theory of the latter structure.

The reason is that it interprets Vaught’s set theory (VS), axiomatized by the schema $$\forall x_1,\dots,x_k\:\exists z\:\forall t\:(t\in z\let\eq\leftrightarrow\eq t=x_1\lor\dots\lor t=x_k)$$ for $k\ge0$ that just says “$\{x_1,\dots,x_k\}$ exists” ($k=0$ gives the empty set). VS is essentially undecidable; see [1] for a discussion of this and related theories.

VS is interpreted in the theory of $(\ep_\alpha,+,\omega^-)$ by taking for $x\in y$ the predicate “$\omega^x$ occurs as one of the terms of the Cantor normal form (CNF) of $y$”, which can be defined by $$x\in y\iff\exists u,v\:(y=u+\omega^x+v\land v<\omega^x).$$ In fact, this gives a direct (i.e., 1-dimensional, unrelativized, with absolute equality) interpretation of the stronger adjunctive set theory (AST) with axioms $$\begin{align*} &\exists z\:\forall t\:t\notin z,\\ &\forall x,y\:\exists z\:\forall t\:(t\in z\eq t\in x\lor t=y), \end{align*}$$ stating that $\varnothing$ and $x\cup\{y\}$ exist. This makes the theory of $(\ep_\alpha,+,\omega^-)$ sequential (see [1] for what that means), and it interprets Robinson’s arithmetic $Q$.

Even better, $(\ep_\alpha,+,\omega^-)$ interprets $(V_\omega,\in)$, and therefore the true arithmetic $(\mathbb N,0,1,+,\cdot,<)$. To see this, let us say $x$ is extensional if no summand in its CNF occurs twice, which can be defined as $$E(x)\iff\neg\exists t,u,v\:(x=u+\omega^t+\omega^t+v\land v<\omega^t),$$ and hereditarily extensional if all ordinals in its recursively expanded CNF are extensional and if it is smaller than $\ep_0$: $$\mathit{HE}(x)\iff\exists z\:\bigl(x\in z\land\forall u\in z\:(E(u)\land u<\omega^u\land\forall v\in u\:v\in z)\bigr)$$ (the formula says “$x$ belongs to a transitive set of non-epsilon extensional elements”). Then the structure of hereditarily extensional elements of $(\ep_\alpha,+,\omega^-)$ with $\in$ is easily seen to be isomorphic to $(V_\omega,\in)$.

Finally, I will not try to write this down formally, but believe ordinal multiplication is definable in $(\ep_\alpha,+,\omega^-)$. The point is that an algorithm for mutiplication of ordinals given in CNF by a finite computation can be described by a formula, using an encoding of finite sets and sequences that we already have.

Reference:

[1] Albert Visser, Pairs, sets and sequences in first-order theories, Archive for Mathematical Logic 47 (2008), no. 4, pp. 299–326, doi 10.1007/s00153-008-0087-1.