Skip to content

The Proof Theory Blog

⊢ ((A → B) → A) → A

Menu
  • Home
  • About
  • Contribute
  • Resources
Menu

Of representations of mathematics

Posted on May 24, 2020June 1, 2020 by Sam Sanders

Short Summary

Studying mathematics via logic implies one needs to choose a suitable logical language and represent part of mathematics therein. For instance, since everything is a set in set theory, one represents the natural numbers via the von Neumann ordinals: 0 corresponds to \emptyset and n+1 corresponds to the set n \cup \{n\}.

An obvious question raised by this practise is whether a given representation remains true to the original. The aim of this post is to show that for a rather common representation practise, namely coding objects in the language L_2 of second-order arithmetic, the answer is negative. In particular, we show that even representations of continuous functions change the logical strength of theorems with Big Names, like Weierstrass, Heine, and Tietze, attached to it.

Disclaimer: the below results may be found in full gruesome detail in [Sa19]; the interested reader should consult this paper before making grand (counter-)claims.

Representations/codes of continuous functions

Before providing the technical definition, I first provide an intuitive motivation for the coding/representation of continuous functions.

Now, the reader will be familiar with continuity, say on the unit interval as in the usual ‘epsilon-delta’ definition as follows:

(\forall \epsilon >0)(\forall x \in [0,1])(\exists \delta >0 )(\forall y\in [0,1])(|x-y|<\delta \rightarrow |f(x)-f(y)|<\epsilon).

A modulus of (pointwise) continuity is any function g:\mathbb{R}^2\rightarrow \mathbb{R} that outputs the above \delta>0 in terms of the other data, i.e.

(\forall \epsilon >0)(\forall x \in [0,1])(\forall y\in [0,1])(|x-y|<g(x, \epsilon) \rightarrow |f(x)-f(y)|<\epsilon).

A moment of thought shows that g(x, \epsilon) can be taken to be continuous in the x variable.

While clearly dealing with uncountable things, a continuous function with a continuous modulus only contains countably much information as follows:

Since g(x, \epsilon) is continuous in the x-variable, the following union covers the union interval: \cup_{q\in \mathbb{Q}\cap [0,1]}B(q, g(q, \frac{1}{2^k})). By compactness, there is a finite sequence q_0, ..., q_{n_k} \in \mathbb{Q}\cap [0,1] such that \cup_{i\leq n_k}B(q_i, g(q_i, \frac{1}{2^k})) also covers [0,1]. By definition, the finite sequence q_0,..., q_{n_k} contains enough points to approximate f up to error 1/2^k as follows:

(\forall k\in \mathbb{N})(\forall x \in [0,1])(\exists i\leq n_k)(|f(x)-f(q_i)|<\frac{1}{2^k}).

Thus, we can reconstruct the function f on [0,1] based on f(q_i) for all i\leq n_k and all k\in \mathbb{N}, i.e. countably much information!

The previous observation is the idea underlying the representation or ‘coding’ of continuous functions in L_2. Recall that the language L_2 only involves variable for natural numbers and sets X\subseteq \mathbb{N} and functions g:\mathbb{N}\rightarrow\mathbb{N}.

The following definition is the standard in Reverse Mathematics (RM for short) and taken from Steve Simpson’s excellent Subsystems of Second-Order Arithmetic [Si09].

As it turns out, one does not need much beyond the computable to show that a (third-order) continuous function on [0,1] has such a code/representation: the ‘Big Five’ system WKL from RM suffices, as shown by Kohlenbach [Ko02]. So far so good: continuous functions can be represented by countable codes, and one does not need much beyond the computable to make this work. Moreover, Kohlenbach’s base theory (see [Ko05]) \text{RCA}_0^\omega proves that every code on [0,1] gives rise to a continuous (third-order) function.

Finally, people have proposed to study more complicated topics (measure theory, topology, …) via codes. The codes become rather complicated and showing that each higher-order object has a code, becomes hard compared to e.g. the Big Five of RM. Perhaps this observation would not come as a surprise, but we show next that even coding continuous functions has its problems.

Problems with coding continuous functions

We now discuss problems with the coding of continuous functions. The results in this section can be found in full detail in [Sa19]. The following table is taken from there. The notion of separably closed set is standard in RM (see e.g. [Bro05]).

In the first column, I have listed a number of well-known theorems from the RM literature. In the second column, one can observe the logical strength of these theorems when formulated in L_2 using RM-codes as in the above definition. The only difference with the third column is that we now use the usual definition of ‘third-order function that is continuous’.

The difference is quite extreme in some cases, less in others. Recall that the system \text{RCA}_0^\omega is Kohlenbach’s base theory of higher-order RM from [Ko05].


Rendered by QuickLaTeX.com

I hope I have convinced you THAT a problem occurs: RM seeks to find the minimal axioms needed to prove theorems of ordinary mathematics and the above table suggests that introducing codes changes what these minimal axioms are/can be.

Too many codes

Let us now try to understand WHY this problem occurs, using the Tietze extension theorem as an example. This theorem is formulated as follows.

(TIE) For f:[0,1]\rightarrow \mathbb{R} continuous on the separably closed C\subseteq[0,1], there is continuous g:[0,1]\rightarrow \mathbb{R} such that f(x)=g(x) for x\in C.

Now let TIE_2 be the theorem TIE interpreted in L_2 using RM-codes. TIE_2 deals with codes for continuous functions defined on a separably closed set C. As is clear from the above table, TIE_2 is equivalent to ACA_0.

Now let TIE_3 be the theorem TIE interpreted without codes for continuous functions. Thus, TIE_3 deals with third-order functions f:[0,1]\rightarrow \mathbb{R} that are also continuous on a separably closed set C. As is clear from the above table, TIE_3 is provable in RCA_0^\omega.

Recall from the above that codes defined on [0,1] always define a third-order function in RCA_0^\omega. For codes defined on separably closed sets, this is no longer the case! In fact, we have the following.

The following are equivalent over RCA_0^\omega:

(a) ACA_0

(b) For an RM-code f:[0,1]\rightarrow \mathbb{R} defined on the separably closed C\subseteq\mathbb{R}, there is a third-order function g:[0,1]\rightarrow \mathbb{R} such that f(x)=g(x) for x\in C.

Note that g from item (b) need not be continuous: this item only expresses that the second-order code f gives rise to a function g.


On a historical note, Tietze’s two main theorems in [Tie12] deal with functions that are everywhere defined on [0,1], as discussed in [Sa19].

From the equivalence between items a) and b), we may conclude that, working in RCA_0^\omega, there are ‘too many’ codes for continuous functions on separably closed sets. Indeed, we need ACA_0 to guarantee that every such code actually denotes a third-order object.

References

[Bro05] Douglas K. Brown, Notions of compactness in weak subsystems of second order arithmetic, Reverse mathematics 2001, Lect. Notes Log., vol. 21, Assoc. Symbol. Logic, pp. 47–66, 2005

[Ko02] 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.

[Ko05] ___________, Higher order reverse mathematics, Reverse mathematics 2001, Lect. Notes Log., vol. 21, ASL, 2005, pp. 281–295.

[Sa19] Sam Sanders, Representations and the foundations of mathematics, Submitted, arXiv: https://arxiv.org/abs/1910.07913

[Si09] Stephen Simpson, Subsystems of second order arithmetic, 2nd ed., Perspectives in Logic, CUP, 2009.

[Tie15] Heinrich Tietze, Uber Funktionen, die auf einer abgeschlossenen Menge stetig sind, J. Reine Angew. Math. 145, 9–14, 1915.

1 thought on “Of representations of mathematics”

  1. Anupam Das says:
    June 3, 2020 at 10:07 am

    Thanks for the interesting post, Sam. Do you know if there is any tradition of showing the robustness of reverse mathematics results with respect to codings? E.g., can we say that your first column holds for any ‘reasonable’ first-order coding? In this way, a bit of a leap, perhaps the offset in logical strength can be calibrated with the order of the representation?

    Reply

Leave a Reply Cancel reply

Your email address will not be published. Required fields are marked *

Meta

  • Register
  • Log in
  • Entries RSS
  • Privacy Policy

Search

© 2023 The Proof Theory Blog | Powered by Minimalist Blog WordPress Theme
The Proof Theory Blog uses cookies, but you can opt-out if you wish. For further information see our privacy policy. Cookie settingsAccept
Privacy & Cookies Policy

Privacy Overview

This website uses cookies to improve your experience while you navigate through the website. Out of these cookies, the cookies that are categorized as necessary are stored on your browser as they are essential for the working of basic functionalities of the website. We also use third-party cookies that help us analyze and understand how you use this website. These cookies will be stored in your browser only with your consent. You also have the option to opt-out of these cookies. But opting out of some of these cookies may have an effect on your browsing experience.
Necessary
Always Enabled
Necessary cookies are absolutely essential for the website to function properly. This category only includes cookies that ensures basic functionalities and security features of the website. These cookies do not store any personal information.
Non-necessary
Any cookies that may not be particularly necessary for the website to function and is used specifically to collect user personal data via analytics, ads, other embedded contents are termed as non-necessary cookies. It is mandatory to procure user consent prior to running these cookies on your website.
SAVE & ACCEPT