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 ADecidableQuantificationOverTheNaturals 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}