Dependent choice as a termination principle

Research output: Contribution to journalArticlepeer-review


We introduce a new formulation of the axiom of dependent choice, which can be viewed as an abstract termination principle that in particular generalises recursive path orderings, the latter being fundamental tools used to establish termination of rewrite systems. We consider several variants of our termination principle, and relate them to general termination theorems in the literature.
Original languageEnglish
Pages (from-to)503-516
Number of pages14
JournalArchive for Mathematical Logic
Issue number3-4
Early online date16 Jan 2020
Publication statusPublished - 1 May 2020


  • Arithmetic in all finite types
  • Dependent choice
  • Higher order reverse mathematics
  • Path orderings
  • Termination

ASJC Scopus subject areas

  • Philosophy
  • Logic


Dive into the research topics of 'Dependent choice as a termination principle'. Together they form a unique fingerprint.

Cite this