Skip to main content
SpringerLink
Log in
Book cover

Conference on Computability in Europe

CiE 2021: Connecting with Computability pp 199–203Cite as

On False Heine/Borel Compactness Principles in Proof Mining

  • 691 Accesses

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

Abstract

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.

Keywords

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
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

References

  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). https://doi.org/10.1007/978-3-540-77533-1

    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. https://doi.org/10.1007/s00153-021-00771-w

  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

  1. Faculdade de Ciências, Universidade de Lisboa, Lisbon, Portugal

    Fernando Ferreira

Authors
  1. Fernando Ferreira
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Fernando Ferreira .

Editor information

Editors and Affiliations

  1. University of Lille, Lille, France

    Liesbeth De Mol

  2. Vakgroep Wiskunde, Ghent University, Ghent, Belgium

    Prof. Dr. Andreas Weiermann

  3. University of Göttingen, Göttingen, Germany

    Florin Manea

  4. Ghent University, Ghent, Belgium

    David Fernández-Duque

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. https://doi.org/10.1007/978-3-030-80049-9_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-80049-9_18

  • 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)

search

Navigation