Abstract
In mathematical proofs axioms and intermediary results are often represented by their names. It is however undecidable whether such a description corresponds to an underlying proof. This implies that there is sometimes no recursive bound of the complexity of the simplest underlying proof in the complexity of the abstract proof description, i.e. the abstract proof description might be non-recursively simpler.
Necessity by §8, no 1, Proposition 1; sufficiency by Theorem 1. (Proof of Corollary page 85 Bourbaki, General Topology 1).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The author is grateful to the anonymous referee for the hint to MacLane’s thesis which contains one of the few explicit discussions of proof macros with the corresponding rules in logic.
References
Aguilera, J. P., & Baaz, M. (2018). Unsound inferences make proofs shorter. arXiv preprint arXiv:1608.07703, to appear in the Journal of Symbolic Logic.
Baaz, M., & Wojtylak, P. (2008). Generalizing proofs in monadic languages. Annals of Pure and Applied Logic, 154(2), 71–138.
Bourbaki, N. (2013). General topology: Chapters 1–4 (Vol. 18). Springer Science & Business Media, London, New York.
Gentzen, G. (1935). Untersuchungen über das logische Schließen. I. Mathematische zeitschrift, 39(1), 176–210.
Hilbert, D. (1899). Grundlagen der Geometrie. Teubner.
Krajíček, J., & Pudlák, P. (1988). The number of proof lines and the size of proofs in first order logic. Archive for Mathematical Logic, 27(1), 69–84.
Mac Lane, S. (1934). Abgekürzte Beweise im Logikkalkül. Hubert.
Orevkov, V. P. (1984). Reconstitution of the proof from its scheme (russian abstract). 8th Soviet Conference on Mathematical Logic. Novosibirsk (p. 133).
Takeuti, G. (1975). Proof Theory 2nd edition (2003) Dover Publications Mineola New York.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Baaz, M. (2019). Note on the Benefit of Proof Representations by Name. In: Centrone, S., Negri, S., Sarikaya, D., Schuster, P.M. (eds) Mathesis Universalis, Computability and Proof. Synthese Library, vol 412. Springer, Cham. https://doi.org/10.1007/978-3-030-20447-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-20447-1_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-20446-4
Online ISBN: 978-3-030-20447-1
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)