Constructivity and Piecewise Functions

Question

I'm currently exploring homotopy type theory and intuitionistic mathematics.

In constructive/intuitionistic mathematics, 2 features arise:

1. A proof of $\neg \neg A$ is not a proof of $A$.

2. All functions are computable.

The consequences of (1) are not so bad. If we have a proof of $\neg \neg A$, this means that $A$ is not refutable. Thus, we are free to introduce $A$ as an additional assumption without fear of raising a contradiction, but we are also free to not assert $A$ if we choose. Thus, (1) gives us more general systems than classical logic.

However, (2) seems to be a problem. Saying all functions are computable means that any piecewise-defined function on $\mathbb{R}$ is not allowed, since equality on the reals is not decidable. This means no square waves, triangle waves, sawtooth waves, or step functions. I'm a physicist. All of these objects are useful. Piecewise functions are used all the time in physics (particle in a box, particle scattering of a square potential, retarded and advanced propagators, etc.), differential equations (Green's functions for the wave equation, Green's functions in general use non-computable Dirac delta distribution in their definition), and audio/signal processing (square waves, triangle waves, etc.). Not being allowed to have these things seems to be a crippling limitation.

On the other hand, I am told that one can "selectively" reintroduce decidability as an additional axiom. Does this mean that, in intuitionistic type theory, there are 2 different types of real numbers, depending on whether or not we assert that equality is decidable? Supposedly, equality being decidable causes a higher inductive type to collapse down to a set, as all iterated identities are trivial.

Answer 1

For (1), you agree that by adding axioms, you can selectively make some predicate decidable, therefore you have a more general system than classical logic.

You can apply (1) to (2): by adding axioms, you can selectively make some type equality decidable. This may give you a more flexible system to work in, but you loose the property that all functions are effectively computable. At the end it's your choice: you still have a more general system than classical logic.

''The real numbers'' without the Law of Excluded Middle are effectively not exactly the same as ''the real numbers'' with the Law of Excluded Middle; more generally, a theory without LEM is usually not the same as the ''same'' theory with LEM.

Answer 2

Firstly let me remark that the terminology regarding constructive/intuitionistic mathematics is unfortunately not quite consistent. In particular, "Brouwer's intuitionism" is quite a different thing than "intuitionistic logic". From your summary, I have the impression that you're mixing some of the possible flavors.

Most flavors of mathematics can use intuitionistic logic as base. Intuitionistic logic is classical logic without the law of excluded middle (or more precisely: classical logic is intuitionistic logic plus the law of excluded middle). These flavors include, among several others:

1. Classical mathematics, where we add the law of excluded middle (and usually also the axiom of choice).

2. Russian-style constructivism, where any function $\mathbb{N} \to \mathbb{N}$ is computable. Models of Russian-style constructivism are given by realizability theory and the internal language of the effective topos.

3. Brouwer-style mathematics, where any function $\mathbb{R} \to \mathbb{R}$ is continuous. Models of Brouwer-style mathematics are for instance given by the internal language of the topological topos.

4. Martin-Löf type theory, in particular homotopy type theory. (Strictly speaking, these flavors of type theory identify the classically-different notions of "constructing an element" (of some set/type/structure) and "proving a statement". They are not layered upon any kind of logic. Rather, logic is an emerging feature.)

Using just intuitionistic logic, none of the anticlassical dream axioms (like any function being continuous, any function being computable, any function being a polynomial, ...) are provable. (Note that some instances of $\neg\neg A \Rightarrow A$ are provable in intuitionistic logic, namely all those where $A$ happens to be equivalent to the negation of some statement. For instance $A \equiv (x = 0)$, where $x$ is a (Dedekind or Cauchy) real.)

That said, let's work in a setting in which any function $\mathbb{R} \to \mathbb{R}$ is continuous. In such a context we can still define the signum function by the usual case distinction. This is not a contradiction to the axiom that any function $\mathbb{R} \to \mathbb{R}$ is continuous because, without the law of excluded middle, we can't verify that the signum function is actually defined on all of $\mathbb{R}$. It's only defined on $\{ x \in \mathbb{R} \,|\, x < 0 \vee x = 0 \vee x > 0 \}$. So we do have the signum function available, and the fact that we can't prove that its domain is all of $\mathbb{R}$ actually tracks an interesting bit of information. You can learn more about this in a blog post by Andrej Bauer, specifically tailored to physics. Similarly with step functions and the other examples you mention.

(Incidentally, there is no problem at all with triangle waves: These are continuous and can be written down, as functions from the (Dedekind) reals to the (Dedekind) reals, in any flavor of mathematics I personally know.)

Regarding your question on the possible flavors of real numbers: Indeed, without the law of excluded middle or the axiom of (countable) choice, several of the familiar constructions cannot any longer be shown to coincide. For instance, in many models of intuitionistic logic, the Cauchy reals are a proper subset of the Dedekind reals. (In the effective topos they happen to coincide.) This recently came up in a different thread.

However, the principle "any real number is zero or not zero" is quite strong and not part of any of the several flavors of constructive mathematics. When phrased about Cauchy reals, it is equivalent to the limited principle of omniscience. I know only two flavors of mathematics where it holds: in classical mathematics (whether expressed in a set-theoretical framework or a type-theoretical one); and internally to a variant of the effective topos not built using Turing machines but using the infinite time Turing machines by Hamkins and Lewis.

Answer 3

Just to add a bit to the answers that are already here:

1. As was noted, "all functions are computable" is not a theorem of "neutral" constructive mathematics. It is a meta-theoretic property of neutral constructive mathematics that all definable functions are computable, which makes it consistent to add as an additional axiom that every function is computable, if desired.

2. The other answers have pointed out several ways to deal with functions like step functions that cannot be defined constructively as total functions on the real numbers. My own inclination, if I needed to deal with such things constructively, would be to treat them as distributions rather than functions (of course the Dirac delta "function" is not a real function even in classical mathematics). I don't know of a constructive development of distribution theory offhand, but Bishop-Bridges original Constructive Analysis does a good deal of measure theory.

3. The decidability of equality on the reals, as an axiom that can be added to constructive mathematics, is at least noticeably weaker than LEM, so it doesn't land you all the way back in classical mathematics. According to this page, decidability of equality for Cauchy reals is even weaker than the Limited Principle of Omniscience. (Decidability of equality for all sets, however, is equivalent to LEM; just apply it to the set of truth values.)

4. Homotopy type theory is not necessarily at all constructive: it is perfectly consistent with LEM, as long as LEM is formulated correctly to refer only to propositions, i.e. homotopy (-1)-types, which are contractible if inhabited. This sort of LEM corresponds to decidable equality for sets, i.e. homotopy 0-types, whose path-types are all propositions. It is true that there is a stronger sort of "decidable equality" that forces a type to be a set, but the conclusion to be drawn from this is not that homotopy type theory is inconsistent with LEM but rather that the correct version of LEM in homotopy type theory is the one that is only about propositions.

Answer 4

You do have piecewise defined continuous functions on $\mathbb{R}$, even without decidable comparison on the real numbers.

In Bishop's constructive mathematics, the common base to both classical and intuitionistic mathematics, the real numbers come with the usual functions $\max : \mathbb{R} \to \mathbb{R} \to \mathbb{R}$ and $abs : \mathbb{R}\to\mathbb{R} $. $\max(x,y)$ is not defined by direct comparison of $x$ and $y$, it rather considers Cauchy sequences of rational numbers that converge to $x$ and $y$, and forms the Cauchy sequence of the maximums of the rational numbers (which are decidable).

For any real numbers $l$ and $\varepsilon >0$, this allows you to define the continuous Heaviside function $$ H_{l,\varepsilon}(x) \; = \; \left|\frac{x - l}{\varepsilon}\right| - \left|\frac{x - l}{\varepsilon} - 1\right| + 1 $$ This function equals 0 before $l$, 2 after $l+\varepsilon$ and is linear in between. By linear combinations of those, you get all piecewise linear continuous functions.

This happens often in constructive mathematics : classical theorems are replaced by constructive approximations, to an arbitrary $\varepsilon$. As a physicist, those approximations on thin frontier domains shouldn't bother you too much.