Skip to main content
added 7 characters in body
Source Link
Fedor Pakhomov
  • 6.1k
  • 1
  • 24
  • 27

Let me show that for extensions $T\supseteq\mathsf{ACA}_0$ the usual proof-theoretic ordinal $|T|_{WO}$ coincide with $|T|_{WPO}$ that is the suprema of $\mathsf{o}(X)$, for recursive wpo $X$, for which $T$ proves that $X$ is a wpo. Here $|T|_{WO}$ is the suprema of order types $\mathsf{ot}(X)$ of recursive well-orderings $X$ for which $T$ proves that they are well-orderings.

Since any well-ordering $X$ is a wpo and $\mathsf{o}(X)=\mathsf{ot}(X)$ (and this is provable in $\mathsf{ACA}_0$), we have $|T|_{WO}\le |T|_{WPO}$.

To establish that $|T|_{WO}\ge |T|_{WPO}$ we consider the rank $|T|_{WF}$ that is the suprema of ranks $\mathsf{rk}(X)$ of well-founded recursive binary relations for which $T$ proves well-foundedness. Since in $\mathsf{ACA}_0$ it is possible to prove that any well-founded relation is embeddable into a well-ordering (and for recursive well-founded relation the corresponding well-ordering is recursive as well), we have $|T|_{WF}=|T|_{WO}$. Thus we

Any anti-chain $Q$ in a partial order $X$ determines a downward-closed set $E(Q)=\{x\in X\mid \forall q\in Q(q\not<_X x)\}$. This gives us the partial order $A^{\mathsf{fin}}(X)$ on all finite anti-chains in $X$: $$Q<_{A^{\mathsf{fin}}(X)} P \iff E(Q)\subseteq E(P).$$$$Q\le_{A^{\mathsf{fin}}(X)} P \iff E(Q)\subseteq E(P).$$ The function $E$ is an embedding of $A^{\mathsf{fin}}(X)$ into the inclusion order $C(X)$ on all downward-closed subsets of $X$. It is straightforward to prove that the following isare equivalent:

  1. $X$ is a wpo
  2. $C(X)$ is well-founded
  3. $A^{\mathsf{fin}}(X)$ is well-founded.

And it is easy to see if $X$ is a wpo, then $E$ is an isomorphism of $A^{\mathsf{fin}}(X)$ and $C(X)$. The proofs of both the facts here require only Ramsey theorem for pairs and could be proved in $\mathsf{ACA}_0$. Fairly obviously, any linearization $L$ of $X$ is embeddable into $C(X)$ by the map $x\longmapsto \{y\in X\mid y<_L x\}$. Thus for wpo's $X$ we have $\mathsf{o}(X)\le \mathsf{rk}(C(X))=\mathsf{rk}(A^{\mathsf{fin}})$.

Notice that for recursive orders $X$ the order $A^{\mathsf{fin}}(X)$ is recursive as well. Thus, $|T|_{WPO}\le |T|_{WF}$.

Let me show that for extensions $T\supseteq\mathsf{ACA}_0$ the usual proof-theoretic ordinal $|T|_{WO}$ coincide with $|T|_{WPO}$ that is the suprema of $\mathsf{o}(X)$, for recursive wpo $X$, for which $T$ proves that $X$ is a wpo. Here $|T|_{WO}$ is the suprema of order types $\mathsf{ot}(X)$ of recursive well-orderings $X$ for which $T$ proves that they are well-orderings.

Since any well-ordering $X$ is a wpo and $\mathsf{o}(X)=\mathsf{ot}(X)$ (and this is provable in $\mathsf{ACA}_0$), we have $|T|_{WO}\le |T|_{WPO}$.

To establish that $|T|_{WO}\ge |T|_{WPO}$ we consider the rank $|T|_{WF}$ that is the suprema of ranks $\mathsf{rk}(X)$ of well-founded recursive binary relations for which $T$ proves well-foundedness. Since in $\mathsf{ACA}_0$ it is possible to prove that any well-founded relation is embeddable into a well-ordering (and for recursive well-founded relation the corresponding well-ordering is recursive as well), we have $|T|_{WF}=|T|_{WO}$. Thus we

Any anti-chain $Q$ in a partial order $X$ determines a downward-closed set $E(Q)=\{x\in X\mid \forall q\in Q(q\not<_X x)\}$. This gives us the partial order $A^{\mathsf{fin}}(X)$ on all finite anti-chains in $X$: $$Q<_{A^{\mathsf{fin}}(X)} P \iff E(Q)\subseteq E(P).$$ The function $E$ is an embedding of $A^{\mathsf{fin}}(X)$ into the inclusion order $C(X)$ on all downward-closed subsets of $X$. It is straightforward to prove that the following is equivalent:

  1. $X$ is wpo
  2. $C(X)$ is well-founded
  3. $A^{\mathsf{fin}}(X)$ is well-founded.

And it is easy to see if $X$ is wpo, then $E$ is an isomorphism of $A^{\mathsf{fin}}(X)$ and $C(X)$. The proofs of both the facts here require only Ramsey theorem for pairs and could be proved in $\mathsf{ACA}_0$. Fairly obviously, any linearization $L$ of $X$ is embeddable into $C(X)$ by the map $x\longmapsto \{y\in X\mid y<_L x\}$. Thus for wpo's $X$ we have $\mathsf{o}(X)\le \mathsf{rk}(C(X))=\mathsf{rk}(A^{\mathsf{fin}})$.

Notice that for recursive orders $X$ the order $A^{\mathsf{fin}}(X)$ is recursive as well. Thus, $|T|_{WPO}\le |T|_{WF}$.

Let me show that for extensions $T\supseteq\mathsf{ACA}_0$ the usual proof-theoretic ordinal $|T|_{WO}$ coincide with $|T|_{WPO}$ that is the suprema of $\mathsf{o}(X)$, for recursive wpo $X$, for which $T$ proves that $X$ is a wpo. Here $|T|_{WO}$ is the suprema of order types $\mathsf{ot}(X)$ of recursive well-orderings $X$ for which $T$ proves that they are well-orderings.

Since any well-ordering $X$ is a wpo and $\mathsf{o}(X)=\mathsf{ot}(X)$ (and this is provable in $\mathsf{ACA}_0$), we have $|T|_{WO}\le |T|_{WPO}$.

To establish that $|T|_{WO}\ge |T|_{WPO}$ we consider the rank $|T|_{WF}$ that is the suprema of ranks $\mathsf{rk}(X)$ of well-founded recursive binary relations for which $T$ proves well-foundedness. Since in $\mathsf{ACA}_0$ it is possible to prove that any well-founded relation is embeddable into a well-ordering (and for recursive well-founded relation the corresponding well-ordering is recursive as well), we have $|T|_{WF}=|T|_{WO}$. Thus we

Any anti-chain $Q$ in a partial order $X$ determines a downward-closed set $E(Q)=\{x\in X\mid \forall q\in Q(q\not<_X x)\}$. This gives us the partial order $A^{\mathsf{fin}}(X)$ on all finite anti-chains in $X$: $$Q\le_{A^{\mathsf{fin}}(X)} P \iff E(Q)\subseteq E(P).$$ The function $E$ is an embedding of $A^{\mathsf{fin}}(X)$ into the inclusion order $C(X)$ on all downward-closed subsets of $X$. It is straightforward to prove that the following are equivalent:

  1. $X$ is a wpo
  2. $C(X)$ is well-founded
  3. $A^{\mathsf{fin}}(X)$ is well-founded.

And it is easy to see if $X$ is a wpo, then $E$ is an isomorphism of $A^{\mathsf{fin}}(X)$ and $C(X)$. The proofs of both the facts here require only Ramsey theorem for pairs and could be proved in $\mathsf{ACA}_0$. Fairly obviously, any linearization $L$ of $X$ is embeddable into $C(X)$ by the map $x\longmapsto \{y\in X\mid y<_L x\}$. Thus for wpo's $X$ we have $\mathsf{o}(X)\le \mathsf{rk}(C(X))=\mathsf{rk}(A^{\mathsf{fin}})$.

Notice that for recursive orders $X$ the order $A^{\mathsf{fin}}(X)$ is recursive as well. Thus, $|T|_{WPO}\le |T|_{WF}$.

Source Link
Fedor Pakhomov
  • 6.1k
  • 1
  • 24
  • 27

Let me show that for extensions $T\supseteq\mathsf{ACA}_0$ the usual proof-theoretic ordinal $|T|_{WO}$ coincide with $|T|_{WPO}$ that is the suprema of $\mathsf{o}(X)$, for recursive wpo $X$, for which $T$ proves that $X$ is a wpo. Here $|T|_{WO}$ is the suprema of order types $\mathsf{ot}(X)$ of recursive well-orderings $X$ for which $T$ proves that they are well-orderings.

Since any well-ordering $X$ is a wpo and $\mathsf{o}(X)=\mathsf{ot}(X)$ (and this is provable in $\mathsf{ACA}_0$), we have $|T|_{WO}\le |T|_{WPO}$.

To establish that $|T|_{WO}\ge |T|_{WPO}$ we consider the rank $|T|_{WF}$ that is the suprema of ranks $\mathsf{rk}(X)$ of well-founded recursive binary relations for which $T$ proves well-foundedness. Since in $\mathsf{ACA}_0$ it is possible to prove that any well-founded relation is embeddable into a well-ordering (and for recursive well-founded relation the corresponding well-ordering is recursive as well), we have $|T|_{WF}=|T|_{WO}$. Thus we

Any anti-chain $Q$ in a partial order $X$ determines a downward-closed set $E(Q)=\{x\in X\mid \forall q\in Q(q\not<_X x)\}$. This gives us the partial order $A^{\mathsf{fin}}(X)$ on all finite anti-chains in $X$: $$Q<_{A^{\mathsf{fin}}(X)} P \iff E(Q)\subseteq E(P).$$ The function $E$ is an embedding of $A^{\mathsf{fin}}(X)$ into the inclusion order $C(X)$ on all downward-closed subsets of $X$. It is straightforward to prove that the following is equivalent:

  1. $X$ is wpo
  2. $C(X)$ is well-founded
  3. $A^{\mathsf{fin}}(X)$ is well-founded.

And it is easy to see if $X$ is wpo, then $E$ is an isomorphism of $A^{\mathsf{fin}}(X)$ and $C(X)$. The proofs of both the facts here require only Ramsey theorem for pairs and could be proved in $\mathsf{ACA}_0$. Fairly obviously, any linearization $L$ of $X$ is embeddable into $C(X)$ by the map $x\longmapsto \{y\in X\mid y<_L x\}$. Thus for wpo's $X$ we have $\mathsf{o}(X)\le \mathsf{rk}(C(X))=\mathsf{rk}(A^{\mathsf{fin}})$.

Notice that for recursive orders $X$ the order $A^{\mathsf{fin}}(X)$ is recursive as well. Thus, $|T|_{WPO}\le |T|_{WF}$.