A formal approach to Menger's theorem

• Autorzy: Bonacina Roberta , Misselbeck-Wessel Daniel

Identyfikatory

DOI

10.4467/20842589RM.22.003.16660

• Języki publikacji: EN

Abstrakty

EN

Menger’s graph theorem equates the minimum size of a separating set for non-adjacent vertices a and b with the maximum number of disjoint paths between a and b. By capturing separating sets as models of an entailment relation, we take a formal approach to Menger’s result. Upon showing that inconsistency is characterised by the existence of sufficiently many disjoint paths, we recover Menger’s theorem by way of completeness.

Słowa kluczowe

EN

disjoint paths; separating set; inductive definition; entailment

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2022
• Tom: Vol. 57
• Strony: 45--51
• Opis fizyczny: Bibliogr. 31 poz., rys.

Twórcy

autor

Bonacina Roberta

• Carl Friedrich von Weizsäcker-Zentrum, Universität Tübingen

autor

Misselbeck-Wessel Daniel

• Daniel Misselbeck-Wessel Dipartimento di Informatica, Universit`a di Verona

Bibliografia

• [1] T. Böhme, F. Göring, and J. Harant, Menger’s Theorem, J. Graph Theory 37:1 (2001), 35–36.
• [2] R. Bonacina and D. Wessel, Ribenboim’s order extension theorem from a constructive point of view, Algebra Universalis 81:5 (2020), https://doi.org/10.1007/s00012-019-0634-0.
• [3] J. Cederquist and T. Coquand, Entailment relations and distributive lattices, in: Logic Colloquium ’98. Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Prague, Czech Republic, August 9–15, 1998, S. R. Buss, P. Hájek and P. Pudl´ak (Eds.), Lect. Notes Logic, A. K. Peters, Natick, MA, 2000, pp.127–139.
• [4] T. Coquand, A syntanctical proof of the Marriage Lemma, Theoret. Comput. Sci. 290:1 (2003), 1107–1113.
• [5] T. Coquand and Guo-Qiang Zhang, Sequents, frames, and completeness, in: Computer Science Logic (Fischbachau, 2000), P. G. Clote and H. Schwichtenberg (Eds.), volume 1862 of Lecture Notes in Comput. Sci., Springer, Berlin 2000, pp. 277–291.
• [6] R. Diestel. Graph Theory, volume 173 of Graduate Texts in Mathematics, fifth edition, Springer, Berlin 2017.
• [7] G.A. Dirac, Short proof of Menger’s graph theorem, Mathematika 13:1 (1966), 42–44.
• [8] C. Dittmann, Menger’s Theorem, Archive of Formal Proofs, 2017. http://isa-afp.org/entries/Menger.html, Formal proof development.
• [9] Ch. Doczkal, Short proof of Menger’s Theorem in Coq (Proof Pearl), Technical report, 2019. URL: http://www-sop.inria.fr/members/Christian.Doczkal/pdf/menger.pdf.
• [10] F. Göring, Short proof of Menger’s theorem, Discrete Math. 219 (2000), 295–296.
• [11] F. Göring, A proof of Menger’s theorem by contraction. Discuss. Math. Graph Theory 22 (2002), 111–112.
• [12] T. Grünwald (later Gallai), Ein neuer Beweis eines Mengerschen Satzes, J. Lond. Math. Soc. 13 (1938), 188–192.
• [13] G. Hajós, Zum Mengerschen Graphensatz, Acta Sci. Math. (Szeged) 7 (1934-35), 44–47.
• [14] R. Halin, Uber trennende Eckenmengen in Graphen und den Mengerschen Satz, ¨ Math. Ann. 157 (1964), 34–41.
• [15] P. Halmos and H. E. Vaughan, The marriage problem, Amer. J. Math. 72 (1950), 214–215.
• [16] D. König, Uber trennende Knotenpunkte in Graphen (nebst Anwendungen auf Determinanten und ¨ Matrizen), Acta Sci. Math. (Szeged) 6:2-3, (1932-34), 155–179.
• [17] L. Lovasz, A remark on Menger’s theorem, Acta Math. Acad. Sci. Hungar. 21:3–4 (1970), 365– 368.
• [18] Y. V. Matiyasevich, The application of the methods of the theory of logical derivation to graph theory, Math. Notes Acad. Sci. USSR 12:6 (1972), 904–908.
• [19] Y. V. Matiyasevich, Metamathematical approach to proving theorems of discrete mathematics, J. Soviet Math. 10 (1978), 517–533.
• [20] W. McCuaig, A simple proof of Menger’s theorem, J. Graph Theory 8 (1984), 427–429.
• [21] K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10:1 (1927), 96–115.
• [22] K. Menger, Kurventheorie, Teubner, Hrsg. unter Mitarb. von Georg Nöbeling, Leipzig, 1932.
• [23] C. J. Mulvey and J. Wick-Pelletier, A globalization of the Hahn–Banach theorem, Adv. Math. 89 (1991), 1–59.
• [24] C. St. John Alvah Nash-Williams and W. T. Tutte, More proofs of Menger’s theorem, J. Graph Theory 1 (1977), 13–17.
• [25] S. Negri, J. von Plato and T. Coquand, Proof-theoretical analysis of order relations, Arch. Math. Logic 43 (2004), 297–309.
• [26] H. Perfect, Applications of Menger’s graph theorem, J. Math. Anal. Appl. 22 (1968), 96–111.
• [27] J. S. Pym, A proof of Menger’s theorem, Monatsh. Math. 73 (1969), 81–83.
• [28] D. Rinaldi, P. Schuster and D. Wessel, Eliminating disjunctions by disjunction elimination, Indag. Math. (N.S.) 29:1 (2018), 226–259.
• [29] D. Rinaldi and D. Wessel, Cut elimination for entailment relations, Arch. Math. Logic 58:5–6 (2019), 605–625.
• [30] D. Scott, Completeness and axiomatizability in many-valued logic, in: Proceedings of the Tarski Symposium (Proc. Sympos. Pure Math., Vol. XXV, Univ. California, Berkeley, Calif., 1971), L. Henkin, J. Addison, C.C. Chang, W. Craig, D. Scott, and R. Vaught (Eds.), Amer. Math. Soc., Providence, RI, 1974, pp. 411–435
• [31] D. Wessel, Point-free spectra of linear spreads, in: Mathesis Universalis, Computability and Proof, Synthese Library, S. Centrone, S. Negri, D. Sarikaya, and P. Schuster (Eds.), Springer, Cham, 2019, pp. 353–374

Uwagi

Opracowanie rekordu ze środków MEiN, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2022-2023).