Finite Model Theory/Basics

From Wikibooks, open books for an open world
< Finite Model Theory
Jump to: navigation, search

Query[edit]

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. \forall_x xRy 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 \mathfrak A be a S-structure with universe A, m a nonegative integer and Q a mapping from S-structures to sets of subsets of Am, s.t. each \mathfrak A 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 \mathfrak A \cong \mathfrak B by a isomorphism f then f(Q(\mathfrak A)) = Q(\mathfrak B).

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: \mathfrak A \in C iff Q(\mathfrak A) = true
  • the closedness condition ensures that only the 'shape' of structures is queries, i.e. it is inimportant 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]

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]

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]

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 \mathfrak A all elements of Q(\mathfrak A) are an assignment on φ s.t. \mathfrak A \vDash \varphi

Remarks[edit]

  • Thus boolean queries are correspond to sentences

Examples[edit]

Simple

On a finite graph the query 'there is an element that is adjacent with all others' can be written in FO as \exists_x \forall_y x R y. 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 it's power.

Partial Isomorphy[edit]

Definition[edit]

Partial Isomorphism among structures

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

  • dom(p) \subseteq A and codom(p) \subseteq 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 a_1, ..., a_n: R^\mathfrak{A} a_1 ... a_n iff R^\mathfrak{B} p(a_1) ... p(a_n)

where a_* \in A, b_* \in B.

Remarks[edit]

  • I.e. a partial Isomorphism on \mathfrak{A} and \mathfrak{B} 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]

  • Let S ={<} be defined over A ={1, 2, 3} and B ={3, 4, 5, 6} the natural way. Then p_1 with 1->3 and 2->4 is a partial isomorphism (since 1 < 2 and p(1) < p(2)) as well as p_3 with 2->3 and 3->6 as well as p_2 with 1->6. Whereas neither p_4 with 1->6 and 2->3 (since 1 < 2 but not p(1) < p(2)) nor p_5 with 2->5 and 3->5 is a partial isomorphism.
  • Let S ={R} with R^\mathfrak{A} =\{(1, 2), (2, 3), (3, 4), (4, 1)\} (a 'square') and R^\mathfrak{B} =\{(1, 2), (1, 3), (3, 4), (3, 5)\} (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 \mathfrak{A} to \mathfrak{B}, since {(1, 2), (2, 3)} becomes {(1, 3), (3, 4)}. Notice that in case R_\mathfrak{B} 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. \exists_x( x<4 \and 2<x ) holds on \mathfrak{A} but \exists_x( x<p(4) \and p(2)<x ) does not hold on \mathfrak{B}. 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]

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]

Definition : Quantifier Rank of a FO-Formula

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

  • qr(\varphi) = 0, if φ is atomic.
  • qr(\varphi_1 \land \varphi_2) = qr(\varphi_1 \lor \varphi_2) = max(qr(\varphi_1), qr(\varphi_2)).
  • qr(\lnot \varphi) = qr(\varphi).
  • qr(\exists_x \varphi) = qr(\varphi) + 1.

Remarks

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

Examples

  • The sentence \forall_x ( \exists_y ((\lnot x = y) \land x R y ) ) \land ( \exists_y ((\lnot x = z) \land z R x ) ) has the Quantifier Rank 2.
  • The sentence in prenex normal form \forall_x\exists_y\exists_y ((\lnot x = y) \land x R y )  \land ( (\lnot x = z) \land z R x ) has the Quantifier Rank 3. Notice that it is equivalent to the above.

Types[edit]

Notion[edit]

Definition[edit]

Rank k m-type

Let ...