Skip to main content

On False Heine/Borel Compactness Principles in Proof Mining

  • 691 Accesses

Part of the Lecture Notes in Computer Science book series (LNTCS,volume 12813)


The use of certain false Heine/Borel compactness principles is justified in source theories of proof mining. The justification rests on the metatheorems of the theory of proof mining. Ulrich Kohlenbach recently produced a counterexample showing that the metatheorems do not apply unrestrictedly to Heine-Borel compactness principles. In this short note, we present a simpler counterexample than Kohlenbach’s, showing that the metatheorems can fail because the source theory is already inconsistent.


  • Proof mining
  • Heine/Borel compactness
  • Bounded collection
  • Uniform boundedness
  • Bounded functional interpretation

We acknowledge the support of Fundação para a Ciência e Tecnologia by way of the grant UIDB/04561/2020 given to the research center CMAFcIO.

This is a preview of subscription content, access via your institution.

Buying options

USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions


  1. Browder, F.E.: Convergence of approximants to fixed points of nonexpansive nonlinear mappings in Banach spaces. Arch. Rational Mech. Anal. 24, 82–90 (1967)

    CrossRef  MathSciNet  Google Scholar 

  2. Engrácia, P., Ferreira, F.: Bounded functional interpretation with an abstract type. In: Rezuş, A. (ed.) Contemporary Logic and Computing. Landscapes in Logic, vol. 1, pp. 87–112. College Publications, London (2020)

    Google Scholar 

  3. Ferreira, F.: A most artistic package of a jumble of ideas. Dialectica 62, 205–222 (2008). Special Issue: Gödel’s dialectica interpretation. Guest editor: Thomas Strahm

    Google Scholar 

  4. Ferreira, F., Leustean, L., Pinto, P.: On the removal of weak compactness arguments in proof mining. Adv. Math. 354, 106728 (2019)

    CrossRef  MathSciNet  Google Scholar 

  5. Kohlenbach, U.: Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics, Springer, Berlin (2008).

    CrossRef  MATH  Google Scholar 

  6. Kohlenbach, U.: On quantitative versions of theorems due to F. E. Browder and R. Wittmann. Adv. Math. 226, 2764–2795 (2011)

    CrossRef  MathSciNet  Google Scholar 

  7. Kohlenbach, U.: Proof-theoretic uniform boundedness and bounded collection principles and countable Heine-Borel compactness. Arch. Math. Logic.

  8. Normann, D., Sanders, S.: Open sets in computability theory and reverse mathematics. J. Logic Comput. 30(8), 1639–1679 (2020)

    CrossRef  MathSciNet  Google Scholar 

  9. Simpson, S.G.: Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic, Springer, Heidelberg (1999)

    CrossRef  Google Scholar 

  10. Spector, C.: Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In: Dekker, F.D.E. (ed.) Recursive Function Theory: Proceedings of Symposia in Pure Mathematics, vol. 5, pP. 1–27. American Mathematical Society, Providence (1962)

    Google Scholar 

Download references

Author information

Authors and Affiliations


Corresponding author

Correspondence to Fernando Ferreira .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and Permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ferreira, F. (2021). On False Heine/Borel Compactness Principles in Proof Mining. In: De Mol, L., Weiermann, A., Manea, F., Fernández-Duque, D. (eds) Connecting with Computability. CiE 2021. Lecture Notes in Computer Science(), vol 12813. Springer, Cham.

Download citation

  • DOI:

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-80048-2

  • Online ISBN: 978-3-030-80049-9

  • eBook Packages: Computer ScienceComputer Science (R0)