When can a function defined on $[a, b] \cup [b, c]$ be constructively extended to a function defined on $[a, c]$?

Question

Let $a, b, c \in \mathbb R$ such that $a \le b \le c$. Let $S$ be some set and $f : [a, b] \cup [b, c] \to S$ be a function. When can we find a function $g : [a, c] \to S$ that meets the following criteria? $$\forall x \in [a, b] \cup [b, c]. g(x) = f(x)$$

Note that extending the identity function on $[a, b] \cup [b, c]$ to a function $[a, c] \to [a, b] \cup [b, c]$ implies the analytic LLPO, which is not provable in constructive mathematics. However, any function $f : [a, b] \cup [b, c] \to \mathbb R$ can be extended to $g : [a, c] \to \mathbb R$ defined by $g(x) = f(\min(x, b)) - f(b) + f(\max(x, b))$. (This construction works for any $f$ whose codomain is a group.)

In constructive mathematics, given $f$, when are some criteria to determine if a $g$ exists?

---

The motivation for this is the definition of piecewise functions.

Classically, functions defined on $[a, b) \cup [b, c]$ are also defined on $[a, c]$ since classical mathematics can prove those are the same the set. Constructively, this isn't the case.

However, the ability to extend functions should be "good enough" for most practical purposes. We can't really hope to extend functions defined on $[a, b) \cup [b, c]$ (this lets you define discontinuous functions), but often in practice the pieces of the piecewise function actually overlap at their endpoints. Thus, being able to extend functions defined on $[a, b] \cup [b, c]$ would still be very useful.

Answer 1

The question for what $S$ this extension property holds is one I've looked at in the context of computable analysis. I've formulated the notion as follows:

Let $\mathbb{T}$ be the space of ternary truth values, with underlying set $\{\mathbf{t},\mathbf{f},\bot\}$ and representation $\delta_\mathbb{T} : 2^\omega \to \{\mathbf{t},\mathbf{f},\bot\}$ where $\delta_\mathbb{T}(0^\omega) = \bot$, $\delta_\mathbb{T}(0^{2n}1p) = \mathbf{t}$ and $\delta_\mathbb{T}(0^{2n+1}1p) = \mathbf{f}$ for all $n \in \mathbb{N}$, $p \in 2^\omega$. So basically, $\bot$ can change to be $\mathbf{t}$ or $\mathbf{f}$ at any time.

Definition. We call a space $\mathbf{X}$ mergeable if the partial function $$\operatorname{Merge} :\subseteq \mathbb{T} \times \mathbf{X} \times \mathbf{X} \to \mathbf{X}$$ with $$\operatorname{Merge}(\mathbf{t},x,y) = x \quad \operatorname{Merge}(\mathbf{f},x,y) = y \quad \operatorname{Merge}(\bot,x,x) = x$$ is computable.

A space $\mathbf{X}$ being mergeable essentially means that if we can define a function into $\mathbf{X}$ using a single instance of $\mathrm{LLPO}$, we can remove the use of $\mathrm{LLPO}$.

Usually, in computable analysis we concern ourselves with (computably) admissible spaces. Here, the picture is simple:

Theorem: Every computably admissible space is mergeable.

Given that this covers the vast majority of spaces people in computable analysis are interested in, it is unsurprising that the notion hasn't really been investigated much from this perspective. There is another generic argument for why a space might be mergeable:

Theorem: Every computably discrete space is mergeable.

The reasoning in the question leads to the observation that the quotient obtained by identifying $(0,0)$ and $(1,0)$ in $\{0,1\} \times [0,1]$ is not mergeable. Quotients are also how I found some non-mergeable spaces, namely:

Theorem: A quotient of $\mathbb{N}$ is mergeable iff it is computably discrete.

So if we take a non-c.e. set $A \subseteq \mathbb{N}$ and quotient by identifying all elements of $A$, the result is not mergeable.

Answer 2

I am going to work Bishop-style (in particular I am giving myself countable choice, we can try to get rid of it later).

Observe that the Cauchy completion of $[a,b] \cup [b,c]$ is $[a,c]$. For this to hold, it suffices to show that every $x \in [a,c]$ is the Cauchy limit of some sequence $a : \mathbb{N} \to [a,b] \cup [b,c]$. Using countable choice we can find one that satisfies $$a_n = \begin{cases} x - 2^{-n} & \text{if $x < b + 2^{-n-1}$} \\ x + 2^{-n} & \text{if $b - 2^{-n-1} < x$} \end{cases} $$

Now we can use a general extension theorem, for example:

Theorem: If $(M,d)$ is a complete metric space and $f : [a,b] \cup [b,c] \to M$ is locally uniformly continuous then there exists a unique locally uniformly continuous $\bar{f} : [a,c] \to M$ extending $f$.

The proof is standard (I hope).

Answer 3

This is not an answer (since that is already well covered by the other answers), but there's a relevant paper that you will probably be interested in: Palmgren, From Intuitionistic to Point-Free Topology: On the Foundation of Homotopy Theory.

Palmgren's answer to this issue is to instead work in formal topologies, where he showed that for the appropriate definition of continuous function, it is always possible to glue together maps like this, even working constructively (and predicatively).

Answer 4

Here is a stronger version of Andrej Bauer's answer. We can extend $f$ if the codomain is $M$ for some complete metric space $(M,d)$. We don't need $f$ to be continuous, nor do we need any choice principles. As a special case, this includes any $M$ with decidable equality (by setting $d(x,y) = 1_{x \neq y}$).

Let $x \in [a, c]$. Define a multivalued sequence

$$y_n = \begin{cases} f(b) & \text{if $d(f(\min(x, b)), f(\max(x,b))) < 2^{-n}$} \\ f(x) & \text{if $x \in [a,b] \cup [b,c]$} \end{cases}$$

We will show that $y$ is a multivalued Cauchy sequence of elements of $M$. First we must show that it is total. Split cases into cases using cotransitivity on $0 < 2^{-n}$.

Case 1, $d(f(\min(x, b)), f(\max(x,b))) < 2^{-n}$: then $f(b) \in y_n$.

Case 2, $0 < d(f(\min(x, b)), f(\max(x,b)))$: Use cotransitivity to split into cases 2a and 2b.

Case 2a, $d(f(\min(x,b)), f(b)) < d(f(\min(x, b)), f(\max(x,b)))$: Assume $x < b$. Then $d(f(\min(x,b)), f(b)) = d(f(\min(x, b)), f(\max(x,b))) < d(f(\min(x,b)), f(b))$, a contradiction. Thus $b \le x$ and then $x \in [b, c]$, implying $f(x) \in y_n$.

Case 2b, $0 < d(f(\min(x,b)), f(b))$: Assume $b < x$. Then $0 < d(f(\min(x,b)), f(b)) = d(f(b), f(b)) = 0$, a contradiction. Thus $x \le b$ and then $x \in [a, b]$, implying $f(x) \in y_n$.

Next, we show that $y$ is Cauchy. Say that $s \in y_j$ is given by the first line and $t \in y_k$ is given by the second line. The first line means $x \in [a,b] \cup [b,c]$, which implies $d(f(\min(x, b)), f(\max(x,b))) = d(f(x), f(b))$. The second line then implies $d(f(x), f(b)) < 2^{-j} < 2^{-j} + 2^{-k}$.

Thus we have proven that $y$ is a multivalued Cauchy sequence. Every multivalued Cauchy sequence corresponds to a Cauchy net, and thus it has a limit in $M$. We define $g(x)$ to be this limit.

Finally, assume that $x \in [a, b] \cup [b, c]$. Then since $f(x) \in y_n$ for each $n$, the sequence must converge on $f(x)$.

Answer 5

Here is a positive result that's pretty obvious but still worth mentioning since you're just supposing that $S$ is a set: if $S=\Omega$ is the power object of a singleton, i.e., the set of truth values, i.e., the subobject classifier (working in the internal logic of a topos, or in $\mathsf{IZF}$), then every function $[a,b]\cup[b,c] \to \Omega$ can be extended to a function $[a,c] \to \Omega$, because this just means that every subset of $[a,b]\cup[b,c]$ is the restriction of a subset of $[a,c]$, and that's certainly the case, namely, of itself. Moreover, since this extension is canonical, it follows that the extension result also holds when $S = \Omega^I$ is the power object of an arbitrary set $I$.

Answer 6

This is mostly a long comment, not really an answer.

If one slightly modifies the closed interval notation as follows: $$[a,b\Vert = \{ x : a \leq x \not\gt b \}$$ $$\Vert b,c] = \{ x : b \not\gt x \leq c \}$$ Then an exact requirement is that there exist functions $f_1:[a,b\Vert\to S$ and $f_2:\Vert b,c]\to S$ that agree with $f$ on $[a,b]$ and $[b,c]$, respectively. (Note that this implies that $f_1(b) = f_2(b)$.)

This is implied by local uniform continuity (as explained by Andrej Bauer), and it is trivially true assuming LLPO (as explained in the question). It is however completely agnostic to the background hypotheses.