 Provability logic has suitable possible worlds semantics, just like many other modal logics. As a reminder, a possible worlds model (or Kripke model) is a triple \(M = \langle W,R,V \rangle\), where \(W\) is a non-empty set of possible worlds, \(R\) is a binary accessibility relation on \(W\), and \(V\) is a valuation that assigns a truth value to each propositional variable for each world in \(W\). The pair \(F = \langle W,R \rangle\) is called the frame of this model. The notion of truth of a formula \(A\) in a model \(M\) at a world \(W\), notation \(M,w \models A\), is defined inductively. Let us repeat only the most interesting clause, the one for the provability operator \(\Box\):