A formal approach to Menger's theorem

Roberta Bonacina,

Daniel Misselbeck-Wessel


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.

AMS subject classification: 05C40, 05C20, 03B35.

Słowa kluczowe: Disjoint paths, separating set, inductive definition, entailment

[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