KnowledgeBase » SEMINAR » ID = 735

There Are No Discontinuous Real Functions

by Mark Bickford, Vincent Rahli
2014

Brouwer stated a continuity principle (CP) for total functionals
that map functions (int -> int) to numbers (int).

There are various ways to state CP in type theory.
As recently shown by Bauer and Escardo, some versions of CP are inconsistent with type theory (i.e. using them we can prove False).

However, using the Nuprl in Coq model, Vincent Rahli has just finished proving that a "squashed" version of CP
is true in Nuprl's type theory.

Since the "squashed" version of CP is weaker, what can we use it for?

Using Bishop's definition of the constructive real numbers, and given a function f of type Real -> Real, and a real number x, we can not prove that f is continuous at x,but we can prove that f is not discontinuous at x!

In the seminar we will go through Escardo's proof that the strong CP is false (in any type theory like Nuprl, Coq, or Agda). Then Vincent will discuss how he showed that the squashed CP is true in Nuprl, and Mark will discuss how that can be used to prove that there are no
discontinuous real functions.