MPI-I-94-234
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: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1994-234
BibTeX
@TECHREPORT{MatthewsSimpson94,
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},
}