Classical and constructive logics together: Ecumenical systems
Much has been said about intuitionistic and classical logical systems since Gentzen’s seminal work. Recently Prawitz, Dowek and others, have been discussing how to put together Gentzen’s systems for classical and intuitionistic logic into a single system. This has been called Ecumenical Logic. I will present an ecumenical sequent calculus and state some of its proof theoretical properties. This approach to an unified system, enabling both classical and intuitionistic features, should shed some light not only on the logics themselves, but also in the ways they can interoperate. This in turn should help enhance the interoperability of proof assistants, to enable seamless communication between them, as discussed in the recent PhD thesis of Emilie Grienneberger, a student of under Gilles Dowek.