📥 Download raw
{-# 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.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.

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 now, 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 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 →
  {!!}

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₀ exists a single entity only 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):

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 = {!!}

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. The following actually adopted definition fixes this issue:

_⇒_ : (L → Set) → (L → Set) → (L → Set)
P ⇒ Q = λ xs → ((ys : L) → P (xs ++ ys) → Q (xs ++ ys))

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

Verifying that the principled definition indeed implies the naive one:

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 = {!!}

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 dobule 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 no P will always hold eventually.

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) = {!!}