An Ehrenfeucht-Fraisse Game for the Logic L-omega1-omega
Tong Wang
Abstract:
The Ehrenfeucht-Fraïssé Game is very useful in studying separation and
equivalence results in logic. The usual finite Ehrenfeucht-Fraïssé
Game EFn characterizes separation in first order logic Lωω. The
infinite Ehrenfeucht-Fraïssé Game EFω and the Dynamic
Ehrenfeucht-Fraïssé Game EFDα characterize separation in L∞ω, the
logic with arbitrary conjunctions and disjunctions of formulas. The
logic Lω1 ω is the extension of first order logic with countable
conjunctions and disjunctions of formulas. It is the most immediate,
and perhaps the most important infinitary logic. However, there is no
Ehrenfeucht-Fraïssé Game in the literature that characterizes
separation in Lω1ω.
In this thesis we introduce an Ehrenfeucht-Fraïssé Game for the logic
Lω1ω . This game is based on a game for propositional and first
order logic introduced by Hella and Väänänen. Unlike the usual
Ehrenfeucht-Fraïssé Games which are modeled solely after the behavior
of quantifiers, this new game also takes into account the behavior of
boolean connectives in logic. We prove the adequacy theorem for this
game. In the final part of the thesis we apply this game to prove
complexity results about infinite binary strings.