A Simple Deduction System for First-Order Logic with Equality, Free Constructors and Induction
Jean Goubault-Larrecq, Jean Goubault-larrecq, Projet Coq · 1999
: Proof systems like Coq feature inductive datatypes, where datatype constructors are free in the sense that two terms built from constructors only are semantically equal if and only if they are syntactically identical. Although free constructors are an essential ingredient of modern formalized mathematics, no automated first-order prover has been specialized with built-in rules for dealing with free constructors, until now. We propose a sequent system for a logic where terms can be built only from variables and free constructors. Thus the logic will be kept simple, as equality in the logic will be syntactical equality. We show how partial functions can be introduced into the logic, in the form of predicates obeying some functionality constraints. We prove that the resulting system is sound and complete with respect to a natural first-order semantics of datatypes, and enjoys cut elimination. We then develop a tableau calculus to find proofs in this sequent system. This involves solving...