Abstract
Around 1870, Cantor demonstrated that the cardinal of the set ℝ of the reals is strictly greater than that of the set ℕ of the integers ; in other words, that continuous infinity (ℝ) is greater than countable infinity (ℕ). He states the continuum hypothesis (HC) : there is no intermediate cardinal between ℕ and ℝ. This conjecture remained open for a long time, so much so that in 1901 Hilbert made it the first in his list of 20 great mathematical problems. In 1938, Gödel showed that HC is consistent with set theory : it can be taken as an axiom because its negation cannot be demonstrated. In 1964, Cohen established that HC is not demonstrable because its negation is consistent. The continuum hypothesis is therefore independent of set theory.
For his demonstration, Cohen invented a new model-building technique, forcing, which enables new sets to be added to an existing model and their properties to be checked via finite approximations : forcing conditions. Since 2009, the work of Krivine, Miquel, Rieg, Jaber, Tabareau and Sozeau has led to a completely different presentation of forcing, internalized in type theory in the form of transformations of propositions and their proof terms, in the style of the doubly negative translations of the4th lecture. These transformations help us to imagine the computational content of the forcing technique. Thus, intuitionistic forcing as presented by Jaber et al. can be seen as a monadic transformation, in the sense of the5th lecture, to a monad of asynchronous inputs where each term can at any time receive more data from the outside.
By specializing the previous results to forcing conditions that are just integers, we obtain a modal logic, called the internal logic of tree topos by Birkedal et al. which allows us to define general (non-algebraic) recursive types, while delving by translation into type theory. This ties in with the ideas of step-indexing, the subject of the next lecture.
