Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system

International audienceDefining a theory, such as arithmetic, geometry, or set theory, in predicate logic just requires to chose function and predicate symbols and axioms, that express the meaning of these symbols. Using, this way, a single logical framework, to define all these theories, has many advantages. First, it requires less efforts, as the logical connectives, ∧, ∨, ∀... and their associated deduction rules are defined once and for all, in the framework and need not be redefined for each theory. Similarly, the notions of proof, model... are defined once and for all. And general theorems, such as the soundness and the completeness theorems, can be proved once and for all. Another advantage of using such a logical framework is that this induces a partial order between theories. For instance, Zermelo-Fraenkel set theory with the axiom of choice (ZFC) is an extension of Zermelo-Fraenkel set theory (ZF), as it contains the same axioms, plus the axiom of choice. It is thus obvious that any theorem of ZF is provable in ZFC, and for each theorem of ZFC, we can ask the question of its provability in ZF. Several theorems of ZFC, that are provable in ZF have been identified, and these theorems can be used in extensions of ZF that are inconsistent with the axiom of choice. Finally, using such a common framework permits to combine, in a proof, lemmas proved in different theories: if T is a theory expressed in a language L and T a theory expressed in a language L , if A is expressed in L ∩ L , A ⇒ B is provable in T , and A is provable in T , then B is provable in T ∪ T. Despite these advantages, several logical systems have been defined, not as theories in predicate logic, but as independent systems: Simple type theory, also known as Higher-order logic, is defined as an independent system—although it is also possible to express it as a theory in predicate logic. Similarly, Intuitionistic type theory, the Calculus of constructions, the Calculus of inductive constructions... are defined as independent systems. As a consequence, it is difficult to reuse a formal proof developed in an automated or interactive theorem prover based on one of these formalisms in another, without redeveloping it. It is also difficult to combine lemmas proved in different systems: the realm of formal proofs is today a tower of Babel, just like the realm of theories was, before the design of predicate logic. The reason why these formalisms have not been defined as theories in predicate logic is that predicate logic, as a logical framework, has several limitations, that make it difficult to express modern logical systems