``` {-# OPTIONS --cubical-compatible #-} module Padova2025.Explorations.Forcing.Cohen (X : Set) (x₀ : X) where ``` # Cohen forcing ``` open import Padova2025.ProgrammingBasics.Lists open import Padova2025.ProgrammingBasics.Naturals.Base open import Padova2025.ProgrammingBasics.Naturals.Arithmetic open import Padova2025.ProvingBasics.Negation open import Padova2025.ProvingBasics.Equality.Base open import Padova2025.ProvingBasics.Equality.General open import Padova2025.ProvingBasics.Equality.Lists open import Padova2025.ProvingBasics.Equality.Reasoning.Core open import Padova2025.ProvingBasics.Termination.Ordering open import Padova2025.ProvingBasics.Termination.Gas using (Maybe; nothing; just; lookupMaybe; just-injective) open import Padova2025.ProvingBasics.Connectives.Existential ``` This module is parametrized by a set `X` which we assume to be inhabited by at least one element `x₀`. The purpose of this module is to provide suitable definitions so that we can explore a forcing extension of the base universe in which a *generic infinite sequence of elements of `X`* exists, i.e. a *generic function `f₀ : ℕ → X`*. This function will turn out to be distinct from every function `ℕ → X` of the base universe; hence Cohen forcing allows us to enlarge the base universe by a new function `ℕ → X` (without changing the naturals or the given type `X`). This new function is *generic* in the sense that, for every property `P` of a certain kind, if `f₀` has it, then so does every function `f : ℕ → X` from the base universe (and indeed even every function `ℕ → X` in any forcing extension). ## Approximating by finite lists For approximating an infinite sequence `ℕ → X`, we employ finite lists of elements of `X` as [described in the introduction](Padova2025.Explorations.Forcing.Intro.html#approximating-from-below). ``` L : Set L = List X ``` Given a predicate `P : L → Set`, the next definition introduces a new predicate `∇ P : L → Set`. The intuitive meaning of the assertion `∇ P xs` is that, no matter how the finite approximation `xs` evolves over time to a better approximation `ys`, eventually `P ys` will hold. The operator `∇` is a so-called *modality*, more precisely the *eventually modality*. ``` data ∇ (P : L → Set) : L → Set where -- "P xs holds already now, no refinement required." now : {xs : L} → P xs → ∇ P xs -- "P xs might not hold yet, we need to wait at least for -- xs to grow by one element." later : {xs : L} → ((x : X) → ∇ P (xs ∷ʳ x)) → ∇ P xs ``` As a basic example how this modality can be used, let us show that no matter how the empty list `[]` evolves over time, eventually it will be a list of length at least 3: ``` eventually-length-3 : ∇ (λ xs → length xs ≥ three) [] eventually-length-3 = {!!} ``` Sometimes it is useful to leverage Agda's [instance arguments feature](https://agda.readthedocs.io/en/stable/language/instance-arguments.html) to lighten the notation. By defining... ``` cur : {{L}} → L cur {{xs}} = xs ∇' : ({{L}} → Set) → (L → Set) ∇' P xs = ∇ (λ ys → P {{ys}}) xs withInstance : ({{L}} → Set) → (L → Set) withInstance P xs = P {{xs}} ``` ...we can rewrite the previous example as follows: ``` eventually-length-3' : ∇' (length cur ≥ three) [] eventually-length-3' = {!!} ``` ### Exercise: Bind operator Arriving at a result of the form `∇ P xs` is not a dead end at all; instead, we can reason "under the modality" as follows. ``` _>>=_ : {P Q : L → Set} {xs : L} → ∇ P xs → ({ys : L} → P ys → ∇ Q ys) → ∇ Q xs _>>=_ = {!!} ``` ### Exercise: Eventually arbitrarily long Prove for every number `n` that the empty list eventually evolves to a list of length at least `n`. ``` eventually-length : (n : ℕ) → ∇' (length cur ≥ n) [] eventually-length zero = {!!} eventually-length (succ n) = eventually-length n >>= λ len≥n → {!!} ``` ### Exercise: Monotone predicates Similarly to the above, we can also prove something a bit troubling: Eventually, the length of our approximation will be exactly 3: ``` eventually-length-exactly-3 : ∇' (length cur ≡ three) [] eventually-length-exactly-3 = {!!} ``` Taken very literally, this *is* true: Eventually, there *will* be a moment where the length is 3. But we might expect that once a predicate holds, it'll stay satisfied when we refine our approximation further. To resolve this, we shall endeavour to only only apply the `∇` operator to predicates which are monotone in the following sense: ``` Monotone : (P : L → Set) → Set Monotone P = (xs : L) → P xs → (ys : L) → P (xs ++ ys) Monotone' : (P : {{L}} → Set) → Set Monotone' P = Monotone (withInstance P) ``` We see that while "length is at least 3" is monotone, "length is exactly 3" isn't monotone: ``` monotone-length-3 : Monotone (λ xs → length xs ≥ three) monotone-length-3 = {!!} ``` ``` ¬monotone-length-exactly-3 : ¬ Monotone (λ xs → length xs ≡ three) ¬monotone-length-exactly-3 = {!!} ``` ### Exercise: ∇ preserves monotonicity Once we ensure that some predicate P is monotone, "eventually P" is monotone as well: ``` ∇-monotone : ∀ {P} → Monotone P → Monotone (∇ P) ∇-monotone = {!!} ``` ## Constructing the generic sequence We cannot directly introduce the generic sequence `f₀` as an actual function of type `ℕ → X`, as the type `ℕ → X` contains only the functions of the base universe. But we can define what it means for the equation `f₀ n ≡ x` to hold. From the point of view of the forcing extension, this will be an assertion just like any other and in particular will have a truth value like any other. From the point of view of the base universe however, the truth value of this assertion will depend on the current approximation: ``` f₀[_]≡_ : {{L}} → ℕ → X → Set f₀[ n ]≡ x = lookupMaybe cur n ≡ just x ``` The generic sequence `f₀`, as a single entity, only exists in the forcing extension. To talk about it from the point of view of the base universe, we need to keep track of the current approximation and be prepared to let the current approximation evolve to a better one. For instance, here is how we express that `f₀` is defined on every input (even though no single finite approximation is): ::: More ::: ``` lemma-lookup : {A : Set} → (xs : List A) (n : ℕ) → length xs > n → ∃[ x ] (lookupMaybe xs n ≡ just x) lemma-lookup = {!!} ``` ::: ``` f₀-total : (n : ℕ) → ∇' (∃[ x ] (f₀[ n ]≡ x)) [] f₀-total = {!!} ``` Finally, meticulous readers will also want to formally check that `f₀[ n ]≡ x` is monotone: ``` f₀-≡-monotone : {n : ℕ} {x : X} → Monotone' (f₀[ n ]≡ x) f₀-≡-monotone = {!!} ``` ## Implication in the forcing extension Let `P` and `Q` be two approximation-dependent propositions, i.e. functions of type `L → Set`. What should it mean that `P` implies `Q`? More precisely, given an approximation `xs`, what should it mean that `P` implies `Q` on stage `xs`? One option would be given by the following straightforward definition, which however we reject. ``` _⇒-naive_ : (L → Set) → (L → Set) → (L → Set) P ⇒-naive Q = λ xs → (P xs → Q xs) -- rejected proposal ``` This definition does not account for the possibility of `xs` evolving to better approximations: Even if `P` doesn't hold for the current approximation `xs`, this may change as we refine our approximation. That is, the naive definition doesn't preserve monotonicity: ``` ⇒-naive-not-monotone : ((P Q : L → Set) → Monotone P → Monotone Q → Monotone (P ⇒-naive Q)) → ⊥ ⇒-naive-not-monotone f = f (withInstance (f₀[ zero ]≡ x₀)) (λ _ → ⊥) {!!} {!!} {!!} {!!} {!!} {!!} where lemma₁ : Monotone' ⊥ lemma₁ xs p ys = {!!} lemma₂ : (withInstance (f₀[ zero ]≡ x₀) ⇒-naive (λ _ → ⊥)) [] lemma₂ () ``` The following definition, actually adopted in practice, fixes this issue: ``` _⇒_ : (L → Set) → (L → Set) → (L → Set) P ⇒ Q = λ xs → ((ys : L) → P (xs ++ ys) → Q (xs ++ ys)) ``` ``` ⇒-monotone : {P Q : L → Set} → Monotone P → Monotone Q → Monotone (P ⇒ Q) ⇒-monotone = {!!} ``` Thorsten Altenkirch calls this style of definition *the logic of storytelling*: Assume that, in a fantasy story, the wise wizard offers the counsel "If our enemies cross that bridge, we will lose the war". This assertion does not only mean that if the enemies cross the bridge now, the protagonists will lose the war at that moment. It rather means that if at some point in the future, after the story has continued, the enemies cross the bridge, the protagonists will then lose the war. ## Negation in the forcing extension Similarly, a principled definition of the forcing extension's bottom proposition is *not*... ``` ⫫-naive : L → Set ⫫-naive xs = ⊥ ``` ...but rather: ``` ⫫-principled : L → Set ⫫-principled xs = ∇' ⊥ xs -- fully spelled out: ⫫ xs = ∇ (λ ys → ⊥) xs ``` In other words, `⫫-principled xs` means that (eventually, after sufficiently many refinements) `⊥` will hold. It is a positive way of expressing that the given approximation `xs` is a dead end. Fortunately, as we have assumed (in the very beginning of this file), that the type `X` is inhabited (by some element `x₀`), the two definitions are actually equivalent, and hence we will adopt the simpler one for the remaining development. ``` ⫫ : L → Set ⫫ = ⫫-naive ``` The principled definition indeed implies the naive one; more generally, if `R` holds *eventually*, but doesn't depend on the current approximation, then it must be that it simply holds: ``` escape : {R : Set} {xs : L} → ∇' R xs → R escape = {!!} ``` ``` ⫫-principled-naive : {xs : L} → ⫫-principled xs → ⫫-naive xs ⫫-principled-naive = {!!} ``` With the forcing extension's bottom at hand, we can define the forcing extension's negation operation. ``` infix 3 ⫬_ ⫬_ : (L → Set) → (L → Set) ⫬_ P = P ⇒ ⫫ ``` The following observation is occasionally useful in order to establish that certain double negations hold. ``` dense→negneg : {P : L → Set} → ((xs : L) → ∃[ ys ] P (xs ++ ys)) → (⫬ ⫬ P) [] dense→negneg = {!!} ``` ::: More ::: In fact, a slightly more general result holds: ``` almostdense→negneg : {P : L → Set} → ((xs : L) → ¬ ¬ (∃[ ys ] P (xs ++ ys))) → (⫬ ⫬ P) [] almostdense→negneg = {!!} ``` ``` negneg→almostdense : {P : L → Set} → (⫬ ⫬ P) [] → ((xs : L) → ¬ ¬ (∃[ ys ] P (xs ++ ys))) negneg→almostdense = {!!} ``` ::: This result (which, after a small modification is strengthened to an equivalence in the folded subsection) suggests that double negation in the forcing extension can be pronounced as *potentially*. The assertion `(⫬ ⫬ P) []` means that it is *possible* for any given approximation `xs` to evolve to a list which validates `P`, without presupposing that it must eventually actually evolve to such a list. ## Freshness of the generic sequence Let us prove, up to a double negation, that the generic sequence differs from any given sequence `ℕ → X` of the base universe in at least one term---assuming that there is some fixpoint-free function `step : X → X`. ``` lemma-lookup-last : (xs : L) (a : X) → lookupMaybe (xs ++ (a ∷ [])) (length xs) ≡ just a lemma-lookup-last = {!!} ``` ``` f₀-fresh : (step : X → X) (fixpoint-free : {x : X} → step x ≡ x → ⊥) → (g : ℕ → X) → (⫬ ⫬ (∇' (∃[ n ] (f₀[ n ]≡ step (g n))))) [] f₀-fresh = {!!} ``` ## Genericity of the generic sequence For a sequence `f : ℕ → X` and a number `n`, we define `f ↓ n` to be the list of the first `n` values of `f`, i.e. the list `f zero ∷ f one ∷ … ∷ f (pred n) ∷ []`. ``` _↓_ : (ℕ → X) → ℕ → List X f ↓ zero = [] f ↓ succ n = (f ↓ n) ∷ʳ f n ``` ``` generic⇒actual : {P : L → Set} → (f : ℕ → X) (n : ℕ) → ∇ P (f ↓ n) → ∃[ m ] P (f ↓ m) generic⇒actual = {!!} ``` The following theorem can be read as follows: "If the generic sequence in the forcing extension has property `P`, then so does (a suitable finite prefix) of any actual sequence in the base universe." ``` generic⇒actual₀ : {P : L → Set} → (f : ℕ → X) → ∇ P [] → ∃[ m ] P (f ↓ m) generic⇒actual₀ f = generic⇒actual f zero ``` ## Markov's principle Markov's principle states: If a sequence `ℕ → ℕ` does *not not* have a zero, then it actually has a zero. As an instance of the principle of double negation elimination, Markov's principle is readily available in classical mathematics; it is a taboo in most flavors of constructive mathematics. Specifically, in this section we will explore that Markov's principle is falsified by the generic sequence. Let us first prove that the generic sequence does *not not* have a certain value `z` as one of its terms, as in the antecedent of Markov's principle. (The value `z` is a placeholder for the natural number zero, which is an element of our fixed type `X` only in case `X = ℕ`.) ``` generic-not-not-has-zero : (z : X) → (⫬ ⫬ (∇' (∃[ n ] f₀[ n ]≡ z))) [] generic-not-not-has-zero = {!!} ``` Contrary to what Markov's principle would predict, let us now also prove that it is *not* the case that the generic sequence actually attains the value `z`---assuming that there is some distinct value `w` in `X`. This shows that Markov's principle is not valid for the generic sequence. ``` ↓-constant : (w : X) (n : ℕ) → (λ _ → w) ↓ n ≡ replicate n w ↓-constant = {!!} ``` ``` not-generic-has-zero : (z w : X) → w ≢ z → ¬ (∇' (∃[ n ] f₀[ n ]≡ z) []) not-generic-has-zero z w w≢z p with generic⇒actual₀ (λ _ → w) p ... | n , m , q = go n m {!!} where go : (n m : ℕ) → lookupMaybe (replicate n w) m ≡ just z → ⊥ go zero m = {!!} go (succ n) zero = {!!} go (succ n) (succ m) = {!!} ```