Why is modal logic's S4 Axiom written as '◻A→◻◻A'?

Question

The Stanford Encyclopedia of Philosophy article on modal logic notes that in S4 ◻◻A is equivalent to ◻A and that "any string of boxes may be replaced by a single box".

The article expresses S4: '◻A→◻◻A'?. However, if they're equivalent, wouldn't the axiom be better expressed as a biconditional? If it's the case that any string of boxes may be replaced by a single box (and not expressly vice versa), then wouldn't '◻◻A→◻A' be more accurate?

I assume the author expressed the axiom correctly; it just seems odd to me.

Why is modal logic's S4 axiom written as '◻A→◻◻A'?

Answer 1

Actually $\square A\implies A$ is an axiom of the parent of that family of modal logics including S4, I forget the name. Makes sense, if $A$ is necessarily true then in particular it's true. So $\square A\implies \square \square A$ is equivalent to $\square A\iff \square \square A$ here.

Answer 2

The way that I read the first few paragraphs of that link, besides the axiom S4 saying ◻A→◻◻A, there is already an earlier axiom (M) saying ◻A → A. From (M) it follows by substitution that ◻◻A → ◻A, and combining this with S4 one obtains the biconditional. So it would be redundant to repeat axiom (M) by incorporating it into a "biconditional" version of S4 as you are suggesting.

Answer 3

There is a difference between the axiom 4 and the system S4. The system S4 contains the axioms K, M, 4, and the Necessitation Rule. Technically the axiom D is also a part of S4, but it is an admissible rule/axiom since it is a direct consequence of axiom M.