Skip to main content
Name of reference; TeX -> Unicode quotes; `\label`+`\eqref`
Source Link
LSpice
  • 12.9k
  • 4
  • 45
  • 69

"at "At most one" versus "at most finitely many"

As shown in Simpson's excellent SOSOASubsystems of Second Order Arithmetic, the 'big five'‘big five’ system ATR$_0$ from second-order reverse mathematics is equivalent to the following principle:

For arithmetical $\varphi$ such that $(\forall n)(\exists \text{ at most one } X)\varphi(X, n)$, there is $Z$ such that $(\forall m)(m\in Z\leftrightarrow (\exists X)\varphi(X,m))$.

My question is whether this 'at‘at most one'one’ comprehension principle is also equivalent to the following `at‘at most finitely many'many’ principle, where $w^{1^*}$ is a finite sequence of sets of length $|w|$$\lvert w\rvert$.

For arithmetical $\varphi$ such that $$ (\forall n)(\exists w^{1^*})(\forall X)\Big[\varphi(X, n)\rightarrow (\exists i< |w|)(X=w(i))\Big], \quad (*) $$$$ (\forall n)(\exists w^{1^*})(\forall X)\Bigl[\varphi(X, n)\rightarrow (\exists i< \lvert w\rvert)(X=w(i))\Bigr],\tag{*}\label{star} $$ there is $Z$ such that $(\forall m)(m\in Z\leftrightarrow (\exists X)\varphi(X,m))$.

Note that the condition $(*)$\eqref{star} guarantees that there are only finitely many $X$ satisfying $\varphi(X,n)$, for fixed $n$.

"at most one" versus "at most finitely many"

As shown in Simpson's excellent SOSOA, the 'big five' system ATR$_0$ from second-order reverse mathematics is equivalent to the following principle:

For arithmetical $\varphi$ such that $(\forall n)(\exists \text{ at most one } X)\varphi(X, n)$, there is $Z$ such that $(\forall m)(m\in Z\leftrightarrow (\exists X)\varphi(X,m))$.

My question is whether this 'at most one' comprehension principle is also equivalent to the following `at most finitely many' principle, where $w^{1^*}$ is a finite sequence of sets of length $|w|$.

For arithmetical $\varphi$ such that $$ (\forall n)(\exists w^{1^*})(\forall X)\Big[\varphi(X, n)\rightarrow (\exists i< |w|)(X=w(i))\Big], \quad (*) $$ there is $Z$ such that $(\forall m)(m\in Z\leftrightarrow (\exists X)\varphi(X,m))$.

Note that the condition $(*)$ guarantees that there are only finitely many $X$ satisfying $\varphi(X,n)$, for fixed $n$.

"At most one" versus "at most finitely many"

As shown in Simpson's excellent Subsystems of Second Order Arithmetic, the ‘big five’ system ATR$_0$ from second-order reverse mathematics is equivalent to the following principle:

For arithmetical $\varphi$ such that $(\forall n)(\exists \text{ at most one } X)\varphi(X, n)$, there is $Z$ such that $(\forall m)(m\in Z\leftrightarrow (\exists X)\varphi(X,m))$.

My question is whether this ‘at most one’ comprehension principle is also equivalent to the following ‘at most finitely many’ principle, where $w^{1^*}$ is a finite sequence of sets of length $\lvert w\rvert$.

For arithmetical $\varphi$ such that $$ (\forall n)(\exists w^{1^*})(\forall X)\Bigl[\varphi(X, n)\rightarrow (\exists i< \lvert w\rvert)(X=w(i))\Bigr],\tag{*}\label{star} $$ there is $Z$ such that $(\forall m)(m\in Z\leftrightarrow (\exists X)\varphi(X,m))$.

Note that the condition \eqref{star} guarantees that there are only finitely many $X$ satisfying $\varphi(X,n)$, for fixed $n$.

Source Link
Sam Sanders
  • 4.4k
  • 1
  • 21
  • 38

"at most one" versus "at most finitely many"

As shown in Simpson's excellent SOSOA, the 'big five' system ATR$_0$ from second-order reverse mathematics is equivalent to the following principle:

For arithmetical $\varphi$ such that $(\forall n)(\exists \text{ at most one } X)\varphi(X, n)$, there is $Z$ such that $(\forall m)(m\in Z\leftrightarrow (\exists X)\varphi(X,m))$.

My question is whether this 'at most one' comprehension principle is also equivalent to the following `at most finitely many' principle, where $w^{1^*}$ is a finite sequence of sets of length $|w|$.

For arithmetical $\varphi$ such that $$ (\forall n)(\exists w^{1^*})(\forall X)\Big[\varphi(X, n)\rightarrow (\exists i< |w|)(X=w(i))\Big], \quad (*) $$ there is $Z$ such that $(\forall m)(m\in Z\leftrightarrow (\exists X)\varphi(X,m))$.

Note that the condition $(*)$ guarantees that there are only finitely many $X$ satisfying $\varphi(X,n)$, for fixed $n$.