Finite Model Theory/FO EFG

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

Logic and Games[edit]

Connection between Games and logical Quantifiers...

Simple Games[edit]

  1. S chooses first all n from one/both side(s), then D chooses all
  2. one match as in 1. for every i = 1 ... n where the i'th choice must include the i-1'th.

Definition[edit]

Ehrenfeucht-Fraisse-Game (EFG)

Let \mathfrak{A} and \mathfrak{B} be finite relational structures, with the same set of relation symbols, and n be a fixed natural number.

A game is said to be an Ehrenfeucht-Fraisse-game iff it is constituted the following way

  • 2 Players: Spoiler S and Duplicator D
  • Game tree:
    • Root: a pair of empty sequences
    • Branch:
      • Move of S: S chooses exactly one element of either A or B that has not been chosen already (latter is not relevant in the first move)
      • Move of D: D chooses exactly one element of the remaining set that has not been chosen already, i.e. if S has chosen from A D has to choose from B and if S chose one from B D has to choose from A.
    • Terminator: The game is finished iff α and β are of size n.
  • Turn: Moves are carried out alternatingly, S is to move first.
  • Payoff: D wins iff the final position defines a partial isomorphism by mapping the i-th elements of α and β, for all i. Else S wins
  • Information: the players are assumed to have perfect information