Skip to main content
added 1005 characters in body
Source Link
Carl Mummert
  • 9.7k
  • 1
  • 46
  • 68

$Z_2$ as it is usually viewed is a first-order theory with two sorts, and as such is not categorical. The difference (apart from terminological issues) is entirely in the semantics that are used. In "full" second-order semantics, the set variables quantify over all subsets of the domain, while in first-order "Henkin" semantics each model has a domain for number variables and a second domain for set quantifiers to range over.

There are two things that you might mean by $PA_2$ (I realized this after writing the answer, so I have expanded it). The first option is to have $PA_2$ include the entire second-order induction scheme; let's call that $PA^s_2$. $PA^s_2$ and $ACA$ are indeed equiconsistent. Every model of $ACA$ is already a model of $PA_2$$PA^s_2$, and every model of $PA_2$$PA^2_2$ extends to a model of $ACA$ by just throwing in the definable sets. In fact, this extends any model of $PA_2$$PA^s_2$ to a model of $Z_2$, so these theories are equiconsistent. There is an issue that this could mean "equiconsistent in full second order semantics" or "equiconsistent in first-order semantics", but either way they are pairwise equiconsistent as long as the same semantics is used for both theories.

The other option is that $PA_2$ might just have the single second-order induction axiom $$ (\forall x)[0 \in X \land (\forall n)[n \in X \to n+1\in X] \to (\forall n) n \in X]. $$ Let's call that version $PA^i_2$. Now the semantics matters. In full second-order semantics, any model of $PA^i_2$ is a model of $PA^s_2$, so it extends to a model of $Z_2$. In first-order semantics, $PA^i_2$ is very weak, because without any comprehension axioms the single second-order induction axiom is not very strong in first-order semantics. $PA^i_2$ is (syntactically) a subtheory of $\mathsf{RCA}_0$, one of the weak systems of arithmetic considered in reverse mathematics, and so $PA^i_2$ has a much lower consistency strength than $Z_2$ in the first-order setting.

$Z_2$ as it is usually viewed is a first-order theory with two sorts, and as such is not categorical. The difference (apart from terminological issues) is entirely in the semantics that are used. In "full" second-order semantics, the set variables quantify over all subsets of the domain, while in first-order "Henkin" semantics each model has a domain for number variables and a second domain for set quantifiers to range over.

$PA_2$ and $ACA$ are indeed equiconsistent. Every model of $ACA$ is already a model of $PA_2$, and every model of $PA_2$ extends to a model of $ACA$ by just throwing in the definable sets. In fact, this extends any model of $PA_2$ to a model of $Z_2$, so these theories are equiconsistent. There is an issue that this could mean "equiconsistent in full second order semantics" or "equiconsistent in first-order semantics", but either way they are pairwise equiconsistent as long as the same semantics is used for both theories.

$Z_2$ as it is usually viewed is a first-order theory with two sorts, and as such is not categorical. The difference (apart from terminological issues) is entirely in the semantics that are used. In "full" second-order semantics, the set variables quantify over all subsets of the domain, while in first-order "Henkin" semantics each model has a domain for number variables and a second domain for set quantifiers to range over.

There are two things that you might mean by $PA_2$ (I realized this after writing the answer, so I have expanded it). The first option is to have $PA_2$ include the entire second-order induction scheme; let's call that $PA^s_2$. $PA^s_2$ and $ACA$ are indeed equiconsistent. Every model of $ACA$ is already a model of $PA^s_2$, and every model of $PA^2_2$ extends to a model of $ACA$ by just throwing in the definable sets. In fact, this extends any model of $PA^s_2$ to a model of $Z_2$, so these theories are equiconsistent. There is an issue that this could mean "equiconsistent in full second order semantics" or "equiconsistent in first-order semantics", but either way they are pairwise equiconsistent as long as the same semantics is used for both theories.

The other option is that $PA_2$ might just have the single second-order induction axiom $$ (\forall x)[0 \in X \land (\forall n)[n \in X \to n+1\in X] \to (\forall n) n \in X]. $$ Let's call that version $PA^i_2$. Now the semantics matters. In full second-order semantics, any model of $PA^i_2$ is a model of $PA^s_2$, so it extends to a model of $Z_2$. In first-order semantics, $PA^i_2$ is very weak, because without any comprehension axioms the single second-order induction axiom is not very strong in first-order semantics. $PA^i_2$ is (syntactically) a subtheory of $\mathsf{RCA}_0$, one of the weak systems of arithmetic considered in reverse mathematics, and so $PA^i_2$ has a much lower consistency strength than $Z_2$ in the first-order setting.

Source Link
Carl Mummert
  • 9.7k
  • 1
  • 46
  • 68

$Z_2$ as it is usually viewed is a first-order theory with two sorts, and as such is not categorical. The difference (apart from terminological issues) is entirely in the semantics that are used. In "full" second-order semantics, the set variables quantify over all subsets of the domain, while in first-order "Henkin" semantics each model has a domain for number variables and a second domain for set quantifiers to range over.

$PA_2$ and $ACA$ are indeed equiconsistent. Every model of $ACA$ is already a model of $PA_2$, and every model of $PA_2$ extends to a model of $ACA$ by just throwing in the definable sets. In fact, this extends any model of $PA_2$ to a model of $Z_2$, so these theories are equiconsistent. There is an issue that this could mean "equiconsistent in full second order semantics" or "equiconsistent in first-order semantics", but either way they are pairwise equiconsistent as long as the same semantics is used for both theories.