Abstract
Scott’s multiple-conclusion entailment relations, originally conceived as a means to clarify several aspects of many-valued logic, and later put to great use in a revised Hilbert programme for abstract algebra, are brought to application in the context of König’s lemma. An inductively generated entailment relation which describes the linear spreads of a detachable unbounded tree over a finite discrete set is given a direct non-inductive description. This immediately prompts a consistency result which serves as an elementary and constructive counterpart of the Weak König Lemma.
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.
See also Shoesmith and Smiley (1978) for a historical account of the development of multiple-conclusion logic.
- 2.
This might as well suffice to fit this paper into place, by assessing that “all the duties imposed upon the language of mathesis universalis are done by modern logic with set theory.” (Marciszewski 1984).
- 3.
A quality shared also by Scott’s information systems (Scott 1982).
- 4.
- 5.
Peter Schuster has kindly pointed this out.
- 6.
The proof of Proposition 2 adapts (Rinaldi et al. 2018, Proposition 4) which in turn rests on an argument by Bell (2005, p. 161 sq.). We slightly improve on Rinaldi et al. (2018) insofar as that we work with a simpler entailment relation, thus avoiding a detour to the entailment relation of prime filter of a Boolean algebra.
- 7.
Tatsuji Kawai has kindly pointed this out. Kawai’s observation improved an earlier version of Proposition 14 which resorted to WLPO.
- 8.
The following discussion owes to a question of the anonymous referee.
- 9.
The opinions expressed in this publication are those of the author and do not necessarily reflect the views of the John Templeton Foundation.
References
Aczel, P., & Rathjen, M. (2000/2001) Notes on constructive set theory (Technical report, Report No. 40). Institut Mittag–Leffler.
Aczel, P., & Rathjen, M. (2010). Constructive set theory. Book draft.
Bell, J. L. (2005). Set theory. Boolean-valued models and independence proofs (Oxford logic guides). Oxford: Oxford University Press.
Berger, J., Ishihara, H., & Schuster, P. (2012). The weak König lemma, Brouwer’s fan theorem, De Morgan’s law, and dependent choice. Reports on Mathematical Logic, 47, 63–86.
Brink, C. (1982). A note on Peirce and multiple conclusion logic. Transactions of the Charles S. Peirce Society, 18(4), 349–351.
Brouwer, L. E. J. (1908). De onbetrouwbaarheid der logische principes. Tijdschrift voor Wijsbegeerte, 2, 152–158.
Brouwer, L. E. J. (1910). On the structure of perfect sets of points. KNAW, Proceedings, 12, 785–794.
Brouwer, L. E. J. (1925). Intuitionistische Zerlegung mathematischer Grundbegriffe. Jahresbericht der Deutschen Mathematiker-Vereinigung, 33, 251–256.
Carnap, R. (1943). Formalization of logic. Cambridge, MA: Harvard University Press.
Cederquist, J., & Coquand, T. (2000). Entailment relations and distributive lattices. In S. R. Buss, P. Hájek, & P. Pudlák (Eds.), Logic Colloquium ’98: Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic (Volume 13 of Lecture Notes in Logic, pp. 127–139). AK Peters/Springer.
Ciraulo, F., & Sambin, G. (2008). Finitary formal topologies and Stone’s representation theorem. Theoretical Computer Science, 405(1–2), 11–23.
Coquand, T. (2005). About Stone’s notion of spectrum. Journal of Pure and Applied Algebra, 197(1–3), 141–158.
Coquand, T. (2009). Space of valuations. Annals of Pure and Applied Logic, 157(2–3), 97–109.
Coquand, T., & Lombardi, H. (2002). Hidden constructions in abstract algebra: Krull dimension of distributive lattices and commutative rings. In M. Fontana, S.-E. Kabbaj, & S. Wiegand (Eds.), Commutative ring theory and applications (Volume 231 of Lecture Notes in Pure and Applied Mathematics, pp. 477–499), Reading, MA: Addison-Wesley.
Coquand, T., & Neuwirth, S. (2017). An introduction to Lorenzen’s “Algebraic and logistic investigations on free lattices” (1951). Preprint. Available from: https://arxiv.org/abs/1711.06139.
Coquand, T., & Schuster, P. (2011). Unique paths as formal points. Journal of Logic and Analysis, 3(6), 1–9.
Coquand, T., & Zhang, G.-Q. (2000). Sequents, frames, and completeness. In H. Schwichtenberg & P. G. Clote (Eds.), Computer Science Logic. 14th International Workshop, CSL 2000 Annual Conference of the EACSL.
Coquand, T., Lombardi, H., & Neuwirth, S. (2017). Lattice-ordered groups generated by an ordered group and regular systems of ideals. Preprint. Available from: https://arxiv.org/abs/1701.05115.
Coste, M., Lombardi, H., & Roy, M.-F. (2001). Dynamical method in algebra: Effective Nullstellensätze. Annals of Pure and Applied Logic, 111(3), 203–256.
Gentzen, G. (1935a). Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift, 39(1), 176–210.
Gentzen, G. (1935b). Untersuchungen über das logische Schließen. II. Mathematische Zeitschrift, 39(1), 405–431.
Hendtlass, M., & Lubarsky, R. (2016). Separating fragments of WLEM, LPO, and MP. The Journal of Symbolic Logic, 81(4), 1315–1343.
Hertz, P. (1929). Über Axiomensysteme für beliebige Satzsysteme. Mathematische Annalen, 101(1), 457–514.
Ishihara, H. (1990). An omniscience principle, the König Lemma and the Hahn-Banach theorem. Mathematical Logic Quarterly, 36(3), 237–240.
Ishihara, H. (2005). Constructive reverse mathematics: Compactness properties. In L. Crosilla & P. Schuster (Eds.), From sets and types to topology and analysis: Towards practicable foundations for constructive mathematics (Volume 48 of Oxford Logic Guides, chapter 16). Oxford: Clarendon Press.
Koppelberg, S. (1989). Handbook of boolean algebras (Vol. 1). Amsterdam: North-Holland.
Lombardi, H., & Quitté, C. (2015). Commutative algebra: Constructive methods. Dordrecht: Springer Netherlands.
Lorenzen, P. (1951). Algebraische und logistische Untersuchungen über freie Verbände. Journal of Symbolic Logic, 16(2), 81–106.
Marciszewski, W. (1984). The principle of comprehension as a present-day contribution to mathesis universalis. Philosophia Naturalis, 21(2–4), 523–537.
Negri, S., & von Plato, J. (1998). Cut elimination in the presence of axioms. Bulletin of Symbolic Logic, 4(4), 418–435.
Payette, G., & Schotch, P. K. (2014). Remarks on the Scott–Lindenbaum theorem. Studia Logica, 102(5), 1003–1020.
Rinaldi, D., & Wessel, D. (2018). Cut elimination for entailment relations. To appear in Archive for Mathematical Logic, Online. https://doi.org/10.1007/s00153-018-0653-0.
Rinaldi, D., Schuster, P., & Wessel, D. (2018). Eliminating disjunctions by disjunction elimination. Indagationes Mathematicae, 29(1), 226–259. Virtual Special Issue – L.E.J. Brouwer, fifty years later.
Sambin, G. (2003). Some points in formal topology. Theoretical Computer Science, 305(1–3), 347–408.
Scott, D. (1974). Completeness and axiomatizability in many-valued logic. In L. Henkin, J. Addison, C. C. Chang, W. Craig, D. Scott, & R. Vaught (Eds.), Proceedings of the Tarski Symposium (Proceedings of symposia in pure mathematics, Vol. XXV, University of California, Berkeley, CA, 1971, pp. 411–435). Providence, RI: American Mathematical Society.
Scott, D. S. (1982). Domains for denotational semantics. In M. Nielsen & E. M. Schmidt (Eds.), Automata, languages and programming (pp. 577–610). Berlin/Heidelberg: Springer.
Shoesmith, D. J., & Smiley, T. J. (1978). Multiple-conclusion logic. Cambridge: Cambridge University Press.
Sikora, A. S. (2004). Topology on the spaces of orderings of groups. Bulletin of the London Mathematical Society, 36(4), 519–526.
Tarski, A. (1930). Fundamentale Begriffe der Methodologie der deduktiven Wissenschaften. Monatshefte für Mathematik und Physik, 37, 361–404.
Troelstra, A. S., & van Dalen, D. (1988). Constructivism in mathematics. An introduction (Volume 121 of studies in logic and the foundations of mathematics). Amsterdam: Elsevier Science.
Wessel, D. (2018). Ordering groups constructively. To appear in Communications in Algebra.
Acknowledgements
The author would like to express his gratitude to the anonymous referee for an appreciative review with valuable suggestions and remarks; to the organizers of the Humboldt-Kolleg “Proof Theory as Mathesis Universalis” for the encouragement to contribute to the present volume in the first place; to Tatsuji Kawai for having generously shared his insights; to Peter Schuster and Davide Rinaldi for guidance and support; and to Karla Misselbeck for a painstakingly thorough reading of an earlier version of the manuscript.
The research that has led to this paper was carried out when the author was a doctoral student at the Universities of Trento and Verona. Financial support through the joint doctoral programme in mathematics and the project “Categorical localisation: methods and foundations” (CATLOC) funded by the University of Verona within the programme “Ricerca di Base 2015”, is gratefully acknowledged. Further research has been undertaken within the project “A New Dawn of Intuitionism: Mathematical and Philosophical Advances” (ID 60842) funded by the John Templeton Foundation,Footnote 9 as well as within the project “Dipartimenti di Eccellenza 2018-2022” of the Italian Ministry of Education, Universities and Research (MIUR). The final version of this note was prepared when the author was visiting the Hausdorff Research Institute for Mathematics in Bonn during the Trimester Program “Types, Sets and Constructions”.
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
Wessel, D. (2019). Point-Free Spectra of Linear Spreads. 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_19
Download citation
DOI: https://doi.org/10.1007/978-3-030-20447-1_19
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)