[FOM] Reducibility and relative consistency

[Albert Visser]

Dear Harvey and Martin,

>Could you send a brief note to Martin Davis to be posted on the FOM,
>containing a brief bibliography of published material on this?

Here it is.

Best,
Albert

------------------------------------------------

The Smorynski paper is the locus classicus for all early work by
Harvey on interpretability. It is here:

@InCollection{smor:nons85,
   author =      "C. Smory\'{n}ski",
   title =       "{Nonstandard models and related developments}",
   booktitle =   "{Harvey {F}riedman's Research on the Foundations of
Mathematics}",
   publisher =   "North Holland",
   year =        "1985",
editor = "L.A. Harrington and M.D. Morley and A. Scedrov and S.G.
Simpson",
  pages = {179--229},
   address =     "Amsterdam"
}

Since I did not fully understand the argument sketched by Craig for
the Friedman characterization, I produced my
own proof, which sharpened the result a bit by giving the
formalization of the characterization in EA. This is slightly
delicate since we need
cutfree provability in EA in stead of ordinary provability in the
statement of the characterization.  See:

@inproceedings{viss:inte90,
                 author="Visser, A.",
                 title="Interpretability logic",
                 booktitle="Mathematical logic, {P}roceedings of the
                   {H}eyting 1988 summer school in {V}arna, {B}ulgaria",
                   editor="Petkov, P.P.",
                   publisher="Plenum Press, Boston",
                 year=1990,
                 pages="175--209"}

This paper contains the most curious consequence of (the formalization
of) Harvey's
result: cutfree-provability in EA is EA-provably the square-root of
ordinary provability
in EA.

The preprint version can be downloaded from 
<http://www.phil.uu.nl/preprints/lgps/list.html >, preprint 40.
or: 
<http://igitur-archive.library.uu.nl/search/search.php?m=simple&p=3&qry=logic%20preprint&language=nl&sort=date  
 >

A lot of the early work could aty present be done is a more natural
way since we now have a
version of cut-elimination, due to Philipp Gerhardy, for predicate
logic which employs a complexity measure
concerning depth of quantifiers. See:

@INPROCEEDINGS(gerh:refi03,
AUTHOR    = "Gerhardy, Philipp",
TITLE     = "{R}efined {C}omplexity {A}nalysis of {C}ut {E}limination",
EDITOR    = "Baaz, Matthias and Makovsky, Johann",
BOOKTITLE = "Proceedings of the 17th International Workshop CSL 2003",
PUBLISHER = "Springer-Verlag, Berlin",
SERIES    = "LNCS",
VOLUME    = "2803",
PAGES     = "212--225",
YEAR      = 2003)

@Article{gerh:role05,
   author = "Gerhardy, Philipp",
   title =       "{The Role of Quantifier Alternations in Cut Elimination}",
   journal =     ndj,
volume = "46, no. 2",
pages = "165--171",
   year =        "2005"
}

More detail on certain lemmas of my proof of the Friedman
characterization can be found in:

@article{viss:insi92,
                 author="Visser, A.",
                 title="An Inside View of {{\sf {E}{X}{P}}}",
                   journal=jsl,
                 volume="57",
                   year=1992,
                   pages="131--165"}

To see how Harvey's work connects to the Orey-Hájek characterization,
see:

@article{viss:seco09,
                 author="Visser, A.",
                 title=" Can we make the {S}econd {I}ncompleteness {T}heorem
                              coordinate free",
  journal =      {Journal of Logic and Computation},
  year =         {2009},
  OPTkey =       {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTpages =     {},
  OPTmonth =     {},
  note = {\texttt{doi:~10.1093/logcom/exp048}}
}

-----
Albert Visser, Department of Philosophy
Heidelberglaan 8, 3584 CS Utrecht
The Netherlands
Phone 0031-30-2532173
Fax 0031-30-2532816