Logic for Computer Science/Querying Proofs

Definition (partial isomorphism on relational S-Structures)

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

• dom(p) ${\displaystyle \subset }$ A and codom(p) ${\displaystyle \subset }$ B
• for every ${\displaystyle a_{1}}$, ${\displaystyle a_{2}}$: ${\displaystyle a_{1}}$ = ${\displaystyle a_{2}}$ iff p(${\displaystyle a_{1}}$) = p(${\displaystyle a_{2}}$).
• for every constant symbol c from S and every a: a = c iff p(a) = c
• for every n-ary relation symbol R from S and ${\displaystyle a_{1}}$, ..., ${\displaystyle a_{n}}$: ${\displaystyle R^{\mathfrak {A}}}$ ${\displaystyle a_{1}}$ ... ${\displaystyle a_{n}}$ iff ${\displaystyle R^{\mathfrak {B}}}$ ${\displaystyle p(a_{1})}$ ... ${\displaystyle p(a_{n})}$

where ${\displaystyle a_{*}}$ ${\displaystyle \in }$ A, ${\displaystyle b_{*}}$ ${\displaystyle \in }$ B.

Remark

• I.e. a partial Isomorphism on ${\displaystyle {\mathfrak {A}}}$ and ${\displaystyle {\mathfrak {B}}}$ is a (plain) Isomprphism on the substructures obtained by choosing dom(p) and codom(p) and 'prune' constants and relations respectively.

Example

• Let S ={<} be defined over A ={1, 2, 3} and B ={3, 4, 5, 6} the 'usual' way. Then ${\displaystyle p_{1}}$ with 1->3 and 2->4 is a partial isomorphism (since 1 < 2 and p(1) < p(2)) as well as ${\displaystyle p_{3}}$ with 2->3 and 3->6 as well as ${\displaystyle p_{2}}$ with 1->6. Whereas neither ${\displaystyle p_{4}}$ with 1->6 and 2->3 (since 1 < 2 but not p(1) < p(2)) nor ${\displaystyle p_{5}}$ with 2->5 and 3->5 is a partial isomorphism.

• Let S ={R} with ${\displaystyle R^{\mathfrak {A}}=\{(1,2),(2,3),(3,4),(4,1)\}}$ (a 'square') and ${\displaystyle 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 ${\displaystyle {\mathfrak {A}}}$ to ${\displaystyle {\mathfrak {B}}}$, since {(1, 2), (2, 3)} becomes {(1, 3), (3, 4)}. Notice that in case ${\displaystyle 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} in the 'usual' way. Then p with 2->3 and 4->5 defines a partial isomorphism. Notice that e.g. ${\displaystyle \exists _{x}(x<4\land 2<x)}$ holds on ${\displaystyle {\mathfrak {A}}}$ but ${\displaystyle \exists _{x}(x<p(4)\land p(2)<x)}$ does not hold on ${\displaystyle {\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

Suppose that we are given two structures ${\displaystyle {\mathfrak {A}}}$ and ${\displaystyle {\mathfrak {B}}}$, each with no function symbols and the same set of relation symbols, and a fixed natural number n.

Then an Ehrenfeucht-Fraisse game is a game with the subsequent properties:

• Elements
  • a position is a pair of sequences α and β, both of length i, i ${\displaystyle \in }$ 0, ..., n
  • the starting position is the pair of empty sequences (i = 0)
  • the game is finished iff α and β are both of size n
  • the players are the 'spoiler' S and the 'duplicator' D
• Moves
  • moves are carried out alternatingly
  • S moves first
  • S chooses exactly one element of either A or B that has not been chosen already (latter is not relevant in the first move)
  • D chooses exactly one element of the other set, i.e. if S has chosen from A then D has to choose from B and if S chose one from B then D has to choose from A.
• Winning & Information
  • D wins iff the final position defines a partial isomorphism by mapping the i-th elements of α and β, for all i.
  • else S wins
  • both players know both of the structures completely and also know about all the moves played previously

Remark

• notice that above constants are not mentioned (yet)

Example

• Let A ={1, 2, 3}, B ={1, 2}, S ={ < }, where '<' is defined the 'usual' way. Here player S can win by playing 2 in the first move and playing the second move corresponding to D's first move in the following way: to 1 he responds 1 and in case of 2 his answer is 3. In both cases D can not follow. He may have isomorphic structures e.g. {2, 3} and {1, 2} but the mapping defined by the sequence of moves is twisted, i.e. it maps 2 to 2 (1st move) and 3 to 1 and thus is not a partial isomorphism.

• Let A ={1, 2, ..., 9}, B ={1, 2, ..., 8}, S ={ < }, where '<' is defined the 'usual' way. So, what is the best way to play for S? In case S picks 1 from A, D picks 1 from B and the game left is mainly the same as before just with 1 element less but also 1 move played already. But we can make a better deal for the price of one move: by playing 5 in A, D is forced to play 5 (or 4) in B what leaves two possible ways to proceed for S: either playing the {1, 2, 3, 4} vs {1, 2, 3, 4} game what of course would lead to an obvious win for D, or playing the {6, 7, 8, 9} vs {6, 7, 8} game. Choosing the latter the quickest win for S is 7 - 7, 8 - 8 and finally 9 with a 4 move win. Since there is no better way to play for both sides S wins if n > 3 for the structures above.

• The result from the above example can be generalised to: For linear orders in an n-move Ehrenfeucht game D has a winning strategy if the size of each of A and B is less or equal 2^n.

• 

  The following is an (popular) illustrative representation of an Ehrenfeucht-game: from the two sequences S has won iff the lines connecting matching letters cross (if D can find a match at all), e.g. S wins after three moves:

...

Definition

The function qr(φ) is said to be the Quantifier Ranking of φ iff

• ${\displaystyle qr(\varphi )=0}$, for φ atomic
• ${\displaystyle qr(\varphi _{1}\land \varphi _{2})=qr(\varphi _{1}\lor \varphi _{2})=max(qr(\varphi _{1}),qr(\varphi _{2}))}$
• ${\displaystyle qr(\lnot \varphi )=qr(\varphi )}$
• ${\displaystyle qr(\forall \varphi )=qr(\exists \varphi )=qr(\varphi )+1}$

Remark

• qr(φ) describes the 'depth of quantifier nesting' of φ.
• We write FO[k] for all Formulas of Quantifier Rank up to k.
• Notice that in prenex normal form the Quantifier Rank of φ is exactly the number of quantifiers appearing in φ.

Example

• The sentence ${\displaystyle \forall _{x}(\exists _{y}((\lnot x=y)\land xRy))\land (\exists _{y}((\lnot x=z)\land zRx))}$ has the Quantifier Rank 2.
• The sentence in prenex normal form ${\displaystyle \forall _{x}\exists _{y}\exists _{y}((\lnot x=y)\land xRy)\land ((\lnot x=z)\land zRx)}$ has the Quantifier Rank 3. Notice that it is equivalent to the above.

...

Theorem

Let ${\displaystyle {\mathfrak {A}}}$ and ${\displaystyle {\mathfrak {B}}}$ be two structures in a relational vocabulary. Then the following are equivalent

• ${\displaystyle {\mathfrak {A}}}$ and ${\displaystyle {\mathfrak {B}}}$ agree on FO[k]
• ${\displaystyle {\mathfrak {A}}\equiv _{k}{\mathfrak {B}}}$

Remark

• The proof is omitted here
• The concept of back and forth relations is not mentioned here, since we do not need it subsequently

The basis for considering expressibility by Ehrenfeucht-Fraisse-Games is given by the following corollary from the above theorem:

Corollary

Let P be a property of finite σ-structures. Then the following are equivalent

• P is not expressible in FO
• for every k ${\displaystyle \in \mathbb {N} }$ there exist two finite σ-structures ${\displaystyle {\mathfrak {A}}_{k}}$ and ${\displaystyle {\mathfrak {B}}_{k}}$, such that the following are both satisfied
  • ${\displaystyle {\mathfrak {A}}_{k}\equiv _{k}{\mathfrak {B}}_{k}}$
  • ${\displaystyle {\mathfrak {A}}_{k}}$ has P and ${\displaystyle {\mathfrak {B}}_{k}}$ does not have P

Example

• To begin pick two linear orders say A ={1, 2, 3, 4} and B ={1, 2, 3, 4, 5}. For a two-move Ehrenfeucht game D is to win, obviously. This gives us two structures that satisfy the above conditions for k = 2 and the Property having even cardinality (that A has and B doesn't). Now we have to expand this over all k ${\displaystyle \in \mathbb {N} }$. From the above example we adopt that in a linear order of cardinality ${\displaystyle 2^{k}}$ or higher D has a winning strategy. Thus we choose the cardinalities depending on k as |A| = ${\displaystyle 2^{k}}$ and |B| = ${\displaystyle 2^{k}}$+1. So we have found an even A and an odd B for every k, where D has a winning strategy. Thus (by the corollary) having even/odd cardinality is a property that can not be expressed in FO for finite σ-structures of linear order.
• Graphs in general are a popular object of interest for FO expressibility. So e.g. it can be shown that the following properties can't be defined in FO:
  • Connectivity
  • Cyclicity
  • Planarity
  • Hamiltonicity
  • n-colorability
  • etc

...