A stepbystep proof of Open Induction by Bar Induction
The purpose of this post is a detailed proof, following Coquand[1], of the Open Induction Principle using DecidableBar Induction[2].
Open induction (OI) is useful when one can not do a proof by usual wellfounded induction, that is, when there is no wellfounded relation that can be used. In such cases, if the space one is in is compact, and the property one wants to prove is open, one can use a nonwellfounded order to do an induction proof. From the computer science perspective, this means one can build a terminating recursive program for computing a property that does not depend on a structurally decreasing criterium of termination.
In this post we concentrate on Cantor space 2^{N}, but it is, in some sense, enough, because every compact space is an image of Cantor space. A member α of 2^{N} is a map N → 2, i.e. an infinite stream of bits, i.e. an infinite branch of the infinite binary tree. α<β if α is “left of” β as a branch of the infinite tree, that is, α<β if they are bit streams which are equal for a finite initial segment and then at some length n of the segment α(n) is “left” while β(n) is “right”. We write αn for the finite initial segment of α of lenght n. Each node in the infinite binary tree corresponds to some initial segment, and viceversa. Each such node, i.e. each finite bit string, is called a basic open. An open, or open subspace, of Cantor space is an arbitrary union of basic opens. Equivalently, an open is determined by a Boolean function G on arbitrary lenght, but finite, bit strings, G : 2^{*} → 2, which is monotone: If s, s′:2^{*}, s is an initial segment of s′, and G(s)=⊤, then also G(s′)=⊤.
∀ α∈2^{N}. ∃ n∈ N. P( 
 n) 
∀ s∈2^{*}. (∀ b∈ 2. Q ⟨ b::s ⟩) → Q s 
Q ⟨ ⟩ 
∀ α. (∀ β<α. β∈ U) → α∈ U (*) 
∀ α. α∈ U. 
Proof. Let α : 2^{N} be given. U is open in 2^{N}, hence given by a mapping G : 2^{*} → 2 which is monotone w.r.t. initial segments: if s is a prefix of t, G s = ⊤ implies G t = ⊤. We say that G bars s with witness k (notation G_{k} s) if all k−bitextensions of s satisfy G.
We define mutually, by (primitive) recursion on finite strings of numbers, two functions f:N^{*} → 2^{*} and acc:N^{*}→ 2:

We set
P(s) := G(f(s)) 
Q(s) := acc(s) → ∃ m. G_{m} f(s) 
and apply bar induction, which gives us a proof of Q(⟨ ⟩), which, since acc(⟨ ⟩)=⊤, gives an m∈ N such that any bitstring with length m satisfies G. Hence, also αm, therefore α∈ U.
The hypotheses of (DBI) are satisfied by the following lemmas.
Proof. We write f(α) for the natural exension of f to infinite sequences. The lemma states that ∀ α∈N^{N}. f(α)∈ U. Let α be given. Apply (*). Let β<f(α), that is, there is some n such that βn = ⟨ ⊥::s ⟩ and ⟨ ⊤::s ⟩ = f(α) n = f(αn) for some s∈2^{*} (of length n−1). By the defining equations of f and app, n>0, s=f(α(n−1)), acc(s) and G_{k}⟨ ⊥::s ⟩, that is, G_{k}βn, for some k. Hence, G(β(n+k)) = ⊤ i.e. β∈ U.
(∀ n∈ N. acc⟨ n::s ⟩ → ∃ m. G_{m} f⟨ n::s ⟩), 
Proof. Since acc(s), also acc⟨ 0::s ⟩, and the hypothesis gives us an m such that G_{m}f⟨ 0::s ⟩, that is, G_{m}⟨ ⊥::f(s) ⟩. This means that acc⟨ m+1::s ⟩, which we use with the hypothesis again to get a k such that G_{k}f⟨ m+1::s ⟩ i.e. G_{k}⟨ acc⟨ m+1::s ⟩::f(s) ⟩ i.e. G_{k}⟨ ⊤::f(s) ⟩. We showed that G bars both ⟨ ⊤::f(s) ⟩ and ⟨ ⊥::f(s) ⟩, which means that G bars f(s) already: G_{max(m,k)}f(s).
Proof. G(f(s)) iff G_{0} f(s).
Comments