Dependent choice as a termination principle

Research output: Contribution to journalArticlepeer-review

Abstract

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
Volume59
Issue number3-4
Early online date16 Jan 2020
DOIs
Publication statusPublished - 1 May 2020

Keywords

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

ASJC Scopus subject areas

  • Philosophy
  • Logic

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

Cite this