An axiomatization theorem
Nobuyoshi Motoháshi · Journal of the Mathematical Society of Japan · 1982
Let $L$ be a first order finitary predicate logic with equality $L_{\omega,\omega}$ , or a first order infinitary predicate logic with equality $L_{\omega_{1},\omega}$ , and $I,$ $J,$ $K$ three sets of formulas in $L$ .Then, $I$ and $J$ are said to be equivalent inAlso, $I$ is said to be an axiomatization of $J$ in $L$ , if $I$ is a subset of $J$ and, $I$ and $J$ are equivalent in $L$ over $J$ .An axiomatization theorem of $J$ in $L$ is a statement to give us a " concrete " method to construct a " simple " axiomati- zation of $J$ in $L$ .Of course, " concrete " and " simple " have no precise mathe- matical meanings and we use them rather informally.But, two remarks on them will be given in the following.First, if $L=L_{\omega,\omega}$ and $J$ is a recursively enumerable set of formulas in $L$ under a nice G\"odel-numbering, then there is a method to construct a primitive recursive axiomatization of $J$ in $L$ by the well- known theorem due to W. Craig (cf.Craig [2]).But the axiomatization of $J$ obtained by Craig's method seems to be so complicated that, in practice, one can not easily tell whether or not a given formula belongs to it, generally (cf.p. 141 in Keisler [4]).This shows us that it is meaningful to give a concrete method to construct a simple axiomatization of $J$ , even if $J$ is recursively enumerable.Secondly, the set $J$ is usually defined using some parameters $p_{1},$ $p_{2},$ $\cdots$ , $p_{n}$ .So, in order to give an axiomatization theorem of $J$ in $L$ , we should clearly state how to construct an axiomatization of $J$ from each values of parameters $p_{1},$ $p_{2},$ $\cdots$ , $p_{n}$ , concretely.To define sets of formulas which we are going to deal with, and to state their axiomatization theorem, we require some definitions.Suppose that $W$ is a set of predicate symbols.Then, W-free (W-positive, W-negative) formulas are formulas which have no (no negative, no positive) occurrences of predicate symbols in $W$ .W-atomic formulas are formulas of the form $P(\overline{t})$ for some $P\in W$ and some sequence $\overline{t}$ of terms.A formula $A$ is said to belong to a formula $B$ syntactically, if every predicate symbol occurring in $A$ positively (negatively) occurs in $B$ positively (negatively).For each sentence $A$ in $L$ , and each two sets $S,$ $Q$ of predicate symbols in $L$ , let