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 (or slightly stronger intuitionistic) 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.
Best Answer
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