Der Satz von Hahn-Banach per Disjunktionselimination

Schlagbauer, Konstantin; Schuster, Peter; Wessel, Daniel

Confluentes Mathematici, Tome 11 (2019) no. 1, pp. 79-93.

The Hahn-Banach extension theorem is at once main pillar of functional analysis and — due to its notorious nature as consequence of the axiom of choice — prime example of a pure existential statement. By way of a general syntactic conservation result for multi-conclusion entailment relations on top of their single-conclusion counterparts, we are able to trace back the Hahn-Banach theorem to a disjunction elimination. The classical result can then be regained by semantic interpretation.

Der Erweiterungssatz von Hahn-Banach ist zugleich ein Stützpfeiler der Funktionalanalysis und — infolge seiner bekannten Natur als Konsequenz des Auswahlaxioms — Musterbeispiel für eine reine Existenzaussage. Vermöge eines allgemeinen syntaktischen Konservativitätsresults bezüglich mehr- über einwertigen Schlussrelationen können wir den Satz von Hahn-Banach auf eine Disjunktionselimination zurückführen. Semantische Interpretation erlaubt sodann Rückschluss auf das klassische Resultat.

Classification : 03F65, 06F20
Mots clés : Hahn-Banach theorem; Scott entailment relations; conservative extension; constructive mathematics.

[1] Peter Aczel, Laura Crosilla, Hajime Ishihara, Erik Palmgren, and Peter Schuster. Binary refinement implies discrete exponentiation. Studia Logica, 84(3) :361–368, 2006. | DOI | MR | Zbl

[2] Peter Aczel and Michael Rathjen. Notes on constructive set theory. Technical report, Institut Mittag–Leffler, 2000/01. Report No. 40.

[3] Peter Aczel and Michael Rathjen. Constructive set theory. Book draft, 2010.

[4] Errett Bishop. Foundations of Constructive Analysis. McGraw-Hill, New York, 1967. | DOI | Zbl

[5] Errett Bishop and Douglas Bridges. Constructive Analysis. Springer, Berlin, 1985. | Zbl

[6] Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics, volume 97 of London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge, 1987. | DOI | Zbl

[7] Douglas S. Bridges and Luminita Simona Vita. Techniques of Constructive Analysis. Universitext. Springer-Verlag, New York, 2006. | DOI | MR | Zbl

[8] Jan Cederquist and Thierry Coquand. Entailment relations and distributive lattices. In Samuel R. Buss, Petr Hájek, and Pavel Pudlák, editors, Logic Colloquium ’98 : Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Prague, Czech Republic, August 9–15, 1998, volume 13 of Lect. Notes Logic, pp. 127–139. AK Peters/Springer, 2000. | DOI | Zbl

[9] Jan Cederquist, Thierry Coquand, and Sara Negri. The Hahn-Banach Theorem in Type Theory. In Giovanni Sambin and Jan M. Smith, editors, Twenty-Five Years of Constructive Type Theory. Oxford University Press, Oxford, 1998. | DOI | Zbl

[10] Thierry Coquand. Two applications of Boolean models. Arch. Math. Logic, 37(3) :143–147, 1998. | DOI | MR | Zbl

[11] Thierry Coquand. A direct proof of the localic Hahn-Banach theorem, 2000. http://www.cse.chalmers.se/~coquand/hahn.ps

[12] Thierry Coquand. Topology and sequent calculus. Conference presentation, June 2000. Topology in Computer Science : Constructivity ; Asymmetry and Partiality ; Digitization. Dagstuhl. http://www.cse.chalmers.se/~coquand/sequents.ps

[13] Thierry Coquand. Geometric Hahn-Banach theorem. Math. Proc. Cambridge Philos. Soc., 140(2) :313–315, 2006. | DOI | MR | Zbl

[14] Thierry Coquand, Henri Lombardi, and Stefan Neuwirth. Lattice-ordered groups generated by an ordered group and regular systems of ideals. Rocky Mountain J. Math. Forthcoming, 2019. | DOI | MR | Zbl

[15] Thierry Coquand and Stefan Neuwirth. An introduction to Lorenzen’s “Algebraic and logistic investigations on free lattices” (1951). Preprint, 2017. | arXiv

[16] Michel Coste, Henri Lombardi, and Marie-Françoise Roy. Dynamical method in algebra : effective Nullstellensätze. Ann. Pure Appl. Logic, 111(3) :203–256, 2001. | DOI | Zbl

[17] Laura Crosilla, Hajime Ishihara, and Peter Schuster. On constructing completions. J. Symbolic Logic, 70(3) :969–978, 2005. | DOI | MR | Zbl

[18] Giulio Fellin. The Jacobson Radical : from Algebra to Logic. Master’s thesis. Università di Verona, Dipartimento di Informatica, 2018.

[19] Giulio Fellin, Peter Schuster, and Daniel Wessel. The Jacobson radical of a propositional theory. Submitted, 2019.

[20] László Fuchs. Partially Ordered Algebraic Systems. Dover Publications, Mineola, New York, 2011.

[21] Paul Howard and Jean E. Rubin. Consequences of the Axiom of Choice, volume 59 of Mathematical Surveys and Monographs. American Mathematical Society, Providence, Rhode Island, 1998. | DOI | Zbl

[22] Hajime Ishihara. On the constructive Hahn-Banach theorem. Bull. Lond. Math. Soc., 21(1) :79–81, 1989. | DOI | MR | Zbl

[23] Hajime Ishihara. An omniscience principle, the König lemma and the Hahn-Banach theorem. Z. Math. Logik Grundlagen Math., 36(3) :237–240, 1990. | DOI | Zbl

[24] Hajime Ishihara. Constructive functional analysis : an introduction. In Klaus Mainzer, Peter Schuster, and Helmut Schwichtenberg, editors, Proof and Computation. Autumn School, Fischbachau, October 2016. World Scientific, Singapore, 2018. | DOI

[25] Henri Lombardi and Claude Quitté. Commutative Algebra : Constructive Methods : Finite Projective Modules. Springer Netherlands, Dordrecht, 2015. | DOI | Zbl

[26] Paul Lorenzen. Algebraische und logistische Untersuchungen über freie Verbände. J. Symbolic Logic, 16(2) :81–106, 1951. | DOI | Zbl

[27] Robert S. Lubarsky and Michael Rathjen. On the constructive Dedekind reals. Log. Anal., 1(2) :131–152, 2008. | DOI | MR | Zbl

[28] Christopher J. Mulvey and Joan Wick-Pelletier. A globalization of the Hahn-Banach theorem. Adv. Math., 89 :1–59, 1991. | DOI | MR | Zbl

[29] Lawrence Narici and Edward Beckenstein. The Hahn-Banach theorem : the life and times. Topology Appl., 77(2) :193–211, 1997. | DOI | MR | Zbl

[30] Sara Negri, Jan von Plato, and Thierry Coquand. Proof-theoretical analysis of order relations. Arch. Math. Logic, 43 :297–309, 2004. | DOI | MR | Zbl

[31] Thomas Powell, Peter Schuster, and Franziskus Wiesnet. An algorithmic approach to the existence of ideal objects in commutative algebra. In Rosalie Iemhoff, Michael Moortgat, and Ruy de Queiroz, editors, 26th Workshop on Logic, Language, Information and Computation (WoLLIC 2019), Utrecht, Netherlands, 2–5 July 2019, Proceedings, volume 11541 of Lect. Notes Comput. Sci., pp. 533–549. Springer-Verlag, Berlin, 2019. | DOI | Zbl

[32] Davide Rinaldi and Peter Schuster. A universal Krull-Lindenbaum theorem. J. Pure Appl. Algebra, 220(9) :3207–3232, 2016. | DOI | MR | Zbl

[33] Davide Rinaldi, Peter Schuster, and Daniel Wessel. Eliminating disjunctions by disjunction elimination. Bull. Symbolic Logic, 23(2) :181–200, 2017. | DOI | MR | Zbl

[34] Davide Rinaldi, Peter Schuster, and Daniel Wessel. Eliminating disjunctions by disjunction elimination. Indag. Math. (N.S.), 29(1) :226–259, 2018. | DOI | MR | Zbl

[35] Davide Rinaldi and Daniel Wessel. Cut elimination for entailment relations. Arch. Math. Logic, 58(5–6) :605–625, 2019. | DOI | MR | Zbl

[36] Davide Rinaldi and Daniel Wessel. Extension by conservation. Sikorski’s theorem. Log. Methods Comput. Sci., 14(4 :8) :1–17, 2018. | Zbl

[37] Walter Rudin. Functional Analysis. McGraw-Hill, New York, 1991. | Zbl

[38] Giovanni Sambin. Some points in formal topology. Theoret. Comput. Sci., 305(1-3) :347–408, 2003. | DOI | MR | Zbl

[39] Konstantin Schlagbauer. Ein syntaktischer Zugang zu Erweiterungssätzen. Master’s thesis. Ludwig-Maximilians-Universität München, Mathematisches Institut, 2017.

[40] Helmut Schwichtenberg. Minimal from classical proofs. In E. Börger et al., editors, Computer Science Logic. 5th Workshop, CSL ’91, Berne, Switzerland, October 7-11, 1991, Proceedings, volume 626 of Lect. Notes Comput. Sci., pp. 326–328. Springer, Berlin, 1992. | DOI | Zbl

[41] Dana Scott. Completeness and axiomatizability in many-valued logic. In Leon Henkin, John Addison, C.C. Chang, William Craig, Dana Scott, and Robert Vaught, editors, Proceedings of the Tarski Symposium (Proc. Sympos. Pure Math., Vol. XXV, Univ. California, Berkeley, Calif., 1971), pp. 411–435. Amer. Math. Soc., Providence, RI, 1974. | DOI

[42] Joseph R. Shoenfield. Mathematical Logic. Addison-Wesley, Reading, MA, 1967. | DOI | Zbl

[43] D. J. Shoesmith and T. J. Smiley. Multiple-Conclusion Logic. Cambridge University Press, Cambridge, 1978. | DOI | Zbl

[44] Anne S. Troelstra and Dirk van Dalen. Constructivism in Mathematics. An Introduction, volume 121 of Studies in Logic and the Foundations of Mathematics. Elsevier Science, 1988. | DOI

[45] Daniel Wessel. A note on connected reduced rings. J. Comm. Algebra. Forthcoming, 2019.

[46] Daniel Wessel. Ordering groups constructively. Comm. Algebra. Forthcoming, 2019. | DOI | MR | Zbl

[47] Ihsen Yengui. Making the use of maximal ideals constructive. Theoret. Comput. Sci., 392 :174–178, 2008. | DOI | MR | Zbl

[48] Ihsen Yengui. Constructive commutative algebra. Projective modules over polynomial rings and dynamical Gröbner bases, volume 2138 of Lecture Notes in Mathematics. Springer, Cham, 2015. | DOI | Zbl