MPI-INF/SWS Research Reports 1991-2021

1. Author,Editor - 3. with BibTeX cite keys


Reflection using the derivability conditions

Matthews, Seán and Simpson, Alex K.

July 1994, 14 pages.

Status: available - back from printing

We extend arithmetic with a new predicate $Pr$, giving axioms for it based on first order versions of L\"ob's derivability conditions. We hoped that the addition of a reflection schema mentioning $Pr$ would then give a non-conservative extension of the original arithmetic theory. The paper investigates this possiblity. It is shown that, under special conditions, the extension is indeed non-conservative. However in general such extensions turn out to be conservative.
Categories / Keywords:
Proof theory, reflection

URL to this document:

Hide details for BibTeXBibTeX
  AUTHOR = {Matthews, Se{\'a}n and Simpson, Alex K.},
  TITLE = {Reflection using the derivability conditions},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-94-234},
  MONTH = {July},
  YEAR = {1994},
  ISSN = {0946-011X},