Herbrand uniformity theorems for infinitary languages
Bienvenido F. Nebres · Journal of the Mathematical Society of Japan · 1972
We begin by recalling several aspects of Herbrand's theorem for $L_{\omega,\omega}$ , or more precisely, of several corollaries to Herbrand's original theorem $ ([31, [6] [8], not in these references but elsewhere in the literature these corollaries are sometimes confused with the theorem itself).$L^{\vee}$ is an extension of $L$ by arbitrarily many function symbols of each number of arguments.(1) Semantic versions.(a) Reduction, for validity, to existential sentences.For every sentence $\varphi$ of $L$ there is an existential sentence $\check{\varphi}$ of $L^{\vee}$ such that $\varphi$ is valid if and only if $\check{\varphi}$ is valid.(b) Weak Uniformity theorem.A prenex existential sentence $\theta=\exists x_{1}\cdots$ $x_{m}\psi(x_{1}, \cdots , x_{m})$ is valid if and only if it is valid in all canonical (term) models; i. e., if and only if for each model $\mathfrak{A}$ of $\theta$ there are terms $t_{1}$ , $\cdot$ .. , $t_{m}$ such that $\mathfrak{A}F\psi(t_{J}, \cdots t_{m})$ .(b)i Uniformity theorem.$\theta$ is valid if and only if for some finite set $T$ of $terms_{t_{1}}\ldots.W_{{}^{t}m\in T}\psi(t_{1}, \cdots , t_{m})$ is valid.A third aspect of Herbrand's theorem will be considered in (2) (b) below.There are many possible sentences $\check{\varphi}$ which can be used for a given $\varphi$ in (1)(a).In the case that $\varphi$ is in prenex form, the validity functional form (often called the Herbrand normal form), which is dual to the Skolem form, always suffices.For example, if $\varphi=\exists y\forall z\varphi_{1}(y, z)$ with $\varphi_{1}$ quantifier-free, the validity functional form of $\varphi$ isFollowing Denton and Dreben [3], one can directly associate existential $\check{\varphi}$ with any $\varphi;\check{\varphi}$ is an Herbrand normal form of a prenex form of $\varphi$ .To illustrate (1)(a) and ( 1) $(b)^{\prime}$ , consider the sentence 1) This paper forms part of the author's Ph.D. thesis, submitted to Stanford University in May, 1970.We would like to thank our thesis adviser, Professor Solo- mon Feferman, for his advice and direction and unfailing willingness to give of his time and effort throughout our work.We also owe a special debt of thanks to Pro-