Download PDFOpen PDF in browser

Transitive Closure Logic: Infinitary and Cyclic Proof Systems

EasyChair Preprint no. 191

5 pagesDate: May 30, 2018

Abstract

Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of the transitive closure operator uniformly captures all finitary inductive definitions. We present an infinitary proof system for transitive closure logic which is an infinite descent-style counterpart to the existing (explicit induction) proof system for the logic. We show that, as for similar systems for first-order logic with inductive definitions, our infinitary system is complete for the standard semantics and subsumes the explicit system. Moreover, the uniformity of the transitive closure operator allows semantically meaningful complete restrictions to be defined using simple syntactic criteria.

Keyphrases: cyclic proofs, induction, infinitary proofs, transitive closure

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:191,
  author = {Reuben Rowe and Liron Cohen},
  title = {Transitive Closure Logic: Infinitary and Cyclic Proof Systems},
  howpublished = {EasyChair Preprint no. 191},
  doi = {10.29007/rbgb},
  year = {EasyChair, 2018}}
Download PDFOpen PDF in browser