The modal logic of pure provability (Q749522)

The author considers a provability-type interpretation of modal formulas treating \(\square\) as ``provable in all extensions''. More precisely, let T be a consistent propositional theory extending classical logic (in the same language). For a modal propositional formula \(\phi\), the predicate \(T\vDash_{PP}\phi\) is defined inductively: 1) if \(\phi\) is \(\square\)-free, then \(T\vDash_{PP}\phi\) iff \(T\vdash \phi;\) 2) if \(\phi =\square \psi\) then \(T\vDash_{PP}\phi\) iff \(S\vDash_{PP}\psi\) for any consistent \(S\supseteq T;\) 3) if \(\phi =\eta (\square \psi_ 1,...,\square \psi_ k)\), \(\eta\) being \(\square\)-free, \(\theta_ i=p\vee \neg p\) if \(T\vDash \square \psi_ i\), and \(\theta_ i=p\wedge \neg p\) otherwise, then \(T\vDash_{PP}\phi\) iff \(T\vdash \eta (\theta_ 1,...,\theta_ k).\) The pure provability theory is defined thus: \(PP=\{\phi |\forall T T\vDash_{PP}\phi \}\); this is not a logic in the usual sense because it is not substitution-closed. The author proves completeness of PP w.r.t. a Kripke model, constructs an (infinite) axiomatic system for PP, and gives a deciding procedure. PP differs from arithmetically complete provability logic as well as from non-monotonic systems treating possibility as ``consistency'' [cf. \textit{D. McDermott} and \textit{J. Doyle}, Artif. Intell. 13, 41-72 (1980; Zbl 0435.68074)]. However the author hopes to investigate applications to non-monotonic logics in the future.