לירון כהן

Many efforts have been made in recent years to construct formal systems for mechanizing mathematical reasoning. A framework which seems particularly suitable for this task is ancestral logic - the logic obtained by augmenting first-order logic with a transitive closure operator. While the study of this logic has so far been mostly model-theoretical, this work is devoted to its proof theory (which is much more relevant for the task of mechanizing mathematics). We develop a Gentzen-style proof system TC_G which is sound for ancestral logic, and prove its equivalence to previous systems for the reflexive transitive closure operator by providing translation algorithms between them. We further provide evidence that TC _G indeed encompasses all forms of reasoning for this logic that are used in practice. The central rule of TC_G is an induction rule which generalizes that of Peano Arithmetic (PA). In the case of arithmetics we show that the ordinal number of TC _G is ε₀.