BRICS RS-97-3 Butz & Moerdijk: A Definability Theorem for First Order Logic BRICS

Basic Research in Computer Science

A Definability Theorem for First Order Logic

Carsten Butz Ieke Moerdijk BRICS Report Series RS-97-3 ISSN 0909-0878 March 1997 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/97/3/

A Definability Theorem for First Order Logic

Carsten Butz (Århus) and Ieke Moerdijk (Utrecht)^{∗}

In this paper, we will present a definability theorem for first order logic. This theorem is very easy to state, and its proof only uses elementary tools. To explain the theorem, let us first observe that if M is a model of a theory T in a language L, then, clearly, any definable subset S ⊂ M (i.e., a subset S = {a | M ⊧ φ(a)} defined by some formula φ) is invariant under all automorphisms of M . The same is of course true for subsets of M^{n} defined by formulas with n free variables.

Our theorem states that, if one allows Boolean valued models, the converse holds. More precisely, for any theory T we will construct a Boolean valued model M , in which precisely the T –provable formulas hold, and in which every (Boolean valued) subset which is invariant under all automorphisms of M is definable by a formula of L.

Our presentation is entirely selfcontained, and only requires familiarity with the most elementary properties of model theory. In particular, we have added a first section in which we review the basic definitions concerning Boolean valued models.

The Boolean algebra used in the construction of the model will be presented concretely as the algebra of closed and open subsets of a topological space X naturally associated with the theory T . The construction of this space is closely related to the one in [1]. In fact, one of the results in that paper could be interpreted as a definability theorem for infinitary logic, using topological rather than Boolean valued models.

1 Preliminary definitions

In this section we review the basic definitions concerning Boolean valued models (see e.g. [2]). Most readers will be familiar with these notions, and they are advised to skip this section. They should note, however, that our Boolean algebras are not necessarily complete, and that we treat constants and function symbols as functional relations.

∗Both authors acknowledge support from the Netherlands Science Organisation (NWO).

Let us fix a signature S, consisting of constants, function and relation symbols. For simplicity we assume it is a single sorted signature, although this restriction is by no means essential. Let L denote the associated first order language L_{ωω}(S).

A Boolean valued interpretation of L is a triple 𝔐 = (B, |𝔐|, [[−]]), where B is a Boolean algebra, |𝔐| is the underlying set of the interpretation, and [[−]] is an operation which assigns to each formula φ(x_{1}, …, x_{n}) of L with free variables among x_{1}, …, x_{n} a function |𝔐|^{n} → B, whose value at (m_{1}, …, m_{n}) is denoted

[[φ(m_{1}, …, m_{n})]].

These functions are required to satisfy the usual identities (where we write m for m_{1}, …, m_{n}):

(i) [[φ ∧ ψ(m)]] = [[φ(m)]] ∧ [[ψ(m)]] and similar for the other Boolean connectives.

(ii) [[∃yφ(y, m)]] = ⋁{[[φ(k, m)]] | k ∈ |𝔐|},

[[∀yφ(y, m)]] = ⋀{[[φ(k, m)]] | k ∈ |𝔐|},

where it is part of the definition of an interpretation that these sups and infs are required to exists in B. Finally, we require

(iii) if ⊢ φ(x_{1}, …, x_{n}) then [[φ(m)]] = 1_{B} for any m ∈ |𝔐|^{n}.

In (iii), ⊢ denotes derivability in (one of the usual axiomatisations of) classical first order logic.

Remark 1.1 (i) Note that, in particular, |𝔐| is equipped with a B–valued equality [[x_{1} = x_{2}]]: |𝔐|^{2} → B, satisfying the identities for reflexivity, transitivity and symmetry,

[[m = m]] = 1_{B},
[[m_{1} = m_{2}]] = [[m_{2} = m_{1}]],
[[m_{1} = m_{2}]] ∧ [[m_{2} = m_{3}]] ≤ [[m_{1} = m_{3}]].

(ii) For each constant c the formulas c = x and x = c define the same function C = [[c = x]]: |𝔐|^{2} → B, which should be viewed as the interpretation of c. It satisfies the conditions C(m) ∧ [[m = m′]] ≤ C(m′) and ⋁{C(m) | m ∈ |𝔐|} = 1_{B}. Similarly, each n–ary function symbol is interpreted, via the formula f(x_{1}, …, x_{n}) = y, by a function F: |𝔐|^{n} × |𝔐| → B. This function satisfies the conditions F (m, k) ∧ [[m = m′]] ∧ [[k = k′]] ≤ F (m′, k′) and ⋁{F (m, k) | k ∈ |𝔐|} = 1_{B}. (Here m = m_{1}, …, m_{n} as before, and [[m = m′]] stands for ⋀_{i=1}^{n}[[m_{i} = m′_{i}]].)

(iii) For each n–ary relation symbol r the formula r(x_{1}, …, x_{n}) defines a map R: |𝔐|^{n} → B, which is extensional in the sense that R(m) ∧ [[m = m′]] ≤ R(m′).

(iv) The entire interpretation is determined by these data in (i)–(iii). First, using derivability of usual equivalences such as ⊢ f(g(x)) = y ↔ ∃z(f(z) = y ∧g(x) = z), one obtains by induction for each term t(x_{1}, …, x_{n}) a function T: |𝔐|^{n+1} → B interpreting the formula t(x_{1}, …, x_{n}) = y. Next, one builds up the interpretation of formulas in the usual way, using the assumption that all necessary sups and infs exist in B.

As usual, we write 𝔐 ⊧ φ if [[φ(m)]] = 1 for all m ∈ |𝔐|^{n}, and we say 𝔐 is a model of a theory T if 𝔐 ⊧ φ whenever T ⊢ φ. In this case, we write 𝔐 ⊧ T , as usual.

2 Automorphisms of models and statement of the theorem

Consider a fixed Boolean valued model 𝔐 = (B, |𝔐|, [[−]]). An automorphism π of 𝔐 consists of two mappings π_{0} and π_{1}. The map π_{0} : B → B is an automorphism of the Boolean algebra B, while π_{1} : |𝔐| → |𝔐| is an automorphism of the underlying set |𝔐|, with the property that

π_{0}[[φ(m_{1}, …, m_{n})]] = [[φ(π_{1}(m_{1}), …, π_{1}(m_{n}))]],  (1)

for any formula φ(x_{1}, …, x_{n}) and any m_{1}, …, m_{n} ∈ |𝔐|. (Of course it is enough to check a condition like (1) for constants, functions and relations of L, and deduce (1) for arbitrary φ by induction.)

An (n–ary) predicate on 𝔐 is a map p: |𝔐|^{n} → B which satisfies the extensionality condition

p(m) ∧ [[m = m′]] ≤ p(m′)  (2)

for any m, m′ ∈ |𝔐|^{n} (where [[m = m′]] stands for ⋀_{i=1}^{n}[[m_{i} = m′_{i}]], as before). Such a predicate p is definable if there is a formula φ(x_{1}, …, x_{n}) such that

p(m) = [[φ(m)]],  for all m ∈ |𝔐|^{n}.  (3)

It is invariant under an automorphism π if

π_{0}p(m) = p(π_{1}(m)),  for all m ∈ |𝔐|^{n},  (4)

(where π_{1}(m) is (π_{1}(m_{1}), …, π_{1}(m_{n}))). Obviously, every definable predicate is invariant. Our theorem states the converse.

Theorem 2.1 Let T be any first order theory. There exists an Boolean valued model 𝔐 such that

(i) 𝔐 is a conservative model of T , in the sense that 𝔐 ⊧ φ iff T ⊢ φ, for any sentence φ.

(ii) Any predicate which is invariant under all automorphisms of 𝔐 is definable.

Before proving the theorem in §4, we will first give an explicit description of the Boolean algebra and the interpretation involved in the next section.

3 Construction of the model

Our Boolean algebra will be defined as the algebra of all clopen (i.e., closed and open) sets in a topological space X. To describe X, let κ ≥ ω be the cardinality of our language L. We fix a set S_{T} of (ordinary, two–valued) models M of T such that every model of cardinality ≤ κ is isomorphic to a model in S_{T}. Then, in particular, a formula is provable from T iff it holds in all models in the set S_{T}.

Definition 3.1 An enumeration of a model M is a function α: κ → |M | such that α^{−1}(a) is infinite for all a ∈ |M | (here |M | is the underlying set of M ).

The space X has as its points the equivalence classes of pairs (M , α), where M ∈ S_{T} and α is an enumeration of M . Two such pairs (M , α) and (N, β) are equivalent if there exists an isomorphism of models θ: M →^{≃} N such that β = θ ∘ α. We will often simply write (M , α) when we mean the equivalence class of (M , α). The topology of X is generated by all the basic open sets of the form

U_{φ,ξ} = {(M , α) | M ⊧ φ(α(ξ))}.  (5)

Here φ = φ(x_{1}, …, x_{n}) is any formula with free variables among x_{1}, …, x_{n}, while ξ = (ξ_{1}, …, ξ_{n}) is a sequence of elements of κ (i.e., ordinals ξ_{i} < κ); we use α(ξ) as an abbreviation of α(ξ_{1}), …, α(ξ_{n}).

Observe that each such basic open set U_{φ,ξ} is also closed, with complement U_{¬φ,ξ}. So X is a zero–dimensional space. We now define the Boolean algebra B as

B = Clopens(X),  (6)

the algebra of all open and closed sets in X.

Notice that arbitrary suprema need not exist in B, although B has many infinite suprema. In particular, if U ⊂ X is clopen and {U_{i}}_{i∈I} is a cover of U by basic open sets, then the union ⋃_{i∈I} U_{i} defines a supremum U = ⋁_{i∈I} U_{i} in B; we only need suprema of this kind.

The Boolean algebra B just constructed is part of a natural Boolean valued model 𝔐 = (B, |𝔐|, [[−]]), with

|𝔐| = κ  (7)

and evaluation of formulas defined by

[[φ(ξ_{1}, …, ξ_{n})]] = U_{φ,ξ},  (8)

for any formula φ(x_{1}, …, x_{n}) and any sequence ξ = ξ_{1}, …, ξ_{n} of ordinals ξ_{i} < κ.

Lemma 3.2 This evaluation defines a B–valued interpretation of the language L.

Proof. One needs to check the requirements (i)–(iii) from Section 1. Now (iii) is clear, while (i) and (ii) are completely straightforward. For illustration, we give the case of the existential quantifier. Suppose φ(y, x) is a formula with just two free variables x and y. Then for any ξ < κ,

[[∃yφ(y, ξ)]] = {(M , α) | M ⊧ ∃yφ(y, α(ξ))}
= {(M , α) | ∃η < κ: M ⊧ φ(α(η), α(ξ))}

(since each α is surjective)

= ⋃_{η<κ}{(M , α) | M ⊧ φ(α(η), α(ξ))}
= ⋃_{η<κ}[[φ(η, ξ)]],

and this union is a supremum in B, by the remark above. □

4 Proof of the theorem

We will now show that the interpretation 𝔐 has the two properties stated in Theorem 2.1. The first one is easy:

Proposition 4.1 𝔐 is a conservative model of T .

Proof. We need to show that 𝔐 ⊧ σ iff T ⊢ σ, for any sentence σ ∈ L. By Lemma 3.2, [[σ]] = {(M , α) | M ⊧ σ}. Thus [[σ]] = X iff M ⊧ σ for all M ∈ S_{T}, and this holds iff T ⊢ σ, by definition of S_{T}. □

For the proof of the definability result 2.1(ii), we shall only need a particular collection of automorphisms of the model 𝔐. Let S_{κ} denote the symmetric group of permutations of κ. Then S_{κ} acts on the model 𝔐 as follows. Any π_{1} ∈ S_{κ} induces a homeomorphism π_{0} : X → X, defined by

π_{0}(M , α) = (M , α ∘ π_{1}^{−1}).

This map has the property that π_{0}(U_{φ,ξ}) = U_{φ,π_{1}(ξ)}, or

π_{0}[[φ(ξ)]] = [[φ(π_{1}(ξ))]],

for any formula φ(x_{1}, …, x_{n}) and any ξ = ξ_{1}, …, ξ_{n} < κ. Thus, the pair π = (π_{1}, π_{0}) is an automorphism of 𝔐. This defines an action of S_{κ} on 𝔐, i.e., a representation

ρ: S_{κ} → Aut(𝔐), ρ(π_{1}) = π.

For the second part of Theorem 2.1, it will now be enough to show:

Proposition 4.2 Any S_{κ}–invariant predicate is definable.

To simplify notation, we will only prove this for a unary predicate. So let us fix such an invariant predicate p. It is a function p: |𝔐| = κ ⟶ B satisfying the extensionality condition

p(ξ) ∧ [[ξ = ξ′]] ≤ p(ξ′),

as well as the invariance condition

p(π_{1}ξ) = π_{0}(p(ξ)),

for any π_{1} ∈ S_{κ}. We will first show that p is “locally” definable (Lemma 4.5).

Lemma 4.3 Let (M , α) ∈ U ∈ B and η_{0} ∈ κ. Then there is a formula δ(x_{1}, …, x_{n}, y) and elements ξ_{1}, …, ξ_{n} ∈ κ such that

(i) (M , α) ∈ U_{δ,(ξ,η_{0})} ≤ U.

(ii) For any point (N, β) in X, any b_{1}, …, b_{n}, c ∈ |N| such that N ⊧ δ(b_{1}, …, b_{n}, c), and any η ∈ κ with β(η) = c, there exists a π_{1} ∈ S_{κ} such that π_{1}(η) = η_{0} and π_{0}(N, β) ∈ U_{δ,(ξ,η_{0})}.

Proof. Choose a basic open set U_{δ′,ξ}, given by a formula δ′(x_{1}, …, x_{n}) and ξ_{1}, …, ξ_{n} < κ, such that

(M , α) ∈ U_{δ′,ξ} ⊂ U.

Let Eq_{α}(x_{1}, …, x_{n}, y) be the formula

⋀_{α(ξ_{i})=α(ξ_{j})} x_{i} = x_{j} ∧ ⋀_{α(ξ_{i})=α(η_{0})} x_{i} = y,

and define δ to be δ′ ∧ Eq_{α}. Then obviously

(M , α) ∈ U_{δ,ξ,η_{0}} ⊂ U_{δ′,ξ} ⊂ U.

Now choose any (N, β), b_{1}, …, b_{n}, c and η satisfying the hypothesis of part (ii) of the lemma. Then in particular N ⊧ Eq_{α}(b_{1}, …, b_{n}, c) and c = β(η). Since β: κ → |N| has infinite fibres, we can find ζ_{1}, …, ζ_{n} < κ such that β(ζ_{i}) = b_{i}, while the sequence ζ_{1}, …, ζ_{n}, η satisfies exactly the same equalities and inequalities as the sequence ξ_{1}, …, ξ_{n}, η_{0}. [Indeed, if ζ_{1}, …, ζ_{i} have been found, and ξ_{i+1} = ξ_{k} for some k ≤ i or ξ_{i+1} = η_{0}, then also α(ξ_{i+1}) = α(ξ_{k}) or α(ξ_{i+1}) = α(η_{0}), hence b_{i+1} = b_{k} or b_{i+1} = c since N ⊧ Eq_{α}(b_{1}, …, b_{n}, c). Thus, we can choose ζ_{i+1} = ζ_{k} respectively ζ_{i+1} = η. If, on the other hand, ξ_{i+1} ∉ {η_{0}, ξ_{1}, …, ξ_{i}}, we can use the fact that β^{−1}(b_{i+1}) is infinite, to find ζ_{i+1} ∈ β^{−1}(b_{i+1}) \ {η, ζ_{1}, …, ζ_{i}}.] Thus, there is a permutation π_{1} ∈ S_{κ} with

π_{1}(η) = η_{0}, π_{1}(ζ_{1}) = ξ_{1}, …, π_{1}(ζ_{n}) = ξ_{n}.

But then N ⊧ δ(b_{1}, …, b_{n}, c) means that N ⊧ δ(π_{1}^{−1}(ξ_{1}), …, π_{1}^{−1}(ξ_{n}), π_{1}^{−1}(η_{0})), or that π_{0}(N, β) ∈ U_{δ,(ξ,η_{0})}. □

Lemma 4.4 Let η_{0} < κ. There is a cover p(η_{0}) = ⋁_{i∈I(η_{0})} U_{i} in B, and formulas ψ_{i}^{η_{0}}(y), such that for any i ∈ I(η_{0}),

(i) U_{i} ≤ [[ψ_{i}^{η_{0}}(η_{0})]].

(ii) For any η < κ, [[ψ_{i}^{η_{0}}(η)]] ≤ p(η).

(iii) ⋁_{i∈I(η_{0})}[[ψ_{i}^{η_{0}}(η_{0})]] = p(η_{0}).

Proof. Observe that (iii) follows from (i) and (ii). To prove these, write U = p(η_{0}), and apply Lemma 4.3 to each of the points (M , α) ∈ U. This will give a cover U = ⋃_{i∈I} U_{i} by basic open sets, and for each index i a formula δ_{i}(x_{1}, …, x_{n}, y) and elements ξ_{1}, …, ξ_{n} < κ such that

U_{i} = U_{δ_{i},(ξ,η_{0})},

and moreover such that property (ii) of Lemma 4.3 holds for each of these formulas δ_{i}. Now define

ψ_{i}^{η_{0}}(y) = ∃x_{1} … ∃x_{n}δ_{i}(x_{1}, …, x_{n}, y).

It is now clear that statement (i) in the lemma holds. For (ii), suppose (N, β) ∈ [[ψ_{i}^{η_{0}}(η)]]. This means that N ⊧ ∃x_{1} … ∃x_{n}δ_{i}(x_{1}, …, x_{n}, y). By 4.3(ii), we can find a π_{1} ∈ S_{κ} such that π_{1}(η) = η_{0} and π_{0}(N, β) ∈ U_{δ_{i},(ξ,η_{0})} = U_{i}. Since U_{i} ⊂ U = p(η_{0}), also π_{0}(N, β) ∈ p(η_{0}), and hence, by invariance of p, (N, β) ∈ p(π_{1}^{−1}(η_{0})) = p(η), as required. □

Lemma 4.5 There is a family {ψ_{i}(y) | i ∈ I} of formulas such that, for all η < κ,

p(η) = ⋁_{i∈I}[[ψ_{i}(η)]].

Proof. This follows immediately from the previous lemma, for the collection of formulas {ψ_{i}^{η_{0}} | η_{0} < κ, i ∈ I(η_{0})}. □

Proof of Proposition 4.2. Consider the function p′: |𝔐| → B defined by p′(η) = ¬p(η). Clearly, since p is a predicate, so is p′, i.e., p′(η) ∧ [[η = η′]] ≤ p′(η′) for all η, η′ < κ. Moreover, p′ is invariant since p is. So we can apply Lemma 4.5 to p′, to find a collection of formulas

{φ_{j}(y) | j ∈ J}

such that for all η < κ,

p′(η) = ⋁_{j∈J}[[φ_{j}(η)]].  (9)

The definability of p now follows by a standard compactness argument. Let c be a “new” constant, and consider the theory T′ = T ∪ {¬ψ_{i}(c) | i ∈ I} ∪ {¬φ_{j}(c) | j ∈ J}. If T′ where consistent, it would have a model M , which we can assume to be (an expansion of a model) in the set S_{T}. Let α be an enumeration of M , and choose η < κ with α(η) = c^{(M )}, the interpretation of c in M . Then (M , α) ∈ X = p(η) ∨ p′(η), hence (M , α) ∈ [[ψ_{i}(η)]] for some i ∈ I or (M , α) ∈ [[φ_{j}(η)]] for some j ∈ J.. This means that M ⊧ φ_{i}(α(η)) ∨ ψ_{j}(α(η)), contradicting the fact that M models T′. This proves that T′ is inconsistent.

Now apply compactness, to find i_{1}, …, i_{n} ∈ I and j_{1}, …, j_{m} ∈ J such that

T ⊢ ∀y(ψ_{i_{1}}(y) ∨ ⋯ ∨ ψ_{i_{n}}(y) ∨ φ_{j_{1}}(y) ∨ ⋯ ∨ φ_{j_{m}}(y)).  (10)

Write ψ = ψ_{i_{1}} ∨ ⋯ ∨ ψ_{i_{n}} and φ = φ_{j_{1}} ∨ ⋯ ∨ φ_{j_{m}}. We claim that ψ defines p. Indeed, let (M , α) be any point in X, and let η < κ. By (10), M ⊧ ψ(α(η))∨ φ(α(η)), or in other words, either (M , α) ∈ [[ψ(η)]] or (M , α) ∈ [[φ(η)]]. If (M , α) ∈ [[ψ(η)]], then (M , α) ∈ p(η) by Lemma 4.2. And if (M , α) ∈ [[φ(η)]], then (M , α) ∈ p′(η) by (9), hence (M , α) ∉ p(η). Thus (M , α) ∈ [[ψ(η)]] iff (M , α) ∈ p(η).

This show that [[ψ(η)]] = p(η) for any η < κ, and completes the proof. □

References

[1] C. Butz and I. Moerdijk. Representing topoi by topological groupoids. Utrecht preprint nr. 984, October 1996. To appear in J. Pure and Applied Alg.

[2] S. Koppelberg. Booleschewertige Logik. Jber. d. dt. Math.-Verein 87 (1985), 19–38.

Ieke Moerdijk, Mathematisch Instituut, Universiteit Utrecht, Postbus 80.010, NL–3508 TA Utrecht, The Netherlands, moerdijk@math.ruu.nl. Carsten Butz, BRICS, Department of Computer Science, University of Aarhus, Ny Munkegade, Building 540, DK-8000 Århus C, Denmark, butz@brics.dk. BRICS Basic Research in Computer Science, Centre of the Danish National Research Foundation.

Recent BRICS Report Series Publications

RS-97-3 Carsten Butz and Ieke Moerdijk. A Definability Theorem for First Order Logic. March 1997. 10 pp.

RS-97-2 David A. Schmidt. Abstract Interpretation in the Operational Semantics Hierarchy. March 1997. 33 pp.

RS-97-1 Olivier Danvy and Mayer Goldberg. Partial Evaluation of the Euclidian Algorithm (Extended Version). January 1997. 16 pp. To appear in the journal Lisp and Symbolic Computation.

RS-96-62 P. S. Thiagarajan and Igor Walukiewicz. An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. December 1996. i+13 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings.

RS-96-61 Sergei Soloviev. Proof of a Conjecture of S. Mac Lane. December 1996. 53 pp. Extended abstract appears in Pitt, Rydeheard and Johnstone, editors, Category Theory and Computer Science: 6th International Conference, CTCS ’95 Proceedings, LNCS 953, 1995, pages 59–80.

RS-96-60 Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal in 1995. December 1996. 5 pp. Appears in Margaria and Steffen, editors, Tools and Algorithms for The Construction and Analysis of Systems: 2nd International Workshop, TACAS ’96 Proceedings, LNCS 1055, 1996, pages 431–434.

RS-96-59 Kim G. Larsen, Paul Pettersson, and Wang Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. December 1996. 12 pp. Appears in 16th IEEE Real-Time Systems Symposium, RTSS ’95 Proceedings, 1995.

RS-96-58 Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal — a Tool Suite for Automatic Verification of Real–Time Systems. December 1996. 12 pp. Appears in Alur, Henzinger and Sontag, editors, DIMACS Workshop on Verification and Control of Hybrid Systems, HY-BRID ’96 Proceedings, LNCS 1066, 1996, pages 232–243.

RS-96-57 Kim G. Larsen, Paul Pettersson, and Wang Yi. Diagnostic Model-Checking for Real-Time Systems. December 1996.