2
$\begingroup$

Treating the Riemann integral in a constructive setting is easy and straightforward. Treating the closely related but much more powerful Henstock-Kurzweil integral constructively is almost easy, except for the dependence on Cousin's lemma where every proof seems to involve the excluded middl.

Assume a constructive setting with set theory axioms strong enough to prove things like Bolzano-Weierstrass and the Heine-Borel theorem. Is there a way to patch things up so that you have a fully constructive presentation of the HK integral along with proof of uniqueness which essentially gives the HK integral in a classical setting? In particular, it should have a constructive proof of the theorem that every derivative is integrable without the assumption that the derivative is continuous.

One approach would be to try to restrict the choice of gauge in a way that preserves most of the power. Under a fairly general set of assumptions the gauge can be chosen to be Baire 2, and so one possible approach could be to require gauges to be Baire functions and prove Cousin's lemma only for Baire functions, which definitely looks less hopeless than proving the full Cousins lemma constructively.

When searching I have only seen slides talking about the reverse mathematics of Cousins lemma, but those seem to consider systems of logic that are of interest but quite a bit much more restricted than set theory.

$\endgroup$
2
  • 1
    $\begingroup$ Just saw that Bishop considered this problem himself (restricting himself to treating the Lebesgue integral), and ended up giving a constructive treatment of the Daniell integral in Constructive Measure Theory (1972). He ran into set theoretic issues trying to get topology to work at all in a constructive setting, and so couldn't do a full constructive treatment of measure spaces before frames and locales formalism was discovered. $\endgroup$
    – saolof
    Commented Mar 10, 2022 at 23:56
  • $\begingroup$ Just a heads up that I found that the HK integral was intuitionistic in the Brouwerian sense (with no choice principle needed). I found a particularly short and simple proof using open induction, which is now the one shown in the Wikipedia article for Cousins theorem. But I would expect the full fan theorem to be sufficient to prove it $\endgroup$
    – saolof
    Commented May 23, 2023 at 8:47

1 Answer 1

Reset to default
7
$\begingroup$

What we have here is a very peculiar historical situation.

Lebesgue defined his integral at the end of the 19th century. To this day we call it the Lebesgue integral. W. H. Young gave an equivalent but different definition a few years later but he was likely the first to call it the "Lebesgue integral." Since then numerous authors have given other equivalent definitions. Yet, here we are 120 years later and we call it the Lebesgue integral.

Lebesgue knew that his integral integrated all bounded derivatives but only some unbounded derivatives. A French mathematician Arnauld Denjoy (1884-1974) (see image below) attacked this problem. Short little guy, but a major mathematician.

He was of the old school that believed in constructive definitions. Adamantly. He used two constructive extensions of the Lebesgue integral to push it one step further. Then he repeated them. Again and again. He proved that in a countable number of these extensions he could integrate all derivatives, constructively! He needed a transfinite sequence of such constructions and showed that, to handle all derivatives required all of the countable ordinals up to the first uncountable one.

A German mathematician named Perron defined an equivalent integral by a fairly simple process. Denjoy blasted that ferociously as not all constructive. It was a furious polemic which I might quote here later if I can find it.

Even so for many years that integral acquired the name Denjoy-Perron. I can imagine what Denjoy thought of that.

In the 1960s a Russian mathematician named Tolstov gave another equivalent definition for Denjoy's integral. Nobody rushed, fortunately, to call it the Tolstov integral or the Denjoy-Perron-Tolstov integral, since that would have been silly.

Then, in the 1950s an Irish mathematician and a Czech mathematician discovered yet another nonconstructive characterization of the Denjoy integral. For some reason when the world recovered from the astonishing fact that a seemingly trivial adjustment to the Riemann integral would produce this integral of Denjoy, they seemed to forget their history.

Far too many people now seem to have never heard of Denjoy and proclaim that this old integral should be called the Henstock-Kurzweil integral. Then a natural question arises. Since the HK-integral [sic] depends on a nonconstructible gauge is there any constructive way of capturing that integral.

Astonishing question! Ask Denjoy. I can only imagine what he would say in his colorful French way.

enter image description here

MUST READ REFERENCE:

The Complexity of Antidifferentiation, Denjoy Totalization, and Hyperarithmetic Reals

Kechris, Alexander S. (1987)

Proceedings of the International Congress of Mathematicians. American Mathematical Society , Providence, RI, pp. 307-313.

https://authors.library.caltech.edu/38894/1/Kechris_1987p307.pdf

$\endgroup$
4
  • $\begingroup$ Is Denjoys work constructive in Bishops sense of the word? I.e. key theorems are provable without the law of the excluded middle? $\endgroup$
    – saolof
    Commented Mar 10, 2022 at 15:04
  • $\begingroup$ @saolof It is constructive in the sense that Denjoy, Borel, et al would have meant in 1900. A countable number of operations. The Borel sets are constructive. The Lebesgue measurable sets, not so according to Borel. $\endgroup$
    – B. S. Thomson
    Commented Mar 10, 2022 at 15:08
  • 1
    $\begingroup$ @saolof I added a reference to a paper of Alex Kechris that considers your problem "... from the point of view of logic and definability theory-more particularly, in this case, descriptive set theory." $\endgroup$
    – B. S. Thomson
    Commented Mar 10, 2022 at 17:04
  • $\begingroup$ The process used by Denjoy is called totalization: I can furthermore add that Renato Caccioppoli was a big fan of this technique. $\endgroup$
    – Daniele Tampieri
    Commented Dec 28, 2022 at 20:25

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .