Zero-one laws for provability logic: Axiomatizing validity in almost all\n models and almost all frames

It has been shown in the late 1960s that each formula of first-order logic\nwithout constants and function symbols obeys a zero-one law: As the number of\nelements of finite models increases, every formula holds either in almost all\nor in almost no models of that size. Therefore, many properties of models, such\nas having an even number of elements, cannot be expressed in the language of\nfirst-order logic. For modal logics, limit behavior for models and frames may\ndiffer. Halpern and Kapron proved zero-one laws for classes of models\ncorresponding to the modal logics K, T, S4, and S5.\n In this paper, we prove zero-one laws for provability logic with respect to\nboth model and frame validity. Moreover, we axiomatize validity in almost all\nrelevant finite models and in almost all relevant finite frames, leading to two\ndifferent axiom systems. In the proofs, we use a combinatorial result by\nKleitman and Rothschild about the structure of almost all finite partial\norders. On the way, we also show that a previous result by Halpern and Kapron\nabout the axiomatization of almost sure frame validity for S4 is not correct.\nFinally, we consider the complexity of deciding whether a given formula is\nalmost surely valid in the relevant finite models and frames.\n