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

1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
6 MAREL - Models And Reuse Engineering, Languages
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier
9 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Abstract : Defining 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.
Type de document :
Communication dans un congrès
Domaine :

https://hal-mines-paristech.archives-ouvertes.fr/hal-01441751
Contributeur : Claire Medrala <>
Soumis le : vendredi 20 janvier 2017 - 11:10:53
Dernière modification le : jeudi 19 décembre 2019 - 01:32:31

### Fichier

A-654.pdf
Fichiers produits par l'(les) auteur(s)

### Identifiants

• HAL Id : hal-01441751, version 1

### Citation

Ali Assaf, Guillaume Burel, Raphal Cauderlier, David Delahaye, Gilles Dowek, et al.. Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system. TYPES: Types for Proofs and Programs, May 2016, Novi SAd, Serbia. ⟨hal-01441751⟩

### Métriques

Consultations de la notice

## 951

Téléchargements de fichiers