A minimal fragment of LTL [ltp-000W]

All of the connectives linear-time temporal logic can be constructed from the following minimal fragment (among others:)

\begin {array}{lcl} \varphi , \psi &::=& \top \mid \mathsf {a} \mid \varphi \land \psi \mid \neg \varphi \mid \mathop {\raisebox {-0.2em}{\text {\Large ○}}} \varphi \mid \varphi \mathbin {\mathcal {U}} \psi \end {array}

The remaining connectives can be derived by using the following identities:

• \bot \equiv \neg \top
• \varphi \lor \psi \equiv \neg (\neg \varphi \land \neg \psi )
• \mathop {\raisebox {-0.2em}{\text {\Large ◇}}} \varphi \equiv \top \mathbin {\mathcal {U}} \varphi
• \mathop {\raisebox {-0.1em}{\text {\Large □}}} \varphi \equiv \neg \mathop {\raisebox {-0.2em}{\text {\Large ◇}}} \neg \varphi
• \varphi \mathbin {\mathcal {R}} \psi \equiv \neg (\neg \varphi \mathbin {\mathcal {U}} \neg \psi )

(where \varphi \equiv \psi means \llbracket \varphi \rrbracket = \llbracket \psi \rrbracket )