109- of references

This is a formalization of an abstract property of possibly infinite derivation trees (modeled by a codatatype), that represents the core of a Beth–Hintikka-style proof of the first-order logic completeness theo-rem and is independent of the concrete syntax or inference rules. This work is described in detail in a publication by the authors [2]. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems as well as various flavors of FOL—e.g., with or without predicates, equality, or sorts. Here, we give only a toy ex-ample instantiation with classical propositional logic. A more serious instance—many-sorted FOL with equality—is described elsewhere [1]