Ah, Chu!

Solomon Feferman

Abstract

A theorem obtained by van Benthem for preservation of formulas under Chu transforms between Chu spaces is strengthened and derived from a general many-sorted interpolation theorem. The latter has been established both by proof-theoretic and model-theoretic methods; there is some discussion as to how these methods compare and what languages they apply to. In the conclusion, several further questions are raised.

Abstract

A theorem obtained by van Benthem for preservation of formulas under Chu transforms between Chu spaces is strengthened and derived from a general many-sorted interpolation theorem. The latter has been established both by proof-theoretic and model-theoretic methods; there is some discussion as to how these methods compare and what languages they apply to. In the conclusion, several further questions are raised.

Dear Johan,

Here, for the record, are some results and ideas that came out of your stimulating presentation to our logic seminar at Stanford last May, “Information transfer across Chu spaces” [B]. Let me begin by recalling some definitions from your notes and your results concerning them. A Chu space is any structure (A, X, R) with two basic (non-empty) domains A and X and a relation R ⊆ A×X. The paradigm example is given by A = a set of objects, X = a collection of subsets of A and R = the ∈ relation. A Chu transform between two Chu spaces (A, X, R) and (B, Y, S) is a pair of functions f, g with f : A → B and g : Y → X such that for all a ∈ A and y ∈ Y, we have

R(a, g(y) ) ⇔ S(f(a), y).

Formulas in the first-order language, with equality, of Chu spaces^{1} are built up with two sorts of variables, a, a_{1}, a_{2}, … and x, x_{1}, x_{2}, … that I shall call a-variables (or of sort s_{a}) and x-variables (or of sort s_{x}), respectively. Atomic formulas are of the form R(a, x), together with equations between a-variables and equations between x-variables. Formulas are built from atomic formulas by ¬, ∧, ∨, and the quantifiers ∀ and ∃ applied to either sort of variable. A flow formula is one that is built up from atomic formulas and their negations by ∧, ∨, and quantifications of the form ∃a and ∀x. Using other terminology, up to equivalence these are essentially existential in the a-variables and essentially universal in the x-variables. Next one defines: φ(a, x) implies ψ(a, x) along Chu transforms if whenever M = (A, X, R) and N = (B, Y, S) are Chu spaces and (f, g) is a Chu transform between M and N then

1In your notes, equality was not necessarily included; this turned out to lead to a methodological issue that will come up below.

M ⊧ φ(a, g(y) ) ⇒ N ⊧ ψ(f(a), y).

If this holds when φ = ψ then φ is said to be Chu-preserved. Your main results were as follows:

Theorem 1 The following are equivalent:

(i) φ implies ψ along Chu transforms

(ii) there exists a flow formula θ such that both φ → θ and θ → ψ are valid.

Corollary 1 φ is preserved under Chu transforms iff φ is equivalent to a flow formula.

As you showed, the implication (ii) ⇒ (i) in Theorem 1 is straightforward; it is only the proof of the forward implication that takes some work. Your proof of that part was by a model-theoretic argument, using (recursively) saturated models. The result reminded me of the kind of thing I had done in the past via a general many-sorted interpolation theorem established by proof-theoretic arguments ([F1]), and so I looked to see if those could provide an alternative approach. Indeed they could; I sketched the idea in the seminar, and here are more details. The first thing that struck me in thinking about the Corollary was that flow formulas behave on the a-variables like formulas preserved under passage to extensions, while they behave on the x-variables like formulas preserved under passage to substructures. That led me to look at the following very special case of Chu transforms. Two Chu spaces M = (A, X, R) and N = (B, Y, S) are said to be simply Chu related if A ⊆ B and Y ⊆ X and for all a ∈ A and y ∈ Y, we have

R(a, y) ⇔ S(a, y).

When this holds, we have a Chu transform (f, g) where f(a) = a for a ∈ A and g(y) = y for y ∈ Y. We say that φ(a, x) implies ψ(a, x) along simple Chu transforms if whenever M and N are simply Chu related and a ∈ A and y ∈ Y and M ⊧ φ(a, y) then N ⊧ ψ(a, y). If φ implies ψ along Chu transforms then φ implies ψ along simple Chu transforms. Thus for your result (i) ⇒ (ii) in Theorem 1, it is sufficient to establish the following:

Theorem 2 Suppose φ implies ψ along simple Chu transforms. Then there exists a flow formula θ such that both φ → θ and θ → ψ are valid.

My proof of Theorem 2 makes use of a many-sorted interpolation theorem of the kind that I established in [F1], in a more general form found later by Jacques Stern [S]. To state this, let me repeat some syntactic definitions from [F1], p. 55. Let L^{∗} be a relational many-sorted language with equality, let Sort be its set of sort symbols, and assume given a partition Sort_{0} and Sort_{1} of Sort, each part of which is non-empty. (In the application to be made, L^{∗} will be an extension of L.) For the application below it will be essential that we allow equality to be between variables of any sort; relations otherwise have a specific arity specifying the sort of each argument place.

Definition 1 For φ a formula of L^{∗}, and for i = 0, 1:

(i) Rel(φ) is the set of relation symbols in φ, together with the equality symbol. (ii) Free(φ) is the set of free variables of φ. (iii) Sort_{i} is the set of sorts s ∈ Sort_{i} such that some variable of sort s occurs

free or bound in φ. (iv) Un_{i}(φ) is the set of s ∈ Sort_{i} such that there is at least one essentially

universal occurrence in φ of some variable of sort s.

(v) Ex_{i}(φ) is the set of s ∈ Sort_{i} such that there is at least one essentially universal occurrence in φ of some variable u of sort s.

As usual, by an interpolant for φ → ψ we mean a formula θ such that φ → θ and θ → ψ are both valid.

Theorem 3 Suppose φ and ψ are formulas of L^{∗} and that φ → ψ is valid and is such that Sort_{i}(φ) ∩ Sort_{i}(ψ) ≠ ∅ for i = 0, 1. Then there is an interpolant θ for φ → ψ in L^{∗}, such that:

(i) Rel(θ) ⊆ Rel(φ)∩ Rel(ψ) (ii) Sort(θ) ⊆ Sort(φ)∩ Sort(ψ) (iii) F ree_{0}(θ) ⊆Free_{0}(φ)∩Free_{0}(ψ) (iv) Un_{0}(θ) ⊆ Un_{0}(φ) and Ex_{0}(θ) ⊆ Ex_{0}(ψ)

(v) Ex_{1}(θ) ⊆ Ex_{1}(φ) and Un_{1}(θ) ⊆ Un_{1}(ψ).

Remarks concerning statement and proofs of Theorem 3. For the case that Sort_{1} = ∅ this follows from Theorem 4.3 of [F1], p. 56, where it was established by a proof-theoretical argument. The theorem in full follows from Theorem 2-1 of Stern [S], p. 4, where it was established by a model-theoretic forcing argument.^{2} (His statement also includes conditions on positive and negative occurrences of relation symbols, as in Lyndon’s well-known interpolation theorem; I have omitted these here for simplicity since they are not needed for the application to preservation under Chu transforms.) The theorem in full may also be proved following the same lines as that for Theorem 4.3 of [F1]. The point there is that in building up an interpolant following a cut-free derivation of φ → ψ, we are forced to introduce quantifiers into the interpolant only as required to maintain the condition (iii), and that turns out to lead to (iv). Since no condition is imposed on free variables of Sort_{1}, we are forced to introduce quantifiers applied to those variables into the interpolant only as required in (v). In July 1998, our visitor Martin Otto obtained an alternative formulation [O] using relativized quantifiers in a single-sorted language in place of many-sorted languages; his proof is model-theoretic using back-and-forth systems.

2When I presented Theorem 3 in the seminar, I had not remembered that Stern had already obtained it in full generality; I only realized this when looking up his paper in preparation for writing up this note. For comparison with his formulation, my Sort_{0} is Stern’s I^{∧} and my Sort_{1} is his I^{∨}; in place of additional constant symbols, I place conditions only on free variables in (iii). To state the theorem in the generality given by Stern, we have to allow Sort_{0} or Sort_{1} to be empty, and then there are some additional conditions on free variables that need to be specified. For simplicity here, I have assumed that both of these sets of sorts is non-empty since that will be the case in our application.

Proof of Theorem 2. By a combined simple Chu structure we mean a structure

M^{∗} = (A, X, A′, X′; R, R′)

with four basic domains, such that

A ⊆ A′, X′ ⊆ X, R ⊆ A × X, R′ ⊆ A′ × X′,

and such that

∀a ∈ A∀x′ ∈ X′[R(a, x′) ↔ R′(a, x′) ].

Let L^{∗} be the four-sorted language for such structures. It has variables a, a_{1}, a_{2}, … of sort s_{a}, variables x, x_{1}, x_{2}, … of sort s_{x}, variables a′, a′_{1}, a′_{2}, … of sort s_{a′}, and, finally, variables x′, x′_{1}, x′_{2}, … of sort s_{x′}. It has two relation symbols R and R′, both of argument sort (s_{a}, s_{x′}), equality relations in each sort and also mixed equality relations of the form a = a′ and x = x′ (or their converses). If χ is a formula of our original language L, by χ′ we mean the same formula with every variable replaced by the corresponding primed variable.

Now φ(a, x) implies ψ(a, x) along simple Chu transforms if and only if every combined simple Chu structure M^{∗} satisfies

M^{∗} ⊧ ∀a∀x′[φ(a, x′) → ψ′(a, x′) ].

By the completeness theorem, that is equivalent to

⊢ σ ∧ ∃a[a′ = a ∧ φ(a, x′) ] → ψ′(a′, x′),  (1)

where

σ = ∀a∃a′[a = a′] ∧ ∀x′∃x[x = x′] ∧ ∀a∀x′[R(a, x′) ↔ R′(a, x′) ].

We are now in a position to apply Theorem 3. Let Sort_{0} = {s_{a}, s_{x}, s_{a′}} and Sort_{1} = {s_{x′}}. By Theorem 3, we can find an interpolant whose sorts are included in the common sorts of the l.h.s and the r.h.s. of the implication in (1); but these are just the prime sorts. Also the free variables in the interpolant of Sort_{0} are included in the common free variables of the l.h.s. and the r.h.s., so this is just the variable a′. On the other hand, there is no restriction on the variables of Sort_{1} in the interpolant, so we take these to be a finite list x′, x′_{1}, …. Thus the interpolant is of the form θ′(a′, x′, x′_{1}, …), which we simply denote by θ′. Now by parts (iv) and (v) of Theorem 3, we have:

Un_{0}(θ′) ⊆ Un_{0}(σ ∧ ∃a[a′ = a ∧ φ(a, x′) ] ) and
Ex_{1}(θ′) ⊆ Ex_{1}(σ ∧ ∃a[a′ = a ∧ φ(a, x′) ] ).

Notice that the only variables of Sort_{0} that could occur in θ′ are of sort s_{a′}; since no such variables occur universally in σ or φ it follows that Un_{0}(θ′) = ∅. By a similar argument we see that Ex_{1}(θ′) = ∅. Hence θ′ has all bound variables of sort s_{a′} in essentially existential position, and all those of sort s_{x′} in essentially universal position. To conclude, from

⊢ σ∧∃a[a′ = a∧φ(a, x′) ] → θ′(a′, x′, x′_{1}, …) and ⊢ θ′(a′, x′, x′_{1}, …) → ψ′(a′, x′),

we have that both implications are valid in all combined simple Chu structures M^{∗} for which A = A′, X = X′, and R = R′, or what comes to the same thing, that

⊢ φ(a, x) → θ(a, x, x_{1}, …) and ⊢ θ(a, x, x_{1}, …) → ψ(a, x).

Moreover, θ is a flow formula by the preceding argument, so by universally quantifying out the additional variables ∀x_{1}, …, we obtain an interpolating flow formula between φ and ψ; Theorem 2 is thus proved.

Remarks.

1. This argument makes essential use of equality relations, which your original argument did not need (though yours works as well if equality is included). Also, as remarked above, Otto’s reformulation [O] of the interpolation theorem dispenses with sorted variables in favor of variables restricted to unary predicates, and so the inclusion relations A ⊆ A′, X′ ⊆ X can be expressed in such a language without use of equality relations. I have not looked to see whether Otto’s reformulation can be given a proof-theoretical proof as well.

2. In your notes [B] you stated that your main theorem holds also in L_{∞,ω}. My result also extends to infinitary languages but only to countable admissible L_{A}, in order to make use of completeness (see [F1]).

Further questions. In our personal discussion of these results, some further areas to explore were suggested. Here they are, from my notes, again for the record.

1. Is there an appropriate notion of Chu^{p} which is related to partial isomorphism between such structures, as Chu is related to isomorphism? [I’m not sure if this question makes sense as stated, but that’s what it shows in my notes.]

2. How would putting additional structure in the A-part of Chu structures affect the preservation results? Your motivation for interest in this question had to do with general frames in modal logic.

3. Is there an interest in pursuing k-valued Chu spaces?

4. There are a number of questions regarding operations on Chu spaces. First of all, which operations preserve elementary equivalence between such structures? In [B] you gave one such result, concerning an operation M ⊕ N, and raised the question whether Vaughan Pratt’s operation M ⊗ N also preserves elementary equivalence. For operations which preserve equivalence in L_{ω,ω} one may be able to apply the work of Vaught and myself on generalized products of structures [F,V]. I also suggested looking back at [F2] for methods and results concerning functors which preserve elementary equivalence in certain infinitary languages (including uncountable ones).

So: Many happy returns of the day, and ... Gesundheit!

References

[B] Johan van Benthem, Information transfer across Chu spaces (Lecture notes for the Logic Seminar, Stanford, May 1998.)

[F1] Solomon Feferman, Lectures on proof theory, Lecture Notes in Mathematics 70 (1968), 1-107.

[F2] Solomon Feferman, Infinitary properties, local functors, and systems of ordinal functions, Conference in Mathematical Logic—London, 70, Lecture Notes in Mathematics 255 (1972), 63-97.

[F,V] Solomon Feferman and Robert L. Vaught, The first-order properties of products of algebraic systems, Fundamenta Mathematicae 47 (1959), 57-103.

[O] Martin Otto, Sketch concerning a variation on Lyndon’s interpolation theorem. (Unpublished notes, Stanford, July 1998.)

[S] Jacques Stern, A new look at the interpolation problem, J. Symbolic Logic 40 (1975), 1-13.

Dept. of Mathematics Stanford University

Stanford CA 94305, USA EM: sf@csli.stanford.edu