Forcing for Second-Order Logic

Forcing is a fundamental set-theoretic technique, with which many independence results can be established. A famous example is the independence of the continuum hypothesis in ZFC set theory. Forcing is also well-known to be complex, and therefore difficult to master. Here, we provide a gentle introduction of forcing, by developing forcing for second-order logic. Second-order logic can be interpreted as a rudimentary kind of set theory. Although very limited as a theory of sets, second-order logic is rich enough to capture a form of the continuum hypothesis, as well as the generalized continuum hypothesis, which is slightly easier to state. We develop forcing for second-order logic in the form of possibility semantics, and use this to show that a second-order version of the generalized continuum hypothesis cannot be derived in a standard proof system for second-order logic. Mathematically, the results we obtain in this way are much weaker than standard independence results in set theory. However, as a consequence, we are able to avoid many technical complexities in the presentation of forcing. In this way, we hope that forcing for second-order logic can serve an expository function, of providing an accessible route towards understanding some of the central ideas behind forcing.