D-Structures and their Semantics

Rohit Parikh

April 1, 1999

Abstract

In these notes we shall be concerned with a semantic object which is a generalization of classical structures, Kripke structures and the regular ∗-structures of Ehrenfeuchtde Jongh. We shall start by showing how these different cases can be obtained by imposing different regularly conditions on the basic object (D-structures) and the semantics can then be directly interpreted into the semantics of D-structures. We shall then give a game-theoretic explanation of the semantics of the D-structures from which the finite model property of regular ∗-sructures can be easily obtained. We go on to look at the proof theory of these objects.

Contents

1 Introduction 2

2 A Game Theoretic Characterisation 7

3 The logic of D-structures 9

1 Introduction

In this survey we shall show that a D-structure is a very flexible (but nontrivial) type of object and includes classical structures, intutionistic structures^{1}, and the regular ∗-structures of Ehrenfeucht-de Jongh as special cases The intuitive idea is this. At any moment of time, what we know about the world is a finite amount, but as time passes, and if our memory is good, this finite amount increases. In other words, the old information is embedded in the new information. The way in which the old information is embedded can be chosen in various possible ways and these different choices lead to different semantics.

In the following, μ will be a finite relational type. Constants are permitte but not function symbols.

Definition 1 A D-structure M of type μ consists of two objects:

1. a family F of finite relational structures (diagrams), all of type μ and 2. a family H of homomorphisms between elements of F. H includes all

the identity maps. H^{t} is the closure of H under composition and clearly ⟨F, H^{t}⟩ will be a category.

Remark: Note that homomorphisms preserve atomic formulae but not necessarily their negations. Members of H will be called allowable maps.

Definition 2 A D-structure M will be said to be rigid if all allowable maps are inclusions. It is directed if given D_{1}, D_{2} in F there is a D_{3} and allowable maps p_{1} : D_{1} → D_{3} and p_{2} : D_{2} → D_{3}. M is weakly directed if ⟨F, H^{t}⟩ is directed.

Definition 3 Let A be a sentence of the language L_{u} augmented by constants from a diagram D (we shall take the elements themselves to be these constants) and modal operators □ and ⋄. We recall that □ means “necessarily” and ⋄ means “possibly”. We define M, D⊧A by induction on the complexity c(A) of A.

1. c(A) = 0. Then M, D⊧A iff A is true in D.

2. A = B ∧ C. Then M, D⊧B ∧ C iff M, D⊧B and M, D⊧C.

3. A = B ∨ C. Then M, D⊧B ∨ C iff M, D⊧B or M, D⊧C.

4. A = ¬B. Then M, D⊧¬B iff M, D |̸=B.

5. A = (∃x)B(x). Then M, D⊧(∃x)B(x) iff there exists a ∈ |D| such that M, D⊧B(a).

6. A = (∀x)B(x). Then M, D⊧(∀x)B(x) iff for all a ∈ |D|, M, D′⊧B(a).

7. A = □B(a_{1}, …, a_{k}). Then

M, D⊧□B(a_{1}, …, a_{k}) iff for all allowable f : D → D′,
M, D′⊧B(f(a_{1}), …, f(a_{k})).

1The finiteness requirement on elements of M has to be dropped in this case, for technical reasons on the diagrams.

8. A = ⋄B(a_{1}, …, a_{k}). Then

M, D⊧ ⋄ B(a_{1}, …, a_{k}) iff for some allowable f : D → D′,
M, D⊧B(f(a_{1}), …, f(a_{k})).

In 7, 8 the constants from |D| are explicitly displayed.

Before studying D-structures in general we shall verify the claim made on before Definition 1.

Definition 4 Let A be a formula of the language L_{μ∗D}, i.e. L_{μ} with constants from |D|. A^{c} is the formula obtained from A if we replace ∃ everywhere by ⋄∃ and ∀ everywhere by □∀.

Theorem 5 Let A be a classical μ-structure. M^{c}(A) = M is th D-structure where F consists of all finite substructures of A. H consists of all inclusion maps. (Thus M is directed and rigid.) A is any sentence of L_{μ∗D}. Then

A⊧A  iff  M, D⊧A^{c},

where D contains all constants of A.

Proof. ¬, ∨, ∧ and atomic sentences are trivial. Suppose now that A is (∃x)B(x, a_{1}, …, a_{k}) then A^{c} is ⋄(∃x)B^{c}(x, a_{1}, …, a_{k}).

[left to right] Suppose A⊧A. Then there is an a ∈ |A| such that

A⊧B(a, a_{1}, …, a_{k}).

Let D′ be a substructure containing D and a. Then by induction hypothesis, M, D′⊧B^{c}(a, a_{1}, …, a_{k}) hence M, D′⊧(∃x)B^{c}(x, a_{1}, …, a_{k}) hence

M, D⊧ ⋄ (∃x)B^{c}(x, a_{1}, …, a_{k}).

I.e. M, D⊧A^{c}.

[right to left] Suppose

M, D⊧ ⋄ (∃x)B^{c}(x, a_{1}, …, a_{k})

then there is a D′ such that D ⊆ D′ and a ∈ D′ such that M, D′⊧B^{c}(a, a_{1}, …, a_{k}). But then A⊧B(a, a_{1}, a_{2}, …, a_{k}) and hence

A⊧(∃x)B(x, a_{1}, a_{2}, …, a_{k}).

The ∀ case is similar.

Theorem 6 Let M be a directed, rigid D-structure. Let

A = ⋃_{D_{a}∈F} D_{a}.

(This union makes sense since M is directed and rigid.) Then, for sentences A of L_{u∗A}, we have if D contains all constants of A,

M, D⊧A^{c}  iff  A⊧A.

Proof. Quite similar to above.

Definition 7 Let A be a formula of the intuitionistic predicate calculus with symbols from μ and additional constants. We define A^{i} by induction on c(A).

1. c(A) = 0, A^{i} = A

2. A = B ∧ C, A^{i} = B^{i} ∧ C^{i}

3. A = B ∨ C, A^{i} = B^{i} ∨ C^{i}

4. A = ¬B, A^{i} = □¬B^{i}

5. A = B → C, A^{i} = □(B^{i} → C^{i})

6. A = (∀x)B(x), A^{i} = □(∀x)B^{i}(x)

7. A = (∃x)B(x), A^{i} = (∃x)B^{i}(x).

(In cases 2,3,7, we could take A^{i} = □(∃x)B^{i}(x) etc. and the next theorem will still hold.)

Definition 8 Let A be an intuitionistic structure (as in [Fit69] p.46). Let D_{Γ} be the structure with base set P (Γ), and in which precisely those atomic A hold where Γ⊧A. There is a homomorphism (which comes from set inclusion) from D_{Γ} to D_{Γ′} just in case R(Γ, Γ′). Then, M = M^{i}(A) is ⟨F, H⟩ where F = {D_{Γ} : Γ ∈ G} and H consists of the homomorphisms just mentioned.

Theorem 9 Let A be a sentence in P̂(Γ). Then

M, D_{Γ}⊧A^{i}  iff  Γ⊧A.

Proof. The proof is immediate if A is atomic. Also, ∧, ∨, ∃ will work in a parallel way. Suppose A = ¬B. Then, A^{i} = □¬B^{i}. We have:

Γ⊧¬B iff for all Γ^{∗}, Γ^{∗} |̸=B
iff for all D_{Γ^{∗}}, M, D_{Γ^{∗}} |̸=B (ind. hyp)
iff for all D_{Γ^{∗}}, M, D_{Γ^{∗}}⊧¬B
iff M, D_{Γ}⊧□¬B^{i}

A = B → C and A = (∀x)B(x) are similar.

Suppose now that M = ⟨F, H⟩ is a D-structure which is a category. We construct a Kripke structure corresponding to M. Given D ∈ F, a selection S for D is a set of maps into D such that if there are any maps D′ → D there is just one such map in S. Take G = the set of all pairs < D, S >, where D ∈ F and S in a selection for D. For Γ = < D, S > ∈ G, take P (Γ) = |D| and an atomic sentence A in P(Γ) is forced by Γ iff it holds in D. We let ΓRΓ′ iff there is a map g ∈ S′, g : D → D′ such that for all f ∈ S, f ∘ g ∈ S′. (We point out that given g : D → D′ there is always such an S′.)

Theorem 10 For A in the language of IPC with constants from D, with Γ = ⟨D, S⟩,

Γ⊧A  iff  M, D⊧A^{i}.

Proof. Quite routine. To check one case, suppose A = ¬B. Then, A^{i} = □¬B^{i}. Then,

Γ⊧A iff ∀Γ^{∗}, Γ^{∗} |̸=B
iff ∀D′ with allowable g : D → D′, M, D′ |̸=B^{i}
iff ∀D′ with allowable g : D → D′, M, D′⊧¬B^{i}
iff M, D⊧□¬B^{i}

etc.

Definition 11 Let A be a (classical) structure of type μ and f a permutation o |A|. Then f(A) is the structure with base set |A| in which

f(A)⊧R(f(a_{1}), f(a_{2}), …, f(a_{n}))  iff  A⊧R(a_{1}, a_{2}, …, a_{n}),

where R ∈ u and a_{1}, a_{2}, …, a_{n} ∈ |A|. A regular ∗-structure over A is a family {f(A) | f ∈ G}, where G is some group containing all finite permutations of |A|.

Definition 12 Let M be a family of first order structures all of the same type μ and with the same base set X. If X_{0} ⊆ X, M ∈ M then

M[X_{0}, M] = {N | N ∈ M and N|_{X_{0}} = M|_{X_{0}}}

Definition 13 (Ehrenfeucht) Let M be a regular ∗-structure on A. X_{0} ⊆ |A|, M ∈ M. A is a sentence of L_{μ∗X_{0}}. We define M[X_{0}, M]⊧A by induction on c(A).

1. c(A) = 0. Then M[X_{0}, M]⊧A iff M⊧A. (Note: this depends only on M|_{X_{0}}.)

2. A = B ∧ C. Then M[X_{0}, M]⊧A iff M[X_{0}, M]⊧B and M[X_{0}, M]⊧C.

3. A = B ∨ C. Then M[X_{0}, M]⊧A iff M[X_{0}, M]⊧B or M[X_{0}, M]⊧C.

4. A = ¬B. Then M[X_{0}, M]⊧A iff M[X_{0}, M] |̸=B.

5. A = (∃x)B(x). Then

M[X_{0}, M]⊧A iff there exist a ∈ X, b ∈ X_{0} ∪ {a}, N ∈ M[X_{0}, M]
such that M[X_{0} ∪ {a}, N]⊧B(b).

6. A = (∀x)B(x). Then

M[X_{0}, M]⊧A iff for all a ∈ X, b ∈ X_{0} ∪ {a}, N ∈ M[X_{0}, M],
M[X_{0} ∪ {a}, N]⊧B(b).

Theorem 14 Let M be a regular ∗-structure on A. Let M_{1} = ⟨F, H⟩ be defined as follows

F = all finite submodels D_{i} of A,

H = all monomorphisms D → D′ with \overline{\overline{D′}} − \overline{\overline{D}} ≤ 1.

Let X_{0} = {a_{1}, a_{2}, …, a_{n}}, A(a_{1}, a_{2}, …, a_{n}) ∈ L_{u∗X_{0}}, M ∈ M and

b_{1}, b_{2}, …, b_{n} ∈ |A| such that A|_{b_{1},b_{2},...,b_{n}} = M|_{a_{1},a_{2},...,a_{n}}.

Then

M[X_{0}, M]⊧A(a_{1}, a_{2}, …, a_{n}) iff M_{1}, D⊧A^{c}(b_{1}, b_{2}, …, b_{n}),

where {b_{1}, b_{2}, …, b_{n}} ⊆ |D|.

Proof. Trivial if A is atomic, a negation, conjuction, or disjunction.

Suppose A = (∀x)B(x). Then, M[X_{0}, M]⊧A(a_{1}, a_{2}, …, a_{n}) gives, for all N, a, b as provided,

M[X_{0} ∪ {a}, N]⊧B(a_{1}, a_{2}, …, a_{n}, b).

Now, let g : D → D′ be an allowable map. We need to show that

M, D′⊧B^{c}(g(b_{1}), …, g(b_{n}), c), for all c ∈ |D′|.

Now, there is a permutation ϕ such that ϕ(g(b_{i})) = a_{i}. Take a = ϕ(b), where b ∈ D′ − g[D], if D′ ≠ g[D] and let a ∈ {a_{1}, …, a_{n}} otherwise.Let b = ϕ(c). Let N = ϕ(A). Then

N|_{{a_{1},...,a_{n}}} = M|_{{a_{1},...,a_{n}}}
≃ A|_{{b_{1},b_{2},...,b_{n}}}
≃ A|_{{g(b_{1}),g(b_{2}),...,g(b_{n})}}.

and we get

M[X_{0} ∪ {a}, N]⊧B(a_{1}.a_{2}…. , a_{n}, b)

hence

M, D′⊧B^{c}(g(b_{1}), …, g(b_{n}), c)

Thus

M, D′⊧(∀x)B^{c}(g(b_{1}), …, g(b_{n}), x)

Hence,

M, D⊧□(∀x)B^{c}(g(b_{1}), …, g(b_{n}), x)

which was to be proved.

The backward argument and the ∃ case are quite similar.

We now show that a D-structure M = ⟨F, H⟩ corresponds to a regular ∗-structure if

1. M is weakly directed,

2. D ∈ F and D′ ⊆ D → D′ ∈ F,

3. the allowable maps are those monomorphisms D → D′ where

\overline{\overline{D′}} = \overline{\overline{D}} ≤ 1.

Theorem 15 Let M be a D-structure as above. Choose a maximal subfamily K ⊆ H^{t} such that K is closed under composition and K contains at most one map from any D to D′. Let A be the direct limit of F under K, and M_{1} a regular ∗-structure on A. Suppose X_{0} ⊆ |A|, M ∈ M_{1} and D, a′_{1}, a′_{2}, …, a′_{n} are such that D ∈ F and D|_{{a′_{1},a′_{2},...,a′_{n}}} ≃ M|_{X_{0}}. Then,

M_{1}[X_{0}, M]⊧A(a_{1}, a_{2}, …, , a_{n}) iff M, D⊧A^{c}(a′_{1}, a′_{2}, …, a′_{n}).

Proof. The proof is straightforward.

2 A Game Theoretic Characterisation

Let μ be a relational type, M a D-structure of type μ, D ∈ M, L = L_{μ∗D}^{M} the language of modal logic (with quantifiers) and nonlogical symbols from μ and |D|, A a closed formula of L. We define a game G_{A,D} by induction on the complexity of A. (1), (2) are two players.

1. A is atomic. G_{A,D} is won by (1) iff D⊧A. Otherwise, it is won by (2).

2. A = B ∧C. Player (2) may choose either game G_{B,D} or G_{C,D} which is then played.

3. A = B ∨C. Player (1) may choose either game G_{B,D} or G_{C,D} which is then played.

4. A = ¬B. (1) wins G_{A,D} iff (s)he loses G_{B,D}.

5. A = (∀x)B(x). Player (2) chooses an a ∈ |D|. The game G_{B(a),D} is then played.

6. A = (∃x)b(x). Player (1) chooses an a ∈ |D|. The game G_{B(a),D} is then played.

7. A = □B(a_{1}, a_{2}, …, a_{n}). Player (2) chooses an f : D → D′, f ∈ H. The game G_{D′,B(f(a_{1}),f(a_{2}),...,f(a_{n}))} is then played.

8. Like (7) except player (1) chooses the f.

(In 7, the elements of |D| are displayed.)

Theorem 16 M, D⊧A iff player (1) has a winning strategy for G_{A,D}.

Corollary 17 Let M = G_{M} be a regular ∗-structure where M is classical and G is a group containing all finite permutations of |M|. Let A closed such that, M⊧A. There exists a finite X ⊆ |M| such that if N = M|_{X} and G_{1} = all permutations of X, then G, M⊧A. (This can be called the “finite model property”.)

Proof. Let l = c(A). There are only finitely many possible diagrams of type μ and size ≤ l (upto isomorphism). Choose X_{i} ⊆ M such that M|_{X_{i}} is a representative of the ith type occuring inside M. Let X = the union of all the X_{i}. Let N = M|_{X}.

Let M_{1} be the D-structure consisting of all diagrams in N with allowable maps being monomorphisms D → D′ with \overline{\overline{D′}} − \overline{\overline{D}} ≤ 1.

M_{2} is the analogous D-structure for M.

Then, clearly, a closed formula of complexity ≤ l holds in M_{1}, D iff it holds in M_{2}, D, where D is the empty diagram. Hence, we get

G_{M}⊧A iff M_{2}⊧A
iff M_{1}⊧A
iff G, N⊧A

using theorem 14.

Theorem 18 (Skolem-Lowenheim theorem for D-structures) Let M = ⟨F, H⟩ be a D-structure. Then there exist countable F_{1}, H_{1}, F_{1} ⊂ F, H_{1} ⊂ H such that for all D ∈ F_{1}, A ∈ L_{μ∗D}^{M},

M_{1} = ⟨F_{1}, H_{1}⟩⊧A  iff  M⊧A.

Moreover, M_{1} is rigid, directed, weakly directed as a category etc. iff M_{1} is. Thus M_{1} corresponds to an intuitionistic, classical, or regular ∗-structure iff M does.

Proof. Let

X = F ∪ H^{t} ∪ ⋃{|D| | D ∈ F}.

We look at the classical structure with base set and relations, constants corresponding to these in μ plus some others. Thus for a relation R(x_{1}, …, x_{n}) ∈ u we have a relation R′(y, x_{1}, …, x_{n}) which holds iff y is a digram and R(x_{1}, …, x_{n}) holds in y. We also have monadic predicates corresponding to F, H, H^{t}, ⋃{|D| | D ∈ F}. In addition we have a function f of two arguments such that

f(x, y) = x(y)  whenever x ∈ H^{t} and y in some D,
where x : D → D′,
= something not an element if the conditions are not fulfilled.

Then we have the following. For each formula A of L_{μ∗D}^{M}, there is a formula A′ in the language of M with constants from |D|, such that

M⊧A  iff  M⊧A′.

Moreover, there are formulae of M expressing various properties of M mentioned. Now take a countable substructure M_{1} of M and take the M_{1} corresponding.

Special cases of this theorem include: classical structures, intuitionistic structures, regular ∗-structures and rigid D-structures. Note that many properties not explicitly mentioned will be elementary in M (possibly after expanding the language) and will be inherited by M_{1}.

Game theoretic arguments can be used to give very direct proofs of many results of [EGGdJ] about regular ∗-structures.

3 The logic of D-structures

We recall the three systems M, M′, M′′ for modal quantificational logic. M consists of

1. the axioms and rules for the predicate calculus,

2. the axioms

A → ⋄A
□A ↔ ¬ ⋄ ¬A
⋄(A ∨ B) ↔ ⋄A ∨ ⋄B,

3. the rules

if ⊢ A ↔ B then ⋄ A ↔ ⋄B

and

if ⊢ A then □A.

Theorem 19 All theorems of M are valid in all D-structures.

Proof. It is clear that the axioms are valid and the rules preserve validity.

The system M′ is S4 and is obtained by adding the axiom □A → □□A. The system M′′ is S5 and is obtained by adding, in addition, the axiom (⋄□A) → □A.

Definition 20 M = ⟨F, H⟩ is filtered if for all allowable maps f : D → D′, g : D → D′′ there exist D′′′, h, k such that the diagram

[figure: D; D′; D′′; D′′′; f; g; h; k]

commutes. M is weakly filtered if ⟨F, H^{t}⟩ is filtered.

Theorem 21 If M is a category then M⊧S4.

Proof. Immediate from the definition.

The converse is not true. Suppose we have a situation

[figure: D; D′_{1}; D_{1}; D_{2}; f′; f; g′; g]

where g ∘ f belongs to H but g′ ∘ f′ does not. However D′_{1} is a copy of D_{1} as far as D is concerned. Then the structure given above will act logically like a category. We do not know if there are any nontrivial examples.

Acknowledgements: I thank K. Georgatos for transcribing my handwritten notes and Ruili Ye for some corrections.

References

[EGGdJ] A. Ehrenfeucht, J. Geiser, C. E. Gordon and D. H. J. de Jongh. A semantics for non iterated local observation. Preprint 197?

[Eh74] Andrzej Ehrenfeucht ”Logic without Iterations” Proceedings of the Tarski Symposium (1974) pp. 265-268.

[Fit69] Melvin C. Fitting. Intuitionistic Logic, Model Theory and Forcing. North-Holland, Amsterdam, 1969.

[GJP72] Dick H.J.de Jongh, Nick Goodman and Rohit Parikh ”On Regular *-structures with Classical Theories”, J. Symb. Logic 37 (1972) 777.

[Pa72] Rohit Parikh ”D-Structures and their Semantics”, Notices of the Amer. Math. Soc. 19 (1972) A329.

[PM72] Rohit Parikh and John Mayberry ”D-structures and *-structures”, Notices of the Amer. Math. Soc. 19 (1972) A454.