Unified Classical Logic Completeness

Abstract. Codatatypes are absent from many programming languages and proof assistants. We make a case for their importance by revisiting a classic result: the completeness theorem for first-order logic established through a Gentzen system. The core of the proof establishes an abstract property of possibly infinite deriva-tion trees, independently of the concrete syntax or inference rules. This separation of concerns simplifies the presentation. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems as well as various flavors of first-order logic. The corresponding Isabelle/HOL formalization demonstrates the re-cently introduced support for codatatypes and the Haskell code generator.