What is the status of the extreme value theorem in forms of constructive mathematics, such as Smooth Infinitesimal Analysis?

In certain intuitionistic frameworks the extreme value theorem cannot be proved. Depending on the exact framework, counterexamples can be constructed as well; see for example pp. 294-295 in

Troelstra, A. S.; van Dalen, D. Constructivism in mathematics. Vol. I. An introduction. Studies in Logic and the Foundations of Mathematics, 121. North-Holland Publishing Co., Amsterdam, 1988. xx+342+XIV pp. ISBN: 0-444-70266-0; 0-444-70506-6

The Smooth Infinitesimal Analysis (SIA) following Lawvere, Kock, J. Bell, and others is based on a category-theoretic framework where the background logic is intuitionistic. What is the status of the extreme value theorem in SIA?

• Please excuse my liberty in generalising your question slightly. – Paul Taylor Aug 17 '14 at 8:59
• @Paul Taylor, I liked the question better before, since I would not call SIA constructive. 1) SIA is not computational. 2) SIA contradicts theorems of Bishop-style mathematics like $x^2=0 \rightarrow x=0$. 3) SIA relies on infinitesimals which can not be exhibited in a way that violates Bishop's principles of "make every concept affirmative" and "avoid pseudo-generality". I like constructively and I like SIA, but let's keep the concepts separate! – Matt F. Aug 20 '14 at 1:20
• @MattF., first of all thanks for your answer. As far as the question title is concerned, I think the change is fine. Arguably "constructive" can be used in the sense of "relying on an intuitionistic logic". The identification of "constructive" and "computational" is one of the cornerstones of Bishop's approach but one may be allowed to hold alternative opinions. For an analysis of Bishop's ideology see arxiv.org/abs/1110.5456 In fact your comment could be the subject of a separate question if you wish to pursue it. – Mikhail Katz Aug 20 '14 at 8:02

By the extreme value theorem I take it that you mean that

Every continuous real-valued function on a closed bounded interval is bounded and attains its bounds.

I am going to answer this in terms of General Topology unsullied by excluded middle first and consider the meanings of the topological terms and the foundational options afterwards.

Any closed bounded interval is compact and any continuous image of a compact subspace is compact.

I am not aware of any setting that questions these two assertions, so the main question says, in part:

Every compact subspace $K\subset\mathbb R$ is bounded and has a maximum.

For this, clearly $K$ must be non-empty. I claim that it is reasonable to define a compact subspace to be non-empty (or, as I call it occupied) if $(K\subset\emptyset)=\bot$.

Then $K$ is covered by the (directed) union $\bigcup_n(-n,n)$, so one of these suffices and provides a bound.

Whether there is a maximum depends on our definitions of the words compact and maximum and in particular of what a real number is, to serve as the maximum.

Also, the main question also asks whether the maximimum value is attained.

To see why it need not be, consider the function $f:[0,2\pi]\to\mathbb R$ given by $f(x) = a \sin x$, which attains its maximum value at $\pi/2$ if $a>0$ or at $3\pi/2$ if $a<0$. However, if $a$ is so close to $0$ that we do not know its sign (because it depends on some unsolved problem) then we don't know where $f$ attains its bound. Imagine $f$ as a standing wave or as a skipping rope. (Seasoned intuitionists will see that there is actually no logical problem here, but will be able to manufacture a more complicated genuine counterexample.)

Now we turn to the definitional and foundational issues that are needed to make sense of this.

Please be aware that there is no party line in constructive mathematics: for perfectly good intellectual reasons, different people study different systems.

Desite being the person who drew Mikhail Katz's attention to Sythetic Differential Geometry (aka Smooth Infinitessimal Analysis) I am going to leave it to the experts in that to answer the specific question, although I suspect that this will be the same as in locale theory or ASD.

The Bishop school does not use the finite open sub-cover definition of compactness; for them, a compact subspace is one that is closed and totally bounded. Thus is because of issues with the Fan Theorem, although that does not bear heavily on this particular question. More relevant is that, for Bishop, the word compact carries more properties than I would want.

My answer is based on my system, Abstract Stone Duality, and specifically on my paper A Lambda Calculus for Real Analysis, which addresses the Intermediate and Extreme Value Theorems. I believe that the situation for Locale Theory and Formal Topology is the same.

We use the finite open sub-cover definition of compactness. This means that the predicate $K\subset U$ is a Scott-continuous function of the open subspace $U$ valued in the Sierpinski space. In locale theory, for the inclusion map $i:K\hookrightarrow\mathbb R$, the direrect image map $i_*$ preserves directed joins.

In this setting, the equations $(K\subset\emptyset)=\bot$ and $i_*\bot=\bot$ are reasonable definitions of a non-empty or occupied compact subspace, since they are lattice duals of the definition $\exists_i\top=\top$ for an inhabited overt subspace.

However, we need to be careful with the definition of a real number in order to say that such a subspace has a maximum.

By a real number $x\in\mathbb R$ we mean a Dedekind cut, which is a pair of continuous Sierpinski-valued predicates $(\delta d,\upsilon u)$ saying whether a number $d$ is a lower bound and $u$ is an upper bound. When a "real number" is said to be uncomputable or not constructively defined, usually what is meant is that one of these predicates is not available. Indeed, we have

Every occupied compact subspace of $\mathbb R$ has a maximum element, as an upper real number.

The problem is that the finite open sub-cover definition of compactness, on its own, gives no information about lower bounds of the upper bound. However, Bishop has

Every closed, inhabited, totally bounded subspace of $\mathbb R$ has a maximum element, as a Dedekind cut,

whilst I would say that

Every inhabited compact overt subspace of $\mathbb R$ has a maximum element, as a Dedekind cut.

I am not going to give the definition of overt subspace here but instead direct you to my MO answer saying why classical mathematicians should care about this idea.

In the case of a compact overt subspace, it is decidable whether it is empty or not and the notions of being inhabited and occupied coincide.

Most familiar (sub)spaces are overt, so to understand the idea (and the constructive status of the Intermediate and Extreme Value Theorems) you need examples of non-overt subspaces, which you will find in my paper cited above.

In the good case, how do we find where the function attains its bounds? We want to consider the inverse image of the maximum and would like this to be another non-empty compact overt subspace.

In a compact Hausdorff space, closed and compact subspaces are the same. The same is true of open and overt subspaces of an overt discrete space, but $\mathbb R$ is not discrete. This means that we have to ask when the inverse image of an overt subspace is overt. This question is the main focus of my paper and my MO answer cited above.

• Thanks Paul this is terrific. I should have clarified that I had uniform continuity in mind. This still admits of counterexamples as you know. Also, I was looking for a maximum ($x$) rather than a maximal value ($y$). – Mikhail Katz Aug 17 '14 at 14:49
• I do not see where uniform continuity has a bearing on this particular question. I introduced the term occupied compact subspace in my paper as the lattice dual of inhabited overt subspace. Occupation and habitation are not the same thing. – Paul Taylor Aug 17 '14 at 14:51
• I did talk about the attainment of the maximum as well as the maximal value. – Paul Taylor Aug 17 '14 at 20:06
• Regarding uniform continuity: as I recall the proof in van Dalen--Troelstra that the maximal value exists depends on the function being uniformly continuous on the interval rather than merely continuous. Is this otherwise in SIA? – Mikhail Katz Aug 18 '14 at 7:35
• Without the law of excluded middle bounded closed internal of $\mathbb{R}$ might fail to be compact (even in a topos, see the section of Sketches of an elephant about real numbers) !! The formal locale of real numbers is always locally compact but is spatial (and hence isomorphic to the topological space of real number) if and only if the topological space of real number is locally compact. Also function $f$ from a closed internal of real numbers to itself extend to a function on the formal locale if and only if it is uniformly continuous. This is why you generally need Uniform Continuity. – Simon Henry Oct 12 '15 at 12:11

1) Yes, in SIA the maximum value $y$ exists. Looking at $R^{[-1,1]}$, the space of all smooth maps, there is a smooth map $\max : R^{[-1,1]} \rightarrow R$ where $y \ge \max(f) \leftrightarrow \forall x\ f(x) \le y$

2) No, in SIA the maximum need not be attained. Let $a,x,w$ range over $[-1,+1]$.

Suppose $\forall f\in R^{[-1,1]} \ \exists x \ \forall w\ \ f(x) \ge f(w)$.

Then $\forall a\ \exists x\ \forall w\ \ ax \ge aw$.

Then $\forall a\ \exists x\ \forall w\ \ a(x-w) \ge 0$.

If $x< 1$, then choose $w=1$, so $x-w<0$, and dividing by $x-w$ gives $a \le 0$.

If $x> -1$, then choose $w=-1$, so $x-w>0$, and dividing by $x-w$ gives $a \ge 0$.

Since $x< 1 \vee x>-1$, we conclude $a \le 0 \vee a \ge 0$.

Since this conclusion does not hold in SIA, the original claim that the maximum is attained can not hold in SIA either.