Logic for Computer Science/Querying

Query and Definability

edit

The problem of satisfiability is central to mathematical logic: for a logic L on a domain D of structures try to find a model in D for a given formula φ from L. The more special problem of model-checking on a logic L and a domain D of structures tries to answer, does   hold for a given structure   and a formula  . Model-checking is an important area in computer science. The concept of querying is leading beyond these 'true-false' evaluations, it introduces the result set as its outcome.

Query

edit

Motivation

Think of a customer-database. Now one can query such a database e.g. "All Customers in Africa" that results in a list of all customers in Africa. In case of a query like "All customers and their countries" the result consists of 2-ary tuples of a customer and a country, whereas the query "(Do) we have a customer in Rwanda" leads to either yes or no. Similarly one can define queries on structures that deliver a set of elements of the universe, where the universe relates to the data in the database.

Notion

First recapture the notion of bound and free variables: whereas a sentence (no free variables) like   computes to either true or false the formula's   truth-value is relative to the free variable y and thus implies a set of values for y for which it is true. In general for a formular with n free variables we get a set of n-tuples (that may also be empty). In this sense sentences deliver 0-ary tuples in case they are true.

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 an 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 queried, i.e. it is unimportant what the universe consists of as long as its related in the same way. Thus questions on the kind of elements of the universe cannot be answered by a query.
  • From a unary query a substructure   of the queried structure   can be obtained with
     , for an m-ary R and with an 1-1 mapping of constants.

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).

Graphs

Typical queries on graphs   are:

  • transitive closure (smallest transitive extension) is a 2-ary query:
     
  • isolated nodes is a 1-ary query:
     
  • planarity is a 0-ary (boolean) query:
     


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 for customers named Ubuntu that are not situated in Africa or middle east. 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.

Definition for classes of structures

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 φ.

Definition for queries

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.  

Examples

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 (and thus is definable in the logic FO2).

Negative

Single step connectivity for graphs can be defined in FO as

 

So we get 2-step connectivity as

 

This can be continued to n-step connectivity for a fixed n, but not for arbitrary n since FO formulas are always of fixed length. It would take some 'infinite conjunction' to expand the above approach to arbitrary length. And since there is no other way to express arbitrary connectivity in FO (what is omitted show here) we say the connectivity query is not definable in FO. It can be shown that it is expressible in UMSO (Universal Monadic Second Order Logic).

Graphs

The definability of the queries considered above is:

  • the transitive closure query is not definable in FO
  • the isolated node query is definable in FO as
     
  • planarity is not definable in FO

Propositions

edit

Query-Safety

TODO

The impact of Order

TODO

Finite Structures

edit

Concept

edit

Definition

A Structure is said to be finite iff it's Universe is finite.

Examples


The unusual effectiveness of finite structures in computer science

edit

Data structures in computer science are usually finite, e.g. a Database always holds finitely many entries. But by restricting to finite structures we have to issues:

  • We still have to deal with structures of arbitrary size, e.g. to sum from 1 to 3 one can write 1 + 2 + 3, from 1 to 4: 1 + 2 + 3 + 4, but from 1 to an arbitrary natural number we must use a special operator like 'Σ' that extends our simple '+' language (Also the '...' notation doesn't help since it extends our language as well).
  • We now have to deal with complexity issues, that we haven't had before. Example ...


Finite Model Theory

edit

So the Theory dealing with finite structures (Finite Model Theory (FMT)) is not just a simplification of the theory also covering infinite ones (Model Theory (MT)). It has it's own character. This is especially an issue when it comes to instruments for proofing. One of the most important of such tools in MT is the compactness theorem, but it is completely useless when we deal with finite structures exclusively:

Consider the following sentence σ3

 

that says that there are at least 3 different elements in a universe. One can expand σ3 easily for n other than 3. So, let Σ = {σ1, σ2, σ3, ...} be the infinite set of all these sentences. Now Σ is obviously not satisfiable by a finite model, although every finite subset of Σ is. Ok, but why does that matter? One of the most useful tools in general Model theory is the Compactness theorem, stating: "Let Σ be a set of FO sentences. If every finite subset of Σ is satisfiable, then Σ is satisfiable." But as just shown this doesn't hold for the finite case, thus there is no Compactness theorem in Finite Model Theory!

And (unfortunately) this is the case for many other important theorems as well (actually the very most of them) like e.g. Gödel's Completeness theorem. Moreover important definitions of MT must be adopted for the finite case. For example the concept of types is a very central one in MT. But applied to FMT it turns out to be quite useless since it already characterises finite structures up to isomorphism. So the definition of types has to be refined in FMT (to a type concept in FO[k], depending on an integer k).

So Finite Model Theorists can not simply adopt the classic instruments from Model theory, they have to find their own. The basic ones are presented in the 'Proofs' section.

The Property of Elementary Equivalence

edit

Querying is about discrimination of structures. So the basic question is "Can i discriminate a structure from all different structures?", where different means not equal up to isomorphy. This can be done for finite structures (but not for infinite ones). E.g. ...

Properties for a finite Number of Structures

edit

So being of a certain structure can be seen as an elementary property, that discriminates a class of isomorphic structures from all others. Now we can think of properties that discriminate 2 different (nonisomorphic) structures from the rest. They can also be discriminated by simply connecting the properties, like e.g. ...

This can be extended to properties for a finite number of structures, like e.g. ...

Properties for an infinite Number of Structures

edit

Also properties that hold for an infinite number of structures can be thought of. But these are not discriminatable in the above way. E.g. ...

There are Logics that allow this sort of infinite disjunction, like ...

So, are there other ways to discriminate these structure in FO? Sometimes, like in the case of ...

So we need a decision tool (method) that decides if structures with a certain property can be discriminated or not, i.e. responds either "yes" or "no" for all possible properties, i.e. is sound and complete.

The special roles of First-Order and Infinitary Logics

edit

TODO

Some Definability Results

edit

FO on Graphs

edit

Fragments of SO

edit

MSO and EMSO on Graphs

edit

MSO and FO on Strings

edit

Fixed-Point Logics

edit