The authors develop and compare proof-theoretic foundations for proof by induction and proof by infinite descent in the context of a first-order logic \(\text{FOL}_{\text{ID}}\) containing inductively defined predicates. These two styles of reasoning are formalized as the corresponding sequent calculi. It is shown that the proof system \(\text{LKID}\), formalizing proof by induction, is complete relative to a class of Henkin models, and that the infinitary proof system \(\text{LKID}^{\omega}\), formalizing proof by infinite descent, is complete relative to the more restrictive class of standard models and is strictly more powerful. Essentially, by transfinite induction up to \(\varepsilon_0\), it is shown that the cut rule is eliminable in both calculi, \(\text{LKID}\) and \(\text{LKID}^{\omega}\). A system \(\text{CLKID}^{\omega}\), consisting of cyclic proofs, is introduced as a natural subsystem of \(\text{LKID}^{\omega}\). The authors' main conjecture is that \(\text{LKID}^{\omega}\) and \(\text{CLKID}^{\omega}\) are equivalent. This approachable and self-contained paper could stimulate a wider interest in proof systems of such kind.