ABSTRACT. Transitive closure logic is obtained by a modest addition to first-order logic that affords enormous expressive power. Most importantly, it provides a uniform way of capturing finitary inductive definitions. Thus, particular induction principles do not need to be added to the logic; instead, all induction schemes are available within a single, unified language. We here present a non-well-founded proof system for transitive closure logic which is complete for the standard semantics. This system captures implicit induction, and its soundness is underpinned by the principle of infinite descent. We also consider its subsystem of cyclic proofs.