Remarks on Herbrand normal forms and Herbrand realizations |
| |
Authors: | Ulrich Kohlenbach |
| |
Affiliation: | 1. Fachbereich Mathematik, J.W. Goethe-Universit?t, Robert-Mayer-Strasse 6-10, W-6000, Frankfurt am Main, Federal Republic of Germany
|
| |
Abstract: | LetAH be the Herbrand normal form ofA andAH,D a Herbrand realization ofAH. We show(i) | There is an example of an (open) theory + with function parameters such that for someA not containing function parameters | (ii) | Similar for first order theories + if the index functions used in definingAH are permitted to occur in instances of non-logical axiom schemata of , i.e. for suitable ,A | (iii) | In fact, in (1) we can take for + the fragment (10-IA)+ of second order arithmetic with induction restricted to10-formulas, and in (2) we can take for the fragment (10,b-IA) of first order arithmetic with induction restricted to formulas VxA(x) whereA contains only bounded quantifiers. | (iv) | On the other hand,
|
| |