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

TL;DR

This paper establishes zero-one laws for provability logic, showing that almost all finite models and frames satisfy certain validity properties, and provides axiomatizations for these properties along with complexity results.

Contribution

It proves zero-one laws for provability logic in finite models and frames, and axiomatizes validity in almost all such structures, correcting previous results and analyzing decision complexity.

Findings

Zero-one laws hold for provability logic models and frames.

Two axiomatizations for almost all finite models and frames.

Decidability results for almost sure validity.

Abstract

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. For modal logics, limit behavior for models and frames may differ. 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.