 The inference rules involve only the classical modus ponens and the necessitation rule for \(G\). In technical terms, the axiom (FP\(_{G}\)) says that \(G\varphi\) is a fixed point of the operator \(\Gamma_{G}\) defined by \(\Gamma_{G} (\theta) = \varphi \land X\theta,\) whereas (GFP\(_{G}\)) says that \(G\varphi\) is (set-theoretically, in terms of its extensions) a greatest post-fixed point of \(\Gamma_{G}.\) Likewise, the axiom (FP\(_{U}\)) says that \(\varphi U\psi\) is a fixed point of the operator \(\Gamma_{U}\) defined by \(\Gamma_{U}(\theta) = \psi \lor (\varphi \land X\theta),\) whereas (LFP\(_{U}\)) says that \(\varphi U\psi\) is a least pre-fixed point of \(\Gamma_{U}\). Some variations of this axiomatic system are  presented in the supplementary document: