caa a22 4500 46912685X CHVBK 20180323133153.0 cr unu---uuuuu 170328e19920901xx s 000 0 eng 10.1007/BF01627504 doi (NATIONALLICENCE)springer-10.1007/BF01627504 Kohlenbach Ulrich Fachbereich Mathematik, J.W. Goethe-Universität, Robert-Mayer-Strasse 6-10, W-6000, Frankfurt am Main, Federal Republic of Germany aut Remarks on Herbrand normal forms and Herbrand realizations [Elektronische Daten] [Ulrich Kohlenbach] Summary: LetA H be the Herbrand normal form ofA andA H,D a Herbrand realization ofA H. 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 definingA H 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 (Σ 1 0 -IA)+ of second order arithmetic with induction restricted toΣ 1 0 -formulas, and in (2) we can take for ℐ the fragment (Σ 1 0,b -IA) of first order arithmetic with induction restricted to formulas VxA(x) whereA contains only bounded quantifiers. (iv) On the other hand, $$PA^2 \vdash A^H \Rightarrow PA \vdash A,$$ wherePA 2 is the extension of first order arithmeticPA obtained by adding quantifiers for functions andA∈ℒ(PA). This generalizes to extensional arithmetic in the language of all finite types but not to sentencesA with positively occurring existential quantifiers for functions. Springer-Verlag, 1992 Archive for Mathematical Logic Springer-Verlag 31/5(1992-09-01), 305-317 0933-5846 31:5<305 1992 31 153 https://doi.org/10.1007/BF01627504 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/BF01627504 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Kohlenbach Ulrich Fachbereich Mathematik, J.W. Goethe-Universität, Robert-Mayer-Strasse 6-10, W-6000, Frankfurt am Main, Federal Republic of Germany aut NATIONALLICENCE 773 0- Archive for Mathematical Logic Springer-Verlag 31/5(1992-09-01), 305-317 0933-5846 31:5<305 1992 31 153 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer