Compactness Theorem for Propositional Logic and Combinatorial Applications

Fabián Fernando Serran Suárez 📧, Thaynara Arielly de Lima 📧 and Mauricio Ayala-Rincón 📧

August 19, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This theory formalises the compactness theorem for propositional logic based on the model existence theorem approach. It also presents applications of the compactness theorem to formalize combinatorial theorems over countable structures: the de Bruijn-Erdős Graph coloring theorem for countable graphs, König's Lemma, and set- and graph-theoretical versions of Hall’s Theorem for countable families of sets and graphs.

License

BSD License

Topics

Related publications

  • Serrano Suárez, F. F., Ayala-Rincón, M., & de Lima, T. A. (2022). Hall’s Theorem for Enumerable Families of Finite Sets. Intelligent Computer Mathematics, 107–121. https://doi.org/10.1007/978-3-031-16681-5_7

Session Prop_Compactness

Depends on

Cite

× 
@article{Prop_Compactness-AFP,
  author  = {Fabián Fernando Serran Suárez and Thaynara Arielly de Lima and Mauricio Ayala-Rincón},
  title   = {Compactness Theorem for Propositional Logic and Combinatorial Applications},
  journal = {Archive of Formal Proofs},
  month   = {August},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/Prop_Compactness.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest