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'?