Supplement: Burgess’ Axiomatic System for PBTL

Burgess’ (1980) axiomatic system for PBTL extends classical propositional logic by

• the familiar axiom schemata $(K_H)$ and $(K_G)$ (see Section 3.5), as well as $G(\varphi \rightarrow \psi)\rightarrow (F\varphi \rightarrow F\psi),$
• the axiom schemata (GP) and the Peircean variant of (HF) (cf. Section 3.5): $\varphi \rightarrow H\neg G\neg\varphi,$
• the axiom schemata (NOBEG) and Peircean versions of (NOEND) (cf. Section 3.6): $G\varphi \rightarrow F\varphi$ and $G\varphi \rightarrow \neg F\neg\varphi,$
• the axiom scheme (TRANS) for H, G, and F (cf. Section 3.6),
• the axiom schemata $H\varphi \rightarrow (\varphi \rightarrow (G\varphi \rightarrow GHp))$ and $H\varphi \rightarrow (\varphi \rightarrow (\neg F\neg\varphi \rightarrow \neg F\neg Hp)),$ and
• the axiom scheme $FG\varphi \rightarrow GF\varphi.$

The inference rules comprise, in addition to (MP), (NEC$_H$), and (NEC$_G$) (see Section 3.5),

• a version of the so-called Gabbay Irreflexivity Rule: If $\vdash H\neg\varphi \rightarrow (\neg\varphi \rightarrow (G\varphi \rightarrow \psi)),$ then $\vdash \psi,$ provided $\varphi$ does not occur in $\psi$.