Formalizing Ordinal Partition Relations Using Isabelle/HOL

References

• Avigad, J., Hölzl, J., Serafin, L. (2017). A formally verified proof of the central limit theorem. J. Autom. Reason. 59(4): 389–423.
   Web of Science ®Google Scholar
• Blanchette, J. C., Nipkow, T. (2010). Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L. C., eds. Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, Springer; pp. 131–146.
   Google Scholar
• Bulwahn, L. (2012). The new Quickcheck for Isabelle. In Hawblitzel, C., Miller, D., eds. Certified Programs and Proofs, LNCS Vol. 7679; pp. 92–108. Springer.
   Google Scholar
• Carroy, R., Pequignot, Y. (2020). Well, better and in-between. In: Monika Seisenberger, Peter Schuster, Andreas Weiermann, eds. Well Quasi-orders in Computation, Logic, Language and Reasoning. Springer; pp. 1–27.
   Google Scholar
• Chang, C-C. (1972). A partition theorem for the complete graph on ωω. J. Comb. Theory. (A). 12: 396–452.
   Google Scholar
• Church, A. (1940). A formulation of the simple theory of types. J. Symb. Log. 5: 56–68. doi:https://doi.org/10.2307/2266170
   Google Scholar
• Cohen, P. (1966). Set Theory and the Continuum Hypothesis. New York: Benjamin.
   Google Scholar
• Džamonja, M. (2020). Fast Track to Forcing. Cambridge: Cambridge University Press.
   Google Scholar
• Erdős, P. (1987). Some problems on finite and infinite graphs. In Logic and combinatorics (Arcata, Calif., 1985), Volume 65 of Contemp. Math. Providence, RI: Amer. Math. Soc.; pp. 223–228
   Google Scholar
• Erdős, P., Rado, R. (1956). A partition calculus in set theory. Bull. Amer. Math. Soc. 62(427/489): 427–489. doi:https://doi.org/10.1090/S0002-9904-1956-10036-0
   Google Scholar
• Erdös, P., Hajnal, A., Mate, A., Rado, R. (1984). Combinatorial Set Theory: Partition Relations for Cardinals. Studies in Logic and the Foundations of Mathematics 106. Elsevier Science Ltd.
   Google Scholar
• Erdős, P., Milner, E. C. (1972). A theorem in the partition calculus. Canad. Math. Bull. 15(4): 501–505.
   Web of Science ®Google Scholar
• Erdős, P., Milner, E. C. (1974). A theorem in the partition calculus corrigendum. Canad. Math. Bull. 17(2): 305.
   Google Scholar
• Galvin, F., Larson, J. A. (1974). Pinning countable ordinals. Fund. Math. 82: 357–361. doi:https://doi.org/10.4064/fm-82-4-357-361
   Google Scholar
• Galvin, F., and Prikry, Karel L. (1973). Borel sets and Ramsey’s theorem. J. Symb. Log. 38: 192–198. doi:https://doi.org/10.2307/2272055
   Web of Science ®Google Scholar
• Gordon, M. J. C. (2015). Tactics for mechanized reasoning: A commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’. Philos. Trans. R. Soc. A. 373(2039).
   Google Scholar
• Hajnal, A., Larson, J. A. (2010). Partition relations. In M. Foreman, A. Kanamori, eds. Handbook of Set Theory, Vol. 1, Springer; pp. 120–213.
   Google Scholar
• Hales, T., Adams, M., Bauer, G., Dang, T. D., Harrison, J., Hoang, L. T., Kaliszyk, C., Magron, V., Mclaughlin, S., Nguyen, T. T., et al. (2017). A formal proof of the Kepler conjecture. Forum Math. Pi. 5:e2.
   Web of Science ®Google Scholar
• Hales, T. C. (2007). The Jordan curve theorem, formally and informally. Amer. Math. Monthly. 114(10): 882–894.
   Web of Science ®Google Scholar
• Harrison, J. (2000). Floating point verification in HOL: Light: the exponential function. Form. Methods Syst. Des. 16: 271–305.
   Web of Science ®Google Scholar
• Harrison, J. (2009). Formalizing an analytic proof of the prime number theorem. J. Autom. Reason. 43(3): 243–261.
   Web of Science ®Google Scholar
• Hodkinson, I. (2003). Kruskal’s theorem and Nash-Williams theory, after Wilfrid Hodges. version 3.6. Available at: www.doc.ic.ac.uk/imh/papers/bar.pdf, February.
   Google Scholar
• Hölzl, J., Heller, A. (2011). Three chapters of measure theory in Isabelle/HOL. In: Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F., eds. Interactive Theorem Proving — Second International Conference, LNCS 6898. Springer; pp. 135–151.
   Google Scholar
• van Benthem Jutting, L.S. (1977). Checking Landau’s “Grundlagen” in the AUTOMATH System. PhD thesis, Eindhoven University of Technology. doi:https://doi.org/10.6100/IR23183.
   Google Scholar
• Kalvala, S. HOL around the world. In: Archer, M., Joyce, J. J., Levitt, K. N., Windley, P. J., eds. International Workshop on the HOL Theorem Proving System and its Applications. IEEE Computer Society, 1991; pp. 4–12.
   Google Scholar
• Kunen, K. (1980). Set Theory, volume 102 of Studies in Logic and the Foundations of Mathematics. North-Holland.
   Google Scholar
• Kříž, I., Thomas, R. (1991). Analyzing Nash-Williams’ partition theorem by means of ordinal types. Discrete Math. 95(1–3): 135–167. Directions in infinite graph theory and combinatorics (Cambridge, 1989).
   Web of Science ®Google Scholar
• Larson, J. A. (1973). A short proof of a partition theorem for the ordinal ωω. Ann. Math. Logic. 6: 129–145.
   Google Scholar
• Laver, R. (1971). On Fraïssé’s order type conjecture. Ann. Math. 93(1): 89–111.
   Web of Science ®Google Scholar
• Marcone, A. (1996). On the logical strength of Nash-Williams’ theorem on transfinite sequences. In: W. Hodges, M. Hyland, C. Steinhorn, J. Truss, eds. Logic: from Foundations to Applications; European logic colloquium. Clarendon Press, 1996, pp. 327–351.
   Google Scholar
• Nash-Williams, C. St. J. A. (1965). On well-quasi-ordering transfinite sequences. Proc. Cambridge Philos. Soc. 61: 33–39. doi:https://doi.org/10.1017/S0305004100038603
   Web of Science ®Google Scholar
• Nicely, T. R. Pentium FDIV flaw, 2011. FAQ. Available at: https://faculty.lynchburg.edu/nicely/pentbug/pentbug.html.
   Google Scholar
• Nipkow, T., Paulson, L. C., Wenzel, M. (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer. Available at http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf.
   Google Scholar
• Owre, S., Rajan, S., Rushby, J. M., Shankar, N., Srivas, M. K. (1996). PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T. A. eds. Computer Aided Verification: 8th International Conference, CAV ’96, LNCS 1102, Springer; pp. 411–414.
   Google Scholar
• Paulson, L. C. (2019). Zermelo Fraenkel set theory in higher-order logic. Archive of Formal Proofs, October. Available at: http://isa-afp.org/entries/ZFC_in_HOL.html, Formal proof development.
   Google Scholar
• Paulson, L. C. (2020). The Nash-Williams partition theorem. Archive of Formal Proofs, May. Available at: http://isa-afp.org/entries/Nash_Williams.html, Formal proof development.
   Google Scholar
• Paulson, L. C. (2020).Ordinal partitions. Archive of Formal Proofs, August. Available at: http://isa-afp.org/entries/Ordinal_Partitions.html, Formal proof development.
   Google Scholar
• Paulson, L. C., Nipkow, T., Wenzel, M. (2019). From LCF to Isabelle/HOL. Formal Aspects Comput. 31(6): 675–698. doi:https://doi.org/10.1007/s00165-019-00492-1
   Web of Science ®Google Scholar
• Ramsey, F. P. (1929). On a problem of formal logic. Proc. London Math. Soc. (2), 30(4): 264–286.
   Google Scholar
• Schipperus, R. (1999). Countable partition ordinals. PhD thesis, University of Colorado-Boulder.
   Google Scholar
• Schipperus, R. (2010). Countable partition ordinals. Ann. Pure Appl. Log. 161(10): 1195–1215.
   Web of Science ®Google Scholar
• Specker, E. (1956). Teilmengen von Mengen mit Relationen. Commentarii Mathematici Helvetici. 31: 302–314. doi:https://doi.org/10.1007/BF02564361
   Google Scholar
• Todorčević, S. (1987). Partitioning pairs of countable ordinals. Acta Math. 159(3/4): 261–294.
   Web of Science ®Google Scholar
• Todorčević, S. (1989). Partition Problems in Topology. Providence, RI: Amer. Math. Soc.
   Google Scholar
• Todorcevic, S. (2010). Introduction to Ramsey spaces, volume 174 of Annals of Mathematics Studies. Princeton, NJ: Princeton University Press.
   Google Scholar
• Freek Wiedijk. (2000). The De Bruijn factor. Technical report. Nijmegen, Netherlands: Department of Computer Science Nijmegen University. Available at: http://www.cs.ru.nl/freek/factor/.
   Google Scholar