Skip to main content
added 60 characters in body
Source Link
Christopher King
  • 7.1k
  • 1
  • 36
  • 69

Let $a, b, c \in \mathbb R$ such that $a \le b \le c$. Let $S$ be some set and $f, g : [a, c] \to S$ be functions. As a follow up to When can a function defined on $[a, b] \cup [b, c]$ be constructively extended to a function defined on $[a, c]$?, when does $$\forall x \in [a,b] \cup [b,c]. f(x) = g(x)$$ imply that $f = g$?


If $S = \mathbb R$, it is true.
Proof: Let $x \in [a,c]$. Assume that $f(x)$ does not equal $g(x)$. Assume $x < b$. Thus $x \in [a,b]$, implying $f(x) = g(x)$, a contradiction. Thus $b \le x$, implying $x \in [b,c]$, implying $f(x) = g(x)$, a contradiction. Thus $f(x)$ does not not equal $g(x)$. Since $\mathbb R$ has stable equality, $f(x)$ equals $g(x)$. $\square$

This of course applies for any $S \subseteq \mathbb R$ as well. In fact, this proof works for any $S$ with stable equality.

On the other hand, there are examples where the property is constructively unprovable.
Proof: Let $o$ be any object, and consider $$S = \{\{o : y \in [a, b] \cup [b, c]\} : y \in [a,c]\}$$ $$f(x) = \{o : x \in [a,b] \cup [b,c]\}$$ $$g(x) = \{o : b \in [a,b] \cup [b,c]\} = \{o\}$$

Then for all $x \in [a,b] \cup [b,c]$, we have $f(x) = \{o\} = g(x)$. But $f = g$ implies that for any $x \in [a,c]$ we have $o \in \{o : x \in [a,b] \cup [b,c]\}$, implying $x \in [a,b] \cup [b,c]$. Thus $[a,c] = [a,b] \cup [b,c]$, implying the analytic LLPO is provable. But the analytic LLPO is constructively taboo, and thus $f = g$ is unprovable. $\square$

This of course also applies to any superset of $S$, such as $\mathcal P(\{o\})$. (This example was inspired by Gro-Tsen's answer.)

Let $a, b, c \in \mathbb R$ such that $a \le b \le c$. Let $S$ be some set and $f, g : [a, c] \to S$ be functions. As a follow up to When can a function defined on $[a, b] \cup [b, c]$ be constructively extended to a function defined on $[a, c]$?, when does $$\forall x \in [a,b] \cup [b,c]. f(x) = g(x)$$ imply that $f = g$?


If $S = \mathbb R$, it is true.
Proof: Let $x \in [a,c]$. Assume that $f(x)$ does not equal $g(x)$. Assume $x < b$. Thus $x \in [a,b]$, implying $f(x) = g(x)$, a contradiction. Thus $b \le x$, implying $x \in [b,c]$, implying $f(x) = g(x)$, a contradiction. Thus $f(x)$ does not not equal $g(x)$. Since $\mathbb R$ has stable equality, $f(x)$ equals $g(x)$. $\square$

This of course applies for any $S \subseteq \mathbb R$ as well.

On the other hand, there are examples where the property is constructively unprovable.
Proof: Let $o$ be any object, and consider $$S = \{\{o : y \in [a, b] \cup [b, c]\} : y \in [a,c]\}$$ $$f(x) = \{o : x \in [a,b] \cup [b,c]\}$$ $$g(x) = \{o : b \in [a,b] \cup [b,c]\} = \{o\}$$

Then for all $x \in [a,b] \cup [b,c]$, we have $f(x) = \{o\} = g(x)$. But $f = g$ implies that for any $x \in [a,c]$ we have $o \in \{o : x \in [a,b] \cup [b,c]\}$, implying $x \in [a,b] \cup [b,c]$. Thus $[a,c] = [a,b] \cup [b,c]$, implying the analytic LLPO is provable. But the analytic LLPO is constructively taboo, and thus $f = g$ is unprovable. $\square$

This of course also applies to any superset of $S$, such as $\mathcal P(\{o\})$. (This example was inspired by Gro-Tsen's answer.)

Let $a, b, c \in \mathbb R$ such that $a \le b \le c$. Let $S$ be some set and $f, g : [a, c] \to S$ be functions. As a follow up to When can a function defined on $[a, b] \cup [b, c]$ be constructively extended to a function defined on $[a, c]$?, when does $$\forall x \in [a,b] \cup [b,c]. f(x) = g(x)$$ imply that $f = g$?


If $S = \mathbb R$, it is true.
Proof: Let $x \in [a,c]$. Assume that $f(x)$ does not equal $g(x)$. Assume $x < b$. Thus $x \in [a,b]$, implying $f(x) = g(x)$, a contradiction. Thus $b \le x$, implying $x \in [b,c]$, implying $f(x) = g(x)$, a contradiction. Thus $f(x)$ does not not equal $g(x)$. Since $\mathbb R$ has stable equality, $f(x)$ equals $g(x)$. $\square$

This of course applies for any $S \subseteq \mathbb R$ as well. In fact, this proof works for any $S$ with stable equality.

On the other hand, there are examples where the property is constructively unprovable.
Proof: Let $o$ be any object, and consider $$S = \{\{o : y \in [a, b] \cup [b, c]\} : y \in [a,c]\}$$ $$f(x) = \{o : x \in [a,b] \cup [b,c]\}$$ $$g(x) = \{o : b \in [a,b] \cup [b,c]\} = \{o\}$$

Then for all $x \in [a,b] \cup [b,c]$, we have $f(x) = \{o\} = g(x)$. But $f = g$ implies that for any $x \in [a,c]$ we have $o \in \{o : x \in [a,b] \cup [b,c]\}$, implying $x \in [a,b] \cup [b,c]$. Thus $[a,c] = [a,b] \cup [b,c]$, implying the analytic LLPO is provable. But the analytic LLPO is constructively taboo, and thus $f = g$ is unprovable. $\square$

This of course also applies to any superset of $S$, such as $\mathcal P(\{o\})$. (This example was inspired by Gro-Tsen's answer.)

Source Link
Christopher King
  • 7.1k
  • 1
  • 36
  • 69

Constructively, when do functions that agree on $[a, b] \cup [b, c]$ also agree on $[a,c]$?

Let $a, b, c \in \mathbb R$ such that $a \le b \le c$. Let $S$ be some set and $f, g : [a, c] \to S$ be functions. As a follow up to When can a function defined on $[a, b] \cup [b, c]$ be constructively extended to a function defined on $[a, c]$?, when does $$\forall x \in [a,b] \cup [b,c]. f(x) = g(x)$$ imply that $f = g$?


If $S = \mathbb R$, it is true.
Proof: Let $x \in [a,c]$. Assume that $f(x)$ does not equal $g(x)$. Assume $x < b$. Thus $x \in [a,b]$, implying $f(x) = g(x)$, a contradiction. Thus $b \le x$, implying $x \in [b,c]$, implying $f(x) = g(x)$, a contradiction. Thus $f(x)$ does not not equal $g(x)$. Since $\mathbb R$ has stable equality, $f(x)$ equals $g(x)$. $\square$

This of course applies for any $S \subseteq \mathbb R$ as well.

On the other hand, there are examples where the property is constructively unprovable.
Proof: Let $o$ be any object, and consider $$S = \{\{o : y \in [a, b] \cup [b, c]\} : y \in [a,c]\}$$ $$f(x) = \{o : x \in [a,b] \cup [b,c]\}$$ $$g(x) = \{o : b \in [a,b] \cup [b,c]\} = \{o\}$$

Then for all $x \in [a,b] \cup [b,c]$, we have $f(x) = \{o\} = g(x)$. But $f = g$ implies that for any $x \in [a,c]$ we have $o \in \{o : x \in [a,b] \cup [b,c]\}$, implying $x \in [a,b] \cup [b,c]$. Thus $[a,c] = [a,b] \cup [b,c]$, implying the analytic LLPO is provable. But the analytic LLPO is constructively taboo, and thus $f = g$ is unprovable. $\square$

This of course also applies to any superset of $S$, such as $\mathcal P(\{o\})$. (This example was inspired by Gro-Tsen's answer.)