Saturated models of universal theories (Q1861531)

A number of conservation results have been proved proof-theoretically as well as model-theoretically. The author cites \(\text{I}\Sigma_1/\text{PRA}\), \(\text{WKL}_0/\text{PRA}\), \(\text{S}^1_2/\text{PV}\), \(\Sigma^1_1\text{-AC}_0/\text{PA}\), and \(\text{B}\Sigma_{k+1}/\text{I}\Sigma_k\). The tool on the proof-theory side is always the cut-elimination/Herbrand theorem (which W. Sieg refined and dubbed Herbrand analysis). On the other side, model-theorists use a variety of tools, like ultrapowers and cuts in nonstandard models. In this paper, the author develops a model-theoretic counterpart of Herbrand analysis and gives a unified proof of the above conservation results. The key is a Herbrand saturated model, that is, a model in which a principal \(U\)-type is realized if it is consistent with the \(U\)-diagram. (``\(U\)-\(\cdots\)'' means ``\(\cdots\) given by universal formulas'', and ``\(H\)-model'' stands for ``Herbrand saturated model'' in this review.) After showing that a consistent \(U\)-theory has an \(H\)-model, the author gives the following recipe for showing conservation. Given two theories \(T_1\) and \(T_2\) in the same language, with \(T_2\) being universal; if \(T_1\) holds in every \(H\)-model of \(T_2\), then \(T_1\) is conservative over \(T_2\) as to \(\forall\exists\)-sentences. So the author's proof of the \(\text{I}\Sigma_1/\text{PRA}\) conservation amounts to the verification of \(\Sigma_1\)-induction in an \(H\)-model of primitive recursive arithmetic. He indicates how to handle the other cases mentioned above. To recover the constructive aspect of Herbrand analysis, the author considers other proofs by forcing, and shows how they relate to realizability and the normalization of \(\lambda\)-terms.