A formal approach to Menger's theorem
Choose format
RIS BIB ENDNOTEA formal approach to Menger's theorem
Publication date: 28.11.2022
Reports on Mathematical Logic, 2022, Number 57, pp. 45-51
https://doi.org/10.4467/20842589RM.22.003.16660Authors
A formal approach to Menger's theorem
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 suficiently many disjoint paths, we recover Menger's theorem by way of completeness.
[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ák (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, Über 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, Über trennende Knotenpunkte in Graphen (nebst Anwendungen auf Determinanten und Matrizen), Acta Sci. Math. (Szeged) 6:2-3, (1932-34), 155-179.
[17] L. Lovász, 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
Information: Reports on Mathematical Logic, 2022, Number 57, pp. 45-51
Article type: Original article
Carl Friedrich von Weizsäcker-Zentrum, Universität Tübingen
Dipartimento di Informatica, Università degli Studi di Verona Strada le Grazie 15, 37134 Verona, Italy
Published at: 28.11.2022
Received at: 09.12.2021
Article status: Open
Licence: CC BY
Percentage share of authors:
Classification number:
Article corrections:
-Publication languages:
English