Yet more forcing in arithmetic: life in a second-order world

by kamerynwilliams

This was a talk in CUNY’s MoPA seminar.

In previous semesters of this seminar, I have talked about how the technique of forcing, originally developed by Cohen for building models of set theory, can be used to produce models of arithmetic with various properties. In this talk, I will present a forcing proof of Harrington’s theorem on the conservativity of \mathsf{WKL}_0 over \mathsf{RCA}_0. More formally, any countable model of \mathsf{RCA}_0 can be extended to a model of \mathsf{WKL}_0 with the same first-order part. As an immediate corollary, we get that any \Pi^1_1 sentence provable by \mathsf{WKL}_0 is already provable by \mathsf{RCA}_0.