Remarks on Herbrand normal forms and Herbrand realizations

Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35)

Review text

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.

Recommendations

Cites work

Cited in

(11)

This page was built for publication: Remarks on Herbrand normal forms and Herbrand realizations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1813063)