Skip to main content
fixed typo
Source Link
Sam Sanders
  • 4.4k
  • 1
  • 21
  • 38

In a nutshell, the reason one uses 'multi-functions', i.e. mappings that do not satisfy the axiom of function extensionality, is that otherwise things would be fairly trivial, as shown essentially by Kohlenbach, building on work by Grilliot.

In more detail, there is a technical result called Grilliot's trick (see [1]) that amounts to

from a discontinuous function on the reals or Baire space, one can compute Kleene's quantifier $\exists^2$, i.e. the Turing jump functional.

Kohlenbach showed that this trick can be formalised in rather weak systems, needing only a small fragment of Goedel's T ([2]). Thus, $\exists^2$ can be computed (via a term in Goedel's T only using primitive recursion for type 1 objects) from any functional $\Phi^{1\rightarrow 1}$ that on input any infinite binary tree $T$, outputs a path $\Phi(T)$ in $T$. The axiom of function extensionality is essential here, as shown in [3].

A similar result holds for any functional that witnesses the intermediate value theorem, the extreme value theorem, etc. In this way, requiring the functionals at hand to be extensional, one obtains many equivalences involving $\exists^2$. This is not the fine-grained picture people are looking for and hence one works with 'multi-functions' for which the output can depend on the representation of the input.

[1] T. J. Grilliot. On effectively discontinuous type-2 objects. J. Symbolic Logic, 36:245–248, 1971.

[2] U. Kohlenbach, Higher order Reverse Mathematics, RM 2001.

[3] U. Kohlenbach, On uniform weak Koenig's lemma.

In a nutshell, the reason one uses 'multi-functions', i.e. mappings that do not satisfy the axiom of function extensionality, is that otherwise things would be fairly trivial, as shown essentially by Kohlenbach, building on work by Grilliot.

In more detail, there is a technical result called Grilliot's trick (see [1]) that amounts to

from a discontinuous function on the reals or Baire space, one can compute Kleene's quantifier $\exists^2$, i.e. the Turing jump functional.

Kohlenbach showed that this trick can be formalised in rather weak systems, needing only a small fragment of Goedel's T ([2]). Thus, $\exists^2$ can be computed (via a term in Goedel's T only using primitive recursion for type 1 objects) from any functional $\Phi^{1\rightarrow 1}$ that on input any infinite binary tree $T$, outputs a path $\Phi(T)$ in $T$. The axiom of function extensionality is essential here, as shown in [3].

A similar result holds for any functional that witnesses the intermediate value theorem, the extreme value theorem, etc. In this way, requiring the functionals at hand to be extensional, one obtains many equivalences involving $\exists^2$. This is not the fine-grained people are looking for and hence one works with 'multi-functions' for which the output can depend on the representation of the input.

[1] T. J. Grilliot. On effectively discontinuous type-2 objects. J. Symbolic Logic, 36:245–248, 1971.

[2] U. Kohlenbach, Higher order Reverse Mathematics, RM 2001.

[3] U. Kohlenbach, On uniform weak Koenig's lemma.

In a nutshell, the reason one uses 'multi-functions', i.e. mappings that do not satisfy the axiom of function extensionality, is that otherwise things would be fairly trivial, as shown essentially by Kohlenbach, building on work by Grilliot.

In more detail, there is a technical result called Grilliot's trick (see [1]) that amounts to

from a discontinuous function on the reals or Baire space, one can compute Kleene's quantifier $\exists^2$, i.e. the Turing jump functional.

Kohlenbach showed that this trick can be formalised in rather weak systems, needing only a small fragment of Goedel's T ([2]). Thus, $\exists^2$ can be computed (via a term in Goedel's T only using primitive recursion for type 1 objects) from any functional $\Phi^{1\rightarrow 1}$ that on input any infinite binary tree $T$, outputs a path $\Phi(T)$ in $T$. The axiom of function extensionality is essential here, as shown in [3].

A similar result holds for any functional that witnesses the intermediate value theorem, the extreme value theorem, etc. In this way, requiring the functionals at hand to be extensional, one obtains many equivalences involving $\exists^2$. This is not the fine-grained picture people are looking for and hence one works with 'multi-functions' for which the output can depend on the representation of the input.

[1] T. J. Grilliot. On effectively discontinuous type-2 objects. J. Symbolic Logic, 36:245–248, 1971.

[2] U. Kohlenbach, Higher order Reverse Mathematics, RM 2001.

[3] U. Kohlenbach, On uniform weak Koenig's lemma.

Source Link
Sam Sanders
  • 4.4k
  • 1
  • 21
  • 38

In a nutshell, the reason one uses 'multi-functions', i.e. mappings that do not satisfy the axiom of function extensionality, is that otherwise things would be fairly trivial, as shown essentially by Kohlenbach, building on work by Grilliot.

In more detail, there is a technical result called Grilliot's trick (see [1]) that amounts to

from a discontinuous function on the reals or Baire space, one can compute Kleene's quantifier $\exists^2$, i.e. the Turing jump functional.

Kohlenbach showed that this trick can be formalised in rather weak systems, needing only a small fragment of Goedel's T ([2]). Thus, $\exists^2$ can be computed (via a term in Goedel's T only using primitive recursion for type 1 objects) from any functional $\Phi^{1\rightarrow 1}$ that on input any infinite binary tree $T$, outputs a path $\Phi(T)$ in $T$. The axiom of function extensionality is essential here, as shown in [3].

A similar result holds for any functional that witnesses the intermediate value theorem, the extreme value theorem, etc. In this way, requiring the functionals at hand to be extensional, one obtains many equivalences involving $\exists^2$. This is not the fine-grained people are looking for and hence one works with 'multi-functions' for which the output can depend on the representation of the input.

[1] T. J. Grilliot. On effectively discontinuous type-2 objects. J. Symbolic Logic, 36:245–248, 1971.

[2] U. Kohlenbach, Higher order Reverse Mathematics, RM 2001.

[3] U. Kohlenbach, On uniform weak Koenig's lemma.