Finite Model Theory/Basics

From Wikibooks, open books for an open world
Jump to navigation Jump to search

Query[edit | edit source]

Notion

Think of a customer-database-software-product that is used by different companies to manage their customers, i.e. they all use their own installations of the same database-product and of course have the data of their own customers in it. Now one can query such a database e.g. "Customers in Africa" that results in a list of all customers in Africa. Although the content of the databases is different the query is defined for all of them - supposed they have customers, countries and the 'in' relation defined. Of course it may deliver different results.

Similarly one can define queries on structures that deliver a set of elements of the universe. Here a set of symbols S corresponds to the database-product, i.e. the naked database-structure, concrete S-structures to database-instances and an interpretation to a database-entry. E.g. retrieves all possible values for y. In general for formular with n free variables we get a set of n-tuples (that may also be empty). In case the query is a sentence (no free variables) we just get 'yes' or 'no' as result, in case the query has a model in the structure or not. In the database above this can correspond to "Kay Ubuntu is Customer in Africa".

Definition

Let be a S-structure with universe A, m a nonnegative integer and Q a mapping from S-structures to sets of subsets of Am, s.t. each maps to a subset of Am.

Q is said to be a m-ary Query on S-structures iff Q is closed under isomorphism,

where closed (or preserved) under isomorphism is: if by a isomorphism then .

Remarks

  • A 0-ary Q is also called a boolean query. In this case Q maps to A0, that is a 0-tuple, or the empty set. The former result is also called TRUE the latter FALSE.
  • For a boolean query Q a subset C of S-structures can be defined by: iff
  • the closedness condition ensures that only the 'shape' of structures is queries, i.e. it is unimportant what the universe consists of as long as its related in the same way.

Examples

Simple

Take S = {<}. We query 'all elements that have no smaller element'. This gives for a universe of {10, 11, 12} the result {(10)} (A set of 1-ary tuples). The query for 'all elements that have a smaller element' gives {(11), (12)}. A query for 'all directly succeeding elements' gives {(10, 11), (11, 12)} (A set of 2-ary tuples). The query 'there is a biggest element' results in {()} (The 0-ary element), whereas 'there is no biggest element' gives {} (false).

counter example?

Definability[edit | edit source]

On one hand we have queries that can be more or less 'complicated'. Just think of a database-query simply for all customers with name = 'Ubuntu' compared to a query covering many properties and relationships. On the other hand we have languages of different expressive power like FO and MFO (monadic first oder logic). So one can ask if the expressive power of a language is strong enough to express (define) a certain query.

of classes of structures[edit | edit source]

Let C be a class of finite structures and L be a logic. C is said to be definable in the logic L iff there is a sentence φ in L s.t. C is the set of all finite models of φ.

of queries[edit | edit source]

Let Q be a query, L a logic

Q is said to be definable in L iff it exists a formular φ(x1,..., xm) of L in S s.t. for all all elements of are an assignment on φ s.t.

Remarks[edit | edit source]

  • Thus boolean queries are correspond to sentences

Examples[edit | edit source]

Simple

On a finite graph the query 'there is an element that is adjacent with all others' can be written in FO as . The language can even be restricted further, e.g. by allowing only 2 variable per formula (this is approximately what the logic FO2 does).

Application

The database query language SQL contains many extensions to increase its power.

Partial Isomorphy[edit | edit source]

Definition[edit | edit source]

Partial Isomorphism among structures

Let and be relational S-Structures and p be a mapping. Then p is said to be a Partial Isomorphism from to iff all of the following hold

  • dom(p) A and codom(p) B
  • p is injective
  • for every constant symbol c from S and every a: a = cA iff p(a) = cB
  • for every n-ary relation symbol R from S and ,..., : ... iff ...

where A, B.

Remarks[edit | edit source]

  • I.e. a partial Isomorphism on and is a (plain) Isomprphism on the substructures obtained by choosing dom(p) and codom(p) and 'prune' constants and relations respectively.
  • Partial Homomorphim...

Examples[edit | edit source]

  • Let S ={<} be defined over A ={1, 2, 3} and B ={3, 4, 5, 6} the natural way. Then with 1->3 and 2->4 is a partial isomorphism (since 1 < 2 and p(1) < p(2)) as well as with 2->3 and 3->6 as well as with 1->6. Whereas neither with 1->6 and 2->3 (since 1 < 2 but not p(1) < p(2)) nor with 2->5 and 3->5 is a partial isomorphism.
  • Let S ={R} with (a 'square') and (a 'binary tree'). A ={1,..., 4} and B ={1,..., 5}. Then p: {1, 2, 3} -> {1, 3, 4} with 1->1, 2->3, 3->4 is a partial isomorphism from to , since {(1, 2), (2, 3)} becomes {(1, 3), (3, 4)}. Notice that in case contained e.g. (4, 1) additionally, p would not be a partial isomorphism.
  • Let S ={<} be defined over A ={1, 2, 3, 4, 5, 6} and B ={1, 3, 5} the natural way. Then p with 2->3 and 4->5 defines a partial isomorphism. Notice that e.g. holds on but does not hold on . I.e. in general the validity of sentences with quantifiers is not preserved. So in order to preserve this validity we need sth stronger than partial isomorphism. That is mainly what the Ehrenfeucht-games will provide us with.

Definition[edit | edit source]

Partially isomorphic structures

Two structures can said to be partially isomorphic for a certain domain size of p, called n. This can be done in a weak sense, i.e. there exists a n-ary partial isomorphism or in a strict sense, i.e. for every n-elementary subset of A it exists a partial isomprphism. Latter will become important later.

Quantifier Rank[edit | edit source]

Definition : Quantifier Rank of a FO-Formula

Let φ be a FO formula. The quantifier rank of φ, written qr(φ), is defined as

  • , if φ is atomic.
  • .
  • .
  • .

Remarks

  • We write FO[n] for the set of all first-order formulas φ with .
  • Notice that in prenex normal form the Quantifier Rank of φ is exactly the number of quantifiers appearing in φ.

Examples

  • The sentence has the Quantifier Rank 2.
  • The sentence in prenex normal form has the Quantifier Rank 3. Notice that it is equivalent to the above.

Types[edit | edit source]

Notion[edit | edit source]

Definition[edit | edit source]

Rank k m-type

Let...