Remarks on Herbrand normal forms and Herbrand realizations (Q1813063)

Let \(A^ H\) be the Herbrand normal form of \(A\) and \(A^{H,D}\) a Herbrand realization of \(A^ H\). We show: (i) There is an example of an (open) theory \({\mathcal T}^ +\) with function parameters such that for some \(A\) not containing function parameters (1) \({\mathcal T}^ +\vdash A^ H\), \(A^{H,D}\), \(\;{\mathcal T}^ +\not\vdash A\). (ii) Similarly for first order theories \({\mathcal T}\) if the index functions used in defining \(A^ H\) are permitted to occur in instances of non- logical axiom schemata of \({\mathcal T}\), i.e. for suitable \({\mathcal T}\), \(A\): (2) \({\mathcal T}[f_ 1,\ldots,f_ n]\vdash A^ H\), \(\;{\mathcal T}\not\vdash A\). (iii) In fact, in (1) we can take for \({\mathcal T}^ +\) the fragment \((\Sigma^ 0_ 1\text{-IA})^ +\) of second order arithmetic with induction restricted to \(\Sigma^ 0_ 1\)-formulas, and in (2) we can take for \({\mathcal T}\) the fragment \((\Sigma_ 1^{0,b}\text{-IA})\) of first order arithmetic with induction restricted to formulas \(\bigvee xA(x)\), where \(A\) contains only bounded quantifiers. (iv) On the other hand, (3) \(PA^ 2\vdash A^ H\Rightarrow PA\vdash A\), where \(PA^ 2\) is the extension of first order arithmetic \(PA\) obtained by adding quantifiers for functions and \(A\in{\mathcal L}(PA)\). This generalizes to extensional arithmetic in the language of all finite types but not to sentences \(A\) with positively occurring existential quantifiers for functions.