# Is there a purely constructive presentation of the HK integral?

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 middle.

In a constructive setting, is there a way to:

• define the HK integral
• prove that the HK integral is unique
• define another notion of integrability which constructively implies HK-integrability and is classically equivalent to Lebesgue integrability
• and prove that every derivative, even if discontinuous, is HK-integrable?

One approach would be restricting the choice of gauge to Baire functions, since under fairly general assumptions the gauge can be chosen to be Baire 2. This would require proving Cousin's lemma only for Baire functions, which looks more promising than proving the full Cousin’s lemma constructively.

I have seen a paper on the reverse mathematics of Cousin’s lemma, but that is not in a constructive setting.

• Cross-posted Mar 10 at 15:46
• I edited this to make it easier to read, to remove the references to set theory (since most formal systems for constructive math are not based on set theory), and to remove the requirement of proving Bolzano-Weierstrass and Heine-Borel (which is not a clear criterion, since the theorems could be stated in different ways). The criteria here for proving statements about the HK integral constructively are substantial enough that further requirements don’t seem necessary. However, feel free to edit further or to revert if you don’t like this version. Apr 7 at 13:19

Firstly, the following paper deals with the HK-integral and constructive math, see [2] below for details.

Taschner R., The swap of integral and limit in constructive mathematics.

Secondly, the general HK integral may be (too) difficult to salvage, as the associated versions of Cousin's lemma (even the restrictions you mention) seem fundamentally non-constructive.

Thirdly, the HK integral restricted to absolutely integrable functions is the Lebesgue integral (on suitable domains). Hence, there should be a constructive treatment of this restriction. In particular, in the case of bounded functions, one can replace the use of Cousin's lemma by Vitali's covering theorem (see Section 3.5 in [1]), where the latter is 'more constructive' than the former. Also, since constructive measure theory exists, there is a 'constructive way around' Vitali's covering theorem, central as the latter is to Lebesgue measure theory (see again [1]).

References

[1] Dag Normann and Sam Sanders, the logical and computational properties of the Vitali covering theorem, arxiv: https://arxiv.org/abs/1902.02756

[2] Taschner R., The swap of integral and limit in constructive mathematics, Math. Log. Quart. 56, No. 5, 533 – 540 (2010) / DOI 10.1002/malq.200910107