Fabián Fernando Serrano Suárez UNAL Manizales, Colombia

Thaynara Arielly de Lima Universidade Federal de Goiáis, Brasil

Mauricio Ayala-Rincón Universidade de Brasília, Brasil

--//--

This project contains the Isabell/HOL formalization of the compactness theorem for propositional logic using Smullyan's model existence theorem approach according to Fitting presentation. In addition, it contains three applications:

1. formalizations of Hall's theorem for the set- and the graph-theoretical case for countable sets and graphs;
2. a formalization of de Bruijn-Erdös k-coloring theorem for countable graphs;
3. and, a formalization of König's Lemma.

Except for the graph-theoretical version of Hall's theorem, obtained from the set-theoretical version of Hall's theorem, the applications are proved constructively building sets of propositional formulas and models, and applying the compactness theorem.

--//--