The system FS, named after Friedman and Sheard (1987), retains the negation axiom \(\forall{\scriptsize A}(T[\neg{\scriptsize A}] \leftrightarrow \neg T{\scriptsize A})\). The further compositional axioms are obtained by lifting the type restriction to their untyped counterparts: