Arithmetic as a Theory Modulo

We present constructive arithmetic in Deduction modulo with rewrite rules only. In natural deduction and in sequent calculus, the cut elimination theorem and the analysis of the structure of cut free proofs is the key to many results about predicate logic with no axioms: analyticity and non-provability results, completeness results for proof search algorithms, decidability results for fragments, constructivity results for the intuitionistic case. . . Unfortunately, the properties of cut free proofs do not extend in the presence of axioms and the cut elimination theorem is not as powerful in this case as it is in pure logic. This motivates the extension of the notion of cut for various axiomatic theories such as arithmetic, Church’s simple type theory, set theory and others. In general, we can say that a new axiom will necessitate a specific extension of the notion of cut: there still is no notion of cut general enough to be applied to any axiomatic theory. Deduction modulo [2, 3] is...

• Type: Conference
• Year: 2005
• Where: RTA
• Authors: Gilles Dowek, Benjamin Werner
• Keywords: Cut Free Proofs, Deduction Modulo, Rewrite Rules, RTA 2005, Theoretical Computer Science