All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.

Description

D-Structures and their semantics Rohit Parikh 1 D-Structures In these notes we shall be concerned with a semantic object which is a generalization of classical structures, Kripke structures and the regular

Transcript

D-Structures and their semantics Rohit Parikh 1 D-Structures 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 Ehrenfeucht-de 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. In the following, µ will be a finite relational type. function symbols. Constants are permitted but not 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. Departments of Computer Science, Mathematics and Philosophy, Graduate School and University Center, City University of New York, 33 West 42nd Street, New York, NY 10036; also Department of Computer Science, Brooklyn College of CUNY; 1 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 (cf. theorems of this section). 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 6. A = ( x)b(x). Then M, D =( x)b(x) iff there exists a D such that M, D =B(a). 7. A = B(a 1,..., a k ). Then 8. A = B(a 1,..., a k ). Then M, D =( x)b(x) iff for all a D, M, D =B(a). M, D = B(a 1,..., a k ) iff for all allowable f : D D, M, D =B(f(a 1 ),..., f(a k )). M, D = B(a 1,..., a k ) iff for some allowable f : D D, M, D =B(f(a 1 ),..., f(a k )). 1 The finiteness requirement on elements of M has to be dropped in this case, for technical reasons on the diagrams. 2 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 the 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 where D contains all constants of A. A =A iff M, D =A c, 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 I.e. M, D =A c. [right to left] Suppose M, D = ( x)b c (x, a 1,..., a k ). 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 The case is similar. A =( x)b(x, a 1, a 2,..., a k ). Theorem 6 Let M be a directed, rigid D-structure. Let A = D a. D a F (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, Proof. Quite similar to above. M, D =A c iff A =A. 3 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 a g : D D there is always such an S.) 4 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 of 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 X0 = M X0 } Definition 13 (Ehrenfeucht) Let M be a regular -structure on A. X 0 A, M M. A is a sentence of L µ X0. We define M[X 0, M] =A by induction on c(a). 1. c(a) = 0. Then (Note: this depends only on M X0.) 2. A = B C. Then 3. A = B C. Then M[X 0, M] =A iff M =A. M[X 0, M] =A iff M[X 0, M] =B and M[X 0, M] =C. 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 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 D D 1. Let X 0 = {a 1, a 2,..., a n }, A(a 1, a 2,..., a n ) L u X0, M M and Then where {b 1, b 2,..., b n } D. b 1, b 2,..., b n A such that A b1,b 2,...,b n = M a1,a 2,...,a n. M[X 0, M] =A(a 1, a 2,..., a n ) iff M 1, D =A c (b 1, b 2,..., b n ), 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 and we get hence Thus Hence, which was to be proved. N {a1,...,a n} = M {a1,...,a n} A {b1,b 2,...,b n} A {g(b1 ),g(b 2 ),...,g(b n)}. M[X 0 {a}, N] =B(a 1.a 2...., a n, b) M, D =B c (g(b 1 ),..., g(b n ), c) M, D =( x)b c (g(b 1 ),..., g(b n ), x) M, D = ( x)b c (g(b 1 ),..., g(b n ), x) The backward argument and the case are quite similar. 6 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 D = 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 X0. 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. These notes will continue. 2 A Game Theoretic Characterisation Let µ be a relational type, M a D-structure of type µ, D M, L = L M µ D 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. 7 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 Xi 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 D 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 using theorem 14. G M =A iff M 2 =A iff M 1 =A iff G, N =A 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 M µ D, 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 M µ D, 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. 8 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 3. the rules and A A A A (A B) A B, if A B then A B 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 f D h D D g D k commutes. M is weakly filtered if F, H t is filtered. 9 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 D D 1 f g D 2 f D 1 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 thanks 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] [Fit69] [GJP72] Andrzej Ehrenfeucht Logic without Iterations Proceedings of the Tarski Symposium (1974) pp Melvin C. Fitting. Intuitionistic Logic, Model Theory and Forcing. North-Holland, Amsterdam, 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 AMS 19 (1972) A329. [PM72] Rohit Parikh and John Mayberry D-structures and *-structures, Notices of the AMS 19 (1972) A

Related Search

We Need Your Support

Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks