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.
- Arithmetic in all finite types
- Dependent choice
- Higher order reverse mathematics
- Path orderings
ASJC Scopus subject areas