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
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
- Background_on_graphs
- SyntaxAndSemantics
- UniformNotation
- Closedness
- FinitenessClosedCharProp
- MaximalSet
- HintikkaTheory
- MaximalHintikka
- BinaryTreeEnumeration
- FormulaEnumeration
- ModelExistence
- PropCompactness
- Hall_Theorem
- Hall_Theorem_Graphs
- k_coloring
- KoenigLemma