Skip to main content
added 43 characters in body
Source Link
Sam Sanders
  • 4.4k
  • 1
  • 21
  • 38

Together with previous research by Ulrich Kohlenbach ([1]), a recent paper by Dag Normann and myself ([2]) provides the following pretty sharp answer.

In a nutshell, coding continuous functions in L$_2$, the language of second-order arithmetic, does not change the RM of WKL$_0$, one of the Big Five systems. By contrast, coding Riemann integrable functions (=continuous almost everywhere and bounded) dramatically changes the logical strength of basic theorems, like Arzela's convergence theorem for the Riemann integral from 1885.

In more detail, Kohlenbach shows in [1] that in RCA$_0^\omega +$ WKL, for any third-order $Y:\mathbb{N}^\mathbb{N}\rightarrow \mathbb{N}$ that is continuous on $2^\mathbb{N}$ (via the usual epsilon-delta definition), there is an RM-code $\alpha$ such that $(\forall f \in 2^{\mathbb{N}})(Y(f)=\alpha(f)$. This is based on a construction by Dag Normann and readily generalised to e.g. $[0,1]$.

In this way, as long as WKL is available, it does not matter whether one formulates a given theorem about continuous functions with or without codes.

Now consider Arzela's 1885 convergence theorem for the Riemann (see [0]):

Let $f$ and $(f_{n})_{n\in \mathbb{N}}$ be Riemann integrable on the unit interval and such that $\lim_{n\rightarrow \infty}f_{n}(x)=f(x)$ for all $x\in [0,1]$. If there is $M\in \mathbb{N}$ such that $|f_{n}(x)|\leq M+1$ for all $n\in \mathbb{N}$ and $x\in [0,1]$, then $\lim_{n\rightarrow \infty}\int_{0}^{1}f_{n}(x)dx=\int_{0}^{1}f(x)dx$.

With codes, this theorem is provable in WKL or weaker. Without codes, this theorem can be formulated in third-order arithmetic, but is not provable from third-order comprehension Z$_2^\omega$, which implies full second-order arithmetic Z$_2$. The stronger fourth order system Z$_2^\Omega$ does prove the above convergence theorem.

Here, Z$_2^\omega$ is Kohlenbach's RCA$_0^\omega$ extended with third-order functionals $S_k^2$ that decide $\Pi_k^1$-formulas (the latter formulated in $L_2$). Such functionals $S_k^2$ are highly similar to the functionals $\nu_k$ in [0b, p. 129]. Moreover, Z$_2^\Omega$ is RCA$_0^\omega$ plus Kleene's (fourth order) $\exists^3$. Note that Z$_2^\omega$ and Z$_2^\Omega$ are conservative extensions of Z$_2$.

In this light, the minimal comprehension axioms required to prove Arzela's convergence theorem for the Riemann integral are massively different depending on whether one uses codes. Moreover, we only need to go 'continuous almost everywhere/Riemann integration' for coding to break down: no need to drag in topology or other abstract stuff.

I note that term-by-term integration, which is similar to the above convergence theorem, can already be found in the work of e.g. Dini (1870).

References

[0] Cesaro Arzela, Sulla integrazione per serie, Atti Acc. Lincei Rend., Rome 1 (1885), 532–537

[0b] Wilfried Buchholz, Solomon Feferman, Wolfram Pohlers, and Wilfried Sieg, Iterated inductive definitions and subsystems of analysis, LNM 897, Springer, 1981.

[1] Ulrich Kohlenbach, Foundational and mathematical uses of higher types, Reflections on the foundations of mathematics, Lect. Notes Log., vol. 15, ASL, 2002, pp. 92–116.

[2] Dag Normann and Sam Sanders, On the uncountability of $\mathbb{R}$, arxiv: https://arxiv.org/abs/2007.07560

Together with previous research by Ulrich Kohlenbach ([1]), a recent paper by Dag Normann and myself ([2]) provides the following pretty sharp answer.

In a nutshell, coding continuous functions in L$_2$, the language of second-order arithmetic, does not change the RM of WKL$_0$, one of the Big Five systems. By contrast, coding Riemann integrable functions (=continuous almost everywhere and bounded) dramatically changes the logical strength of basic theorems, like Arzela's convergence theorem for the Riemann integral from 1885.

In more detail, Kohlenbach shows in [1] that in RCA$_0^\omega +$ WKL, for any third-order $Y:\mathbb{N}^\mathbb{N}\rightarrow \mathbb{N}$ that is continuous on $2^\mathbb{N}$ (via the usual epsilon-delta definition), there is an RM-code $\alpha$ such that $(\forall f \in 2^{\mathbb{N}})(Y(f)=\alpha(f)$. This is readily generalised to e.g. $[0,1]$.

In this way, as long as WKL is available, it does not matter whether one formulates a given theorem about continuous functions with or without codes.

Now consider Arzela's 1885 convergence theorem for the Riemann (see [0]):

Let $f$ and $(f_{n})_{n\in \mathbb{N}}$ be Riemann integrable on the unit interval and such that $\lim_{n\rightarrow \infty}f_{n}(x)=f(x)$ for all $x\in [0,1]$. If there is $M\in \mathbb{N}$ such that $|f_{n}(x)|\leq M+1$ for all $n\in \mathbb{N}$ and $x\in [0,1]$, then $\lim_{n\rightarrow \infty}\int_{0}^{1}f_{n}(x)dx=\int_{0}^{1}f(x)dx$.

With codes, this theorem is provable in WKL or weaker. Without codes, this theorem can be formulated in third-order arithmetic, but is not provable from third-order comprehension Z$_2^\omega$, which implies full second-order arithmetic Z$_2$. The stronger fourth order system Z$_2^\Omega$ does prove the above convergence theorem.

Here, Z$_2^\omega$ is Kohlenbach's RCA$_0^\omega$ extended with third-order functionals $S_k^2$ that decide $\Pi_k^1$-formulas (the latter formulated in $L_2$). Such functionals $S_k^2$ are highly similar to the functionals $\nu_k$ in [0b, p. 129]. Moreover, Z$_2^\Omega$ is RCA$_0^\omega$ plus Kleene's (fourth order) $\exists^3$. Note that Z$_2^\omega$ and Z$_2^\Omega$ are conservative extensions of Z$_2$.

In this light, the minimal comprehension axioms required to prove Arzela's convergence theorem for the Riemann integral are massively different depending on whether one uses codes. Moreover, we only need to go 'continuous almost everywhere/Riemann integration' for coding to break down: no need to drag in topology or other abstract stuff.

I note that term-by-term integration, which is similar to the above convergence theorem, can already be found in the work of e.g. Dini (1870).

References

[0] Cesaro Arzela, Sulla integrazione per serie, Atti Acc. Lincei Rend., Rome 1 (1885), 532–537

[0b] Wilfried Buchholz, Solomon Feferman, Wolfram Pohlers, and Wilfried Sieg, Iterated inductive definitions and subsystems of analysis, LNM 897, Springer, 1981.

[1] Ulrich Kohlenbach, Foundational and mathematical uses of higher types, Reflections on the foundations of mathematics, Lect. Notes Log., vol. 15, ASL, 2002, pp. 92–116.

[2] Dag Normann and Sam Sanders, On the uncountability of $\mathbb{R}$, arxiv: https://arxiv.org/abs/2007.07560

Together with previous research by Ulrich Kohlenbach ([1]), a recent paper by Dag Normann and myself ([2]) provides the following pretty sharp answer.

In a nutshell, coding continuous functions in L$_2$, the language of second-order arithmetic, does not change the RM of WKL$_0$, one of the Big Five systems. By contrast, coding Riemann integrable functions (=continuous almost everywhere and bounded) dramatically changes the logical strength of basic theorems, like Arzela's convergence theorem for the Riemann integral from 1885.

In more detail, Kohlenbach shows in [1] that in RCA$_0^\omega +$ WKL, for any third-order $Y:\mathbb{N}^\mathbb{N}\rightarrow \mathbb{N}$ that is continuous on $2^\mathbb{N}$ (via the usual epsilon-delta definition), there is an RM-code $\alpha$ such that $(\forall f \in 2^{\mathbb{N}})(Y(f)=\alpha(f)$. This is based on a construction by Dag Normann and readily generalised to e.g. $[0,1]$.

In this way, as long as WKL is available, it does not matter whether one formulates a given theorem about continuous functions with or without codes.

Now consider Arzela's 1885 convergence theorem for the Riemann (see [0]):

Let $f$ and $(f_{n})_{n\in \mathbb{N}}$ be Riemann integrable on the unit interval and such that $\lim_{n\rightarrow \infty}f_{n}(x)=f(x)$ for all $x\in [0,1]$. If there is $M\in \mathbb{N}$ such that $|f_{n}(x)|\leq M+1$ for all $n\in \mathbb{N}$ and $x\in [0,1]$, then $\lim_{n\rightarrow \infty}\int_{0}^{1}f_{n}(x)dx=\int_{0}^{1}f(x)dx$.

With codes, this theorem is provable in WKL or weaker. Without codes, this theorem can be formulated in third-order arithmetic, but is not provable from third-order comprehension Z$_2^\omega$, which implies full second-order arithmetic Z$_2$. The stronger fourth order system Z$_2^\Omega$ does prove the above convergence theorem.

Here, Z$_2^\omega$ is Kohlenbach's RCA$_0^\omega$ extended with third-order functionals $S_k^2$ that decide $\Pi_k^1$-formulas (the latter formulated in $L_2$). Such functionals $S_k^2$ are highly similar to the functionals $\nu_k$ in [0b, p. 129]. Moreover, Z$_2^\Omega$ is RCA$_0^\omega$ plus Kleene's (fourth order) $\exists^3$. Note that Z$_2^\omega$ and Z$_2^\Omega$ are conservative extensions of Z$_2$.

In this light, the minimal comprehension axioms required to prove Arzela's convergence theorem for the Riemann integral are massively different depending on whether one uses codes. Moreover, we only need to go 'continuous almost everywhere/Riemann integration' for coding to break down: no need to drag in topology or other abstract stuff.

I note that term-by-term integration, which is similar to the above convergence theorem, can already be found in the work of e.g. Dini (1870).

References

[0] Cesaro Arzela, Sulla integrazione per serie, Atti Acc. Lincei Rend., Rome 1 (1885), 532–537

[0b] Wilfried Buchholz, Solomon Feferman, Wolfram Pohlers, and Wilfried Sieg, Iterated inductive definitions and subsystems of analysis, LNM 897, Springer, 1981.

[1] Ulrich Kohlenbach, Foundational and mathematical uses of higher types, Reflections on the foundations of mathematics, Lect. Notes Log., vol. 15, ASL, 2002, pp. 92–116.

[2] Dag Normann and Sam Sanders, On the uncountability of $\mathbb{R}$, arxiv: https://arxiv.org/abs/2007.07560

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

Together with previous research by Ulrich Kohlenbach ([1]), a recent paper by Dag Normann and myself ([2]) provides the following pretty sharp answer.

In a nutshell, coding continuous functions in L$_2$, the language of second-order arithmetic, does not change the RM of WKL$_0$, one of the Big Five systems. By contrast, coding Riemann integrable functions (=continuous almost everywhere and bounded) dramatically changes the logical strength of basic theorems, like Arzela's convergence theorem for the Riemann integral from 1885.

In more detail, Kohlenbach shows in [1] that in RCA$_0^\omega +$ WKL, for any third-order $Y:\mathbb{N}^\mathbb{N}\rightarrow \mathbb{N}$ that is continuous on $2^\mathbb{N}$ (via the usual epsilon-delta definition), there is an RM-code $\alpha$ such that $(\forall f \in 2^{\mathbb{N}})(Y(f)=\alpha(f)$. This is readily generalised to e.g. $[0,1]$.

In this way, as long as WKL is available, it does not matter whether one formulates a given theorem about continuous functions with or without codes.

Now consider Arzela's 1885 convergence theorem for the Riemann (see [0]):

Let $f$ and $(f_{n})_{n\in \mathbb{N}}$ be Riemann integrable on the unit interval and such that $\lim_{n\rightarrow \infty}f_{n}(x)=f(x)$ for all $x\in [0,1]$. If there is $M\in \mathbb{N}$ such that $|f_{n}(x)|\leq M+1$ for all $n\in \mathbb{N}$ and $x\in [0,1]$, then $\lim_{n\rightarrow \infty}\int_{0}^{1}f_{n}(x)dx=\int_{0}^{1}f(x)dx$.

With codes, this theorem is provable in WKL or weaker. Without codes, this theorem can be formulated in third-order arithmetic, but is not provable from third-order comprehension Z$_2^\omega$, which implies full second-order arithmetic Z$_2$. The stronger fourth order system Z$_2^\Omega$ does prove the above convergence theorem.

Here, Z$_2^\omega$ is Kohlenbach's RCA$_0^\omega$ extended with third-order functionals $S_k^2$ that decide $\Pi_k^1$-formulas (the latter formulated in $L_2$). Such functionals $S_k^2$ are highly similar to the functionals $\nu_k$ in [0b, p. 129]. Moreover, Z$_2^\Omega$ is RCA$_0^\omega$ plus Kleene's (fourth order) $\exists^3$. Note that Z$_2^\omega$ and Z$_2^\Omega$ are conservative extensions of Z$_2$.

In this light, the minimal comprehension axioms required to prove Arzela's convergence theorem for the Riemann integral are massively different depending on whether one uses codes. Moreover, we only need to go 'continuous almost everywhere/Riemann integration' for coding to break down: no need to drag in topology or other abstract stuff.

I note that term-by-term integration, which is similar to the above convergence theorem, can already be found in the work of e.g. Dini (1870).

References

[0] Cesaro Arzela, Sulla integrazione per serie, Atti Acc. Lincei Rend., Rome 1 (1885), 532–537

[0b] Wilfried Buchholz, Solomon Feferman, Wolfram Pohlers, and Wilfried Sieg, Iterated inductive definitions and subsystems of analysis, LNM 897, Springer, 1981.

[1] Ulrich Kohlenbach, Foundational and mathematical uses of higher types, Reflections on the foundations of mathematics, Lect. Notes Log., vol. 15, ASL, 2002, pp. 92–116.

[2] Dag Normann and Sam Sanders, On the uncountability of $\mathbb{R}$, arxiv: https://arxiv.org/abs/2007.07560