S5 (modal logic)

It is formed with propositional calculus formulas and tautologies, and inference apparatus with substitution and modus ponens, but extending the syntax with the modal operator necessarily

Determining the satisfiability of an S5 formula is an NP-complete problem.

The hardness proof is trivial, as S5 includes the propositional logic.

While this is useful for keeping propositions reasonably short, it also might appear counter-intuitive in that, under S5, if something is possibly necessary, then it is necessary.

Alvin Plantinga has argued that this feature of S5 is not, in fact, counter-intuitive.

[4] Leibniz proposed an ontological argument for the existence of God using this axiom.

[5] S5 is also the modal system for the metaphysics of saint Thomas Aquinas and in particular for the Five Ways.

[6] However, these applications require that each operator is in a serial arrangement of a single modality.

This aligns with the intuition that proposing a certain necessary entity does not mean it is real.