Logic for Computer Science/Querying

Query and Definability

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 ${\mathfrak {A}}\vDash \psi \$ hold for a given structure ${\mathfrak {A}}\in D$ and a formula $\psi \ \in L$. 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

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 $\forall _{x}\exists _{y}xRy$ computes to either true or false the formula's $\forall _{x}xRy$ 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 ${\mathfrak {A}}$ be a S-structure with universe A, m a nonnegative integer and Q a mapping from S-structures to sets of subsets of A^m, s.t. each ${\mathfrak {A}}$ maps to a subset of A^m.

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 an 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 A⁰, 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 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 ${\mathfrak {B}}$ of the queried structure ${\mathfrak {A}}$ can be obtained with

  $R^{\mathfrak {B}}=R^{\mathfrak {A}}\cap Q^{m}$, 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 $G=(V,E)$ are:

• transitive closure (smallest transitive extension) is a 2-ary query:

  ${\big \{}(x,y)\in V^{2}|{\mbox{ there is a path from x to y }}{\big \}}$

• isolated nodes is a 1-ary query:

  $\{(x)\in V|{\mbox{ there is no node connected with x }}\}$

• planarity is a 0-ary (boolean) query:

  ${\begin{cases}\{()\}&{\mbox{if G is planar}}\\\{\}&else\end{cases}}$

Definability

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 φ(x₁, ..., x_m) 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$

Examples

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}xRy$. The language can even be restricted further, e.g. by allowing only 2 variable per formula (and thus is definable in the logic FO²).

Negative

Single step connectivity for graphs can be defined in FO as

$\forall _{xy}E(x,y)$

So we get 2-step connectivity as

$\forall _{xz}\exists _{y}E(x,y)\land E(y,z)$

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

  $\forall _{y}\neg E(x,y)$

• planarity is not definable in FO

Propositions

Query-Safety

TODO

The impact of Order

TODO

Finite Structures

Concept

Definition

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

Examples

The unusual effectiveness of finite structures in computer science

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

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

$\exists _{x}\exists _{y}\exists _{z}(x\neq y\land y\neq z\land x\neq z)$

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

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

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

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

TODO