 “SQML” is an acronym for “simplest quantified modal logic”, and it is so-called because it is a straightforward amalgam of the most popular and semantically least complicated propositional  modal logic  S5 and  classical first-order logic  (with  identity)—FOL,  for  short.[37]  The deductive system SQML, accordingly, is an amalgam of the corresponding deductive systems S5 and  FOL.[38]  S5 builds on the foundation of classical propositional logic—PL, for short—whose deductive system PL takes every instance of the following schemas as its axioms and Modus Ponens as its inference rule: