Sylvester Kollin: Probabilistic Provability Logic

Abstract.

This essay introduces a novel probabilistic generalisation of propositional modal logic, with its language including a modal operator \(\Box_{\ge r}\). The standard relational semantics is generalised by, roughly, replacing deterministic valuations with probability measures, where \(\Box_{\ge r}A\) is true if and only if \(A\) is assigned a probability of at least \(r\) at all possible states of affairs. Three systems of modal logic are generalised in this setting: the minimal K, K4, which extends K, and Gödel-Löb provability logic, GL. It is proven that these generalisations are all sound relative to certain classes of probabilistic models. Inspired by how GL and related systems are suitable for reasoning about provability within sufficiently strong first-order theories, this novel development is motivated by a notion of probabilistic provability.