I've heard before that classical propositional logic is Post-complete, for example, see this answer.
This means that given a set of axioms and inference rules $(A, I)$ for classical propositional logic, for any well-formed formula $\alpha$ such that $A \not\vdash_I \alpha$, it holds for all propositions $\varphi$ that $A, \alpha \vdash_I \varphi$. Let's call the latter system one-valued logic.
The modal logic $\mathsf{S5}$ seems to have a similar property to classical logic here. Asserting any additional well-formed formula $\alpha$ as an axiom gives us back $\mathsf{S5}$ or one-valued logic or classical logic with modal operators being interpreted as identity functions.
My question is severalfold:
- What is the name for this maximality property that $\mathsf{S5}$ has?
- How do we prove that it has it (if indeed it does have property (1))?
The logic S5 does not have this property, see e.g. this paper. To see this for yourself, try to find a formula which is not valid in S5 but which is valid in the two-element S5 frame. On the other hand, the logic of this two-element frame does have the property you are looking for (because each normal extension of S5 is complete with respect to some class of finite frames and each S5 frame with at least two elements has the two-element S5 frame as a p-morphic image).
A logic which has no non-trivial proper extension is usually called a maximal logic. I don't think that the property that a logic has no non-trivial proper extension other than classical logic has a standard name, but it makes sense to call it a maximal subclassical logic (a subclassical logic being one contained in classical logic).