When I originally posted the question, my colleague Jim Schmerl and I had just discovered a major gap (as well as a fix for the gap) in the proof of a "classical" characterization (1975) by Barwise and Schlipf of recursively saturated models of PA (Peano arithmetic). This result of Barwise and Schlipf inaugurated the study of recursivey saturated models of PA, a topic that boasts a rich literature.

More specifically, the aforementioned Barwise-Schlipf theorem states:

Theorem. The following are equivalent for a nonstandard model $M$ of PA:

(1) $M$ is recursively saturated.

(2) There is $\mathfrak{X}$ such that $(M,\mathfrak{X})$ satisfies $\Delta^1_1$-Comprehension.

This recently published paper of Schmerl and me shows that the Barwise-Schlipf proof of $(2)\implies(1)$ has a serious gap. This problematic direction is established via an alternative argument in our paper uses a coding method introduced by Kaufmann and Schmerl (1984).

For nonexperts: this recent note by John Baez on recursive saturation sings the praises of recursively saturated models of PA.

When I originally posted the question, my colleague Jim Schmerl and I had just discovered a major gap (as well as a fix for the gap) in the proof of a "classical" characterization (1975) by Barwise and Schlipf of recursively saturated models of PA (Peano arithmetic). This result of Barwise and Schlipf inaugurated the study of recursivey saturated models of PA, a topic that boasts a rich literature.

More specifically, the aforementioned Barwise-Schlipf theorem states:

Theorem. The following are equivalent for a nonstandard model $M$ of PA:

(1) $M$ is recursively saturated.

(2) There is $\mathfrak{X}$ such that $(M,\mathfrak{X})$ satisfies $\Delta^1_1$-Comprehension.

This recently published paper of Schmerl and me shows that the Barwise-Schlipf proof of $(2)\implies(1)$ has a serious gap. This problematic direction is established via an alternative argument in our paper using a coding method introduced by Kaufmann and Schmerl (1984).

For nonexperts: this recent note by John Baez on recursive saturation sings the praises of recursively saturated models of PA.

When I originally posted the question, my colleague Jim and Schmerl and I had just discovered a major gap (as well as a fix for the gap) in the proof of a "classical" characterization (1975) by Barwise and Schlipf of recursively saturated models of PA (Peano arithmetic). This result of Barwise and Schlipf inaugurated the study of recursivey saturated models of PA, a topic that boasts a rich literature.

More specifically, the aforementioned Barwise-Schlipf theorem states:

Theorem. The following are equivalent for a nonstandard model $M$ of PA:

(1) $M$ is recursively saturated.

(2) There is $\mathfrak{X}$ such that $(M,\mathfrak{X})$ satisfies $\Delta^1_1$-Comprehension.

This recently published paper of Schmerl and me shows that the Barwise-Schlipf proof of $(2)\implies(1)$ has a serious gap. This problematic direction is established in our paper uses a coding method introduced by Kaufmann and Schmerl (1984).

For nonexperts: this recent note by John Baez on recursive saturation sings the praises of recursively saturated models of PA.

When I originally posted the question, my colleague Jim Schmerl and I had just discovered a major gap (as well as a fix for the gap) in the proof of a "classical" characterization (1975) by Barwise and Schlipf of recursively saturated models of PA (Peano arithmetic). This result of Barwise and Schlipf inaugurated the study of recursivey saturated models of PA, a topic that boasts a rich literature.

More specifically, the aforementioned Barwise-Schlipf theorem states:

Theorem. The following are equivalent for a nonstandard model $M$ of PA:

(1) $M$ is recursively saturated.

(2) There is $\mathfrak{X}$ such that $(M,\mathfrak{X})$ satisfies $\Delta^1_1$-Comprehension.

This recently published paper of Schmerl and me shows that the Barwise-Schlipf proof of $(2)\implies(1)$ has a serious gap. This problematic direction is established via an alternative argument in our paper uses a coding method introduced by Kaufmann and Schmerl (1984).

For nonexperts: this recent note by John Baez on recursive saturation sings the praises of recursively saturated models of PA.