Pierre-Marie Pédrot: The Definitional Side of the Forcing

 

Forcing has been historically introduced by Cohen to prove the independence of the Continuum Hypothesis in set theory. Later, categorical ideas have been used by Lawvere and Tierney to recast this construction in terms of topos of presheaves.

Basing on recent work, we will rather study forcing translations in dependent type theory, which reveal an elegant proof-as-program interpretation through the Curry-Howard correspondence, amounting to the existence of a monotonous global variable. Thanks to a call-by-push-value decomposition, we will synthesize two simply-typed translations: one call-by-value, corresponding to the translation derived from the presheaf construction, and one call-by-name, which is a variant of a presentation given by Krivine and Miquel in classical realizability.

Focusing on the call-by-name translation, we will adapt it to the dependent case and prove that it is compatible with the definitional equality of our system, thus avoiding coherence problems. This allows us to use any category as forcing conditions, which is out of reach with the call-by-value translation. Our construction also exploits the notion of storage operators in order to interpret dependent elimination for inductive types. This is the first example of a dependent type theory with side-effects, clarifying how dependent elimination for inductive types must be restricted in a non-pure setting.

Being implemented as a Coq plugin, this work gives the possibility to formalize easily consistency results. We will finally sketch how the forcing translation may give rise to a computational interpretation of the univalence axiom.