No CrossRef data available.
Published online by Cambridge University Press: 12 March 2014
One of the typical preservation theorems in a first order classical predicate logic with equality L is the following theorem due to J. Łoś [4] and A. Tarski [9] (also cf. [1, p. 139]).
Theorem A (Łoś-Tarski). For any sentences A and B in L, the following two conditions (i) and (ii) are equivalent.
(i) Every extension of any model of A is a model of B.
(ii) The two sentences A ⊃ C and C ⊃ B are provable in L for some existential sentence C in L.
In [2], S. Feferman obtained a similar preservation theorem for outer extensions. In the following, we assume that L has a fixed binary predicate symbol <. Then Σ-formulas are formulas in L which are constructed from atomic formulas and their negations by applying ∧ (conjunctions), ∨ (disjunctions), ∀x < y (bounded universal quantifications), and ∃ (existential quantifications). An extension of an L-structure is said to be an outer extension of if ⊨ a < b and b ϵ ∣∣ imply a ϵ ∣∣ for any elements a, b in ∣∣.
Theorem B (Feferman). For any sentences A and B in L, the following two conditions (i) and (ii) are equivalent.
(i) Every outer extension of any model of A is a model of B.
(ii) The two sentences A ⊃ C and C ⊃ B are provable in L for some Σ-sentence C in L.
This paper was presented at the special session on proof theory at the January 1983 Annual Meeting of the American Mathematical Society in Denver, Colorado; unfortunately its appearance in print has been delayed until now.