The Modal Logic of the Countable Random Frame

Valentin Goranko & Bruce Kapron

One of the major attractions in finite model theory is the study of asymptotic probabilities, 0-1 laws, and almost surely validity of properties of random finite structures, formalizable in various logical languages (see surveys [1], [2], and [3]).

An important problem in the area is to give a logical characterization of the almost sure validity in the finite, i.e. of those formulas which are valid with asymptotic probability 1 in a randomly chosen finite structure. However, this is not a priori logically tractable concept, as it lacks explicit logical semantics in terms of particular models, but rather involves the class of all finite models as a whole. Usually such characterizations are associated with the countable random structure of the We study the modal logic ML^{r} of the countable random frame which is contained in the modal logic of almost sure frame validity.

We give a sound and complete axiomatization of ML^{r} and show that it is not finitely axiomatizable. Then we describe the finite frames of that logic and show that it has the finite frame property and its satisfiability problem is in EXPSPACE. Finally, we show that there are modal formulas which are almost surely valid in the finite, yet fail in the countable random frame, and hence do not follow from the extension axioms.

[1] K. J. Compton, 0-1 laws in logic and combinatorics, in: NATO Adv. Study Inst. on Algorithms and Order, I. Rival (ed.), Reidel, 1988, 353–383.

[2] Y. Gurevich, Zero-One Laws: The Logic in Computer Science Column, Bulletin of the European Association for Theoretical Computer Science, 1992, 90-106.

[3] Ph. G. Kolaitis and M. Y. Vardi, 0-1 Laws for Fragments of Second-Order Logic: an overview, In: Y. Moschovakis (ed.), Logic for Computer Science, Proc. of workshop in 1989, 265-286.

Addresses Valentin Goranko: Department of Mathematics, Rand Afrikaans University, PO Box 524, Auckland Park 2006, Johannesburg, South Africa

E-mail: vfg@na.rau.ac.za

Bruce Kapron: Department of Computer Science, University of Victoria, Victoria, BC, V8W 3P6 Canada

E-mail: bmkapron@csr.uvic.ca