Martin Escardo, 7 May 2014.

For any function f : ℕ∞ → ℕ, it is decidable whether f is non-continuous.

Π(f : ℕ∞ → ℕ). ¬(continuous f) + ¬¬(continuous f).

Based on the paper

"Constructive decidability of classical continuity".
http://www.cs.bham.ac.uk/~mhe/papers/wlpo-and-continuity-revised.pdf

which will appear in MSCS.

The title of this paper is a bit misleading. It should have been
called "Decidability of non-continuity".

\begin{code}

{-# OPTIONS --without-K #-}

module DecidabilityOfNonContinuity where

open import GenericConvergentSequence hiding (_≣_)
open import Two
open import Naturals hiding (_+_)
open import DecidableAndDetachable
open import Equality
open import CurryHoward
open import SetsAndFunctions

Lemma-3·1 : (q : ℕ∞ → ℕ∞ → ₂)
→ decidable((m : ℕ) → ¬((n : ℕ) → q (under m) (under n) ≡ ₁))
Lemma-3·1 q = claim₄
where
A : ℕ∞ → Set
A u = ∀(n : ℕ) → q u (under n) ≡ ₁
claim₀ :  (u : ℕ∞) → decidable(A u)
claim₀ u = Theorem-8·2 (q u)
p : ℕ∞ → ₂
p = π₀ (indicator claim₀)
p-spec : (x : ℕ∞) → (p x ≡ ₀ → A x) × (p x ≡ ₁ → ¬(A x))
p-spec = π₁ (indicator claim₀)
claim₁ : decidable((n : ℕ) → p(under n) ≡ ₁)
claim₁ = Theorem-8·2 p
claim₂ : ((n : ℕ) → ¬ A (under n)) → (n : ℕ) → p(under n) ≡ ₁
claim₂ φ n = Lemma[b≢₀→b≡₁] (λ v → φ n (π₀ (p-spec (under n)) v))
claim₃ : decidable((n : ℕ) → p(under n) ≡ ₁) → decidable((n : ℕ) → ¬(A(under n)))
claim₃ (in₀ f) = in₀ (λ n → π₁ (p-spec (under n)) (f n))
claim₃ (in₁ u) = in₁ (contra-positive claim₂ u)
claim₄ : decidable((n : ℕ) → ¬(A(under n)))
claim₄ = claim₃ claim₁

\end{code}

Omitting the inclusion function, or coercion,

under : ℕ → ℕ∞,

a map f : ℕ∞ → ℕ is called continuous iff

∃ m. ∀ n ≥ m. f n ≡ ∞,

where m and n range over the natural numbers.

The negation of this statement is equivalent to

∀ m. ¬ ∀ n ≥ m. f n ≡ ∞.

We can implement ∀ y ≥ x. A y as ∀ x. A(max x y), so that the
continuity of f amounts to

∃ m. ∀ n. f(max m n) ≡ ∞,

and its negation to

∀ m. ¬ ∀ n. f(max m n) ≡ ∞.

\begin{code}

non-continuous : (ℕ∞ → ℕ) → Set
non-continuous f = ∀(m : ℕ) → ¬(∀(n : ℕ) → f(max (under m) (under n)) ≣ f ∞)

Theorem-3·2 : (f : ℕ∞ → ℕ) → decidable(non-continuous f)
Theorem-3·2 f = Lemma-3·1 ((λ x y → χ≡ (f(max x y)) (f ∞)))

\end{code}

(Maybe) to be continued (see the paper for the moment).

* MP gives that continuity and doubly negated continuity agree.

* WLPO is equivalent to the existence of a non-continuous function ℕ∞ → ℕ.

* ¬WLPO is equivalent to the doubly negated continuity of all functions ℕ∞ → ℕ.

* If MP and ¬WLPO then all functions ℕ∞ → ℕ are continuous.

For future use:

\begin{code}

continuous : (ℕ∞ → ℕ) → Set
continuous f = ∃ \(m : ℕ) → ∀(n : ℕ) → f(max (under m) (under n)) ≡ f ∞

\end{code}