Dependent choice as a termination principle

Archive for Mathematical Logic 59 (3-4):503-516 (2020)
  Copy   BIBTEX

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.

Categories

Add categories

Keywords

Reprint years

DOI

10.1007/s00153-019-00706-6

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,423

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

A general theorem on termination of rewriting.Jeremy E. Dawson - unknown
Extensions of arithmetic for proving termination of computations.Clement F. Kent & Bernard R. Hodgson - 1989 - Journal of Symbolic Logic 54 (3):779-794.
Modular termination of basic narrowing and equational unification.María Alpuente, Santiago Escobar & José Iborra - 2011 - Logic Journal of the IGPL 19 (6):731-762.
Strong termination for the epsilon substitution method.Grigori Mints - 1996 - Journal of Symbolic Logic 61 (4):1193-1205.
Strong Termination for the Epsilon Substitution Method.Grigori Mints - 1996 - Journal of Symbolic Logic 61 (3):1193-1205.
The rigid relation principle, a new weak choice principle.Joel David Hamkins & Justin Palumbo - 2012 - Mathematical Logic Quarterly 58 (6):394-398.
Effect of delayed conditioned stimulus termination on extinction of an avoidance response following different termination conditions during acquisition.Allen C. Israel, Vernon T. Devine, Margaret A. O'Dea & Mark E. Hamdi - 1974 - Journal of Experimental Psychology 103 (2):360.
Genetic counseling and termination of pregnancy in hungary.Zoltan Papp - 1989 - Journal of Medicine and Philosophy 14 (3):323-333.
Bounding derivation lengths with functions from the slow growing hierarchy.Andreas Weiermann - 1998 - Archive for Mathematical Logic 37 (5-6):427-441.
Is the Choice on Termination of Pregnancy Act Guilty of Disability Discrimination?S. Hall - 2013 - South African Journal of Philosophy 32 (1):36-46.
Direct and Indirect Abortion in the Roman Catholic Tradition: A Review of the Phoenix Case. [REVIEW]S. S. Coleman - 2013 - HEC Forum 25 (2):127-143.
Freedom of Conscience, Employee Prerogatives, and Consumer Choice: Veal, Birth Control, and Tanning Beds.J. M. Dieterle - 2008 - Journal of Business Ethics 77 (2):191-203.
The Boolean Prime Ideal Theorem Plus Countable Choice Do Not Imply Dependent Choice.Paul Howard & Jean E. Rubin - 1996 - Mathematical Logic Quarterly 42 (1):410-420.
Epsilon Substitution Method for Δ11 − CR: a Constructive Termination Proof.Sergei Tupailo - 2003 - Logic Journal of the IGPL 11 (3):367-377.
On the termination of russell’s description elimination algorithm.Clemens Grabmayer, Joop Leo, Vincent van Oostrom & Albert Visser - 2011 - Review of Symbolic Logic 4 (3):367-393.

Analytics

Added to PP
2020-01-16

Downloads
8 (#1,291,989)

6 months
2 (#1,240,909)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Proof-theoretic analysis of termination proofs.Wilfried Buchholz - 1995 - Annals of Pure and Applied Logic 75 (1-2):57-65.
The equivalence of bar recursion and open recursion.Thomas Powell - 2014 - Annals of Pure and Applied Logic 165 (11):1727-1754.

Add more references