INFINITARY LOGIC FOR COMPUTER-SCIENCE

Infinitary logic L(infinityomega) extends first-order logic by allowing infinitary conjunctions and disjunctions (i.e., conjunctions with an infinite number of conjuncts and disjunctions with an infinite number of disjuncts). One usually thinks of infinitary logic as a fairly esoteric logic, which is not of much interest in computer science. Surprisingly, a certain fragment L(infinityomega)omega of L(infinityomega) turns out to be of great interest in computer science. This fragment is obtained by restricting formulas to contain a finite number of distinct variables, though the formulas can be of infinite length, The advantage of dealing with L(infinityomega)omega is that its the expressive power can be completely characterized in game-theoretic terms. We will describe applications of this logic to the study of 0-1 laws and the expressive power of database query languages.