  It has been shown in the late 1960s that each formula of first-order logic
without constants and function symbols obeys a zero-one law: As the number of
elements of finite models increases, every formula holds either in almost all
or in almost no models of that size. Therefore, many properties of models, such
as having an even number of elements, cannot be expressed in the language of
first-order logic. Halpern and Kapron proved zero-one laws for classes of
models corresponding to the modal logics K, T, S4, and S5.
  In this paper, we prove zero-one laws for provability logic with respect to
both model and frame validity. Moreover, we axiomatize validity in almost all
relevant finite models and in almost all relevant finite frames, leading to two
different axiom systems. In the proofs, we use a combinatorial result by
Kleitman and Rothschild about the structure of almost all finite partial
orders. On the way, we also show that a previous result by Halpern and Kapron
about the axiomatization of almost sure frame validity for S4 is not correct.
Finally, we consider the complexity of deciding whether a given formula is
almost surely valid in the relevant finite models and frames.
