[A reflection on Richmond Thomason’s “Independence of the Dual Axiom in Modal K with Primitive ◊”]
Within modal logic we customarily take necessary to be equivalent to not possibly not. Thomason shows that the answer to my title question is NO: if we formulate the logic with ◊ as primitive, we need to add that equivalence as an axiom. There is an interpretation of K in which the duality fails. The interpretation, he says, is exotic …. It is, but also startling and provocative.
I’ll explain his model and reasoning, and then explore his method with a smaller model (which gives a weaker result). His method: construction of a small language that is classical (truth-functional connectives) and hyper-intensional.
In Thomason’s paper the family of propositions is represented by the union B ∪ B’ of two Boolean algebras with two atoms each:

The partial order within this union is just within each of the parts: if x and y belong to B and B’ they are not ordered relative to each other, they have no meet or join. Think of this as a matrix, with only V and V’ designated values (‘true’).
There is a sort of complement operator, which I will symbolize as ¬, that is ordinary in B but takes elements in B’ to B.
As a result, of course, ¬¬ x is always in B, and is called Twin(x). Specifically, ¬1 = 2, ¬2 = 1. But ¬ 2’ = 1 as well, so Twin(2’) = ¬ ¬ 2’ = 2. Similarly, ¬1’ = 2, so Twin(1’) = 1.
Then there is sort of conditional operator (x → y) = (¬Twin(x) v Twin(y)); its values are always in B. Thus when sentences are given these propositions as their semantic values, and “not” and “if then” are assigned ¬ and →, classical propositional logic is sound.
Clearly ¬ is not an involution on B ∪ B’, but like in Intuitionistic logic, doubly complimented propositions act classically.
So, as far as that is concerned, the strange algebraic structure of the family of propositions is hidden from sight. But that strangeness can be utilized in the interpretation of ◊.

That interpretation is simple: each of B and B’ is divided into ‘possible’ and ‘impossible’ regions: the ‘possible’ propositions are those inside the dotted ellipses.
The possibility operator, too, when applied to an element of B’, shifts attention to B:
◊1 = V, ◊V = V, but if x is in B’, we still refer to V in B: ◊2’ = V, ◊V’ = V. In all other cases ◊x= ∧. Notice that for all x, ◊x is in B, so this addition cannot affect the soundness of classical sentential logic.
With this interpretation we can verify the K axiom formulated with ◊ as primitive:
¬ ◊¬ (x → y) → [¬◊¬x → ¬◊¬y]
To check that no assignment of values to x, y yields a counterexample is straightforward.
What has happened to duality? If we define □ x as ~◊~x, what is the status of
Duality. ◊x → ~□~x, and ~□~x → ◊x ?
The first part is the same as ◊x → ~~◊~~x, which is the same as ◊x → ◊~~x. If x = 2’ then this is (◊2’ → ◊~~2’), which is (V → 2) = 2, hence not true.
The second part is similarly seen not to be true, using 1’ rather than 2’.
Adding Duality as an axiom will eliminate the ‘exotic’ interpretation.
PART TWO.
Thomason’s method has a general form:
choose a structure and interpretation in such a way that all the semantic values of complex sentences belong to a Boolean algebra, and use extra structure in the interpretation of non-Boolean operators.
That makes it possible to construct non-standard interpretations of even normal modal logics.
I thought I’d try my hand it with a small familiar lattice that has a Boolean sublattice. As it turns out (not surprisingly) it (only) gets half of Thomason’s result.

This is N5, the smallest non-modular (hence non-distributive) lattice, the ‘pentagon lattice’. Let us define operations on it in the way Thomason did:
a sort of complement: ┐1 = ⎯ 1, ┐ ⎯ 1 = 1, ┐k = ⎯ 1, ┐T = ⊥, ┐⊥ = T.
We define the Twin x* of x to be ┐┐x. Note that k* = 1.
N5 has a Boolean sublattice B = {T, 1, ⎯ 1, ⊥} = {x*: x in N5}
a sort of conditional: (x → y) = (┐x* v y*)
Only T is designated (‘true’). Interpretation of the syntax: as above; once again all semantic values of complex sentences are located in the Boolean sublattice, so classical sentential logic theorems are all true.
a sort of possibility operator: ◊x = T iff x = 1 or T; ◊x = ⊥ otherwise.
Verification of the K axiom
¬ ◊¬ (x → y) → [¬ ◊¬x → ¬◊¬y]
Note:
¬◊¬T = T, ¬◊¬1 = T
¬ ◊¬k = ¬◊(⎯ 1) = T ¬◊¬(⎯ 1) = ¬◊1 = ⊥
¬◊¬ ⊥ = ⊥
For the consequent of the K axiom to be ⊥ means that [◊¬x v ¬◊¬y] = ⊥, so:
x is k or T or 1, and y is (⎯1) or ⊥
In these cases the antecedent is ¬◊¬ followed by:
(k → ⎯ 1) = (¬k* v ⎯ 1) = ⎯ 1
(k → ⊥) = (¬k* v ⊥) = ⎯ 1
(T→ ⎯ 1) = ⎯ 1
(T → ⊥ ) = ⊥
(1 → ⎯ 1) = ⎯ 1
(1 → ⊥ ) = ⎯ 1
and the result of prefixing ¬◊¬ is in each case ⊥. So any attempt at a counterexample fails.
Now for the duality axiom:
Duality. ◊x → ¬¬□~x, and ¬□¬x → ◊x
The second part is the same as ¬¬◊¬¬x→ ◊x, which is the same as ◊¬¬x → ◊x. But (◊¬¬k → ◊k) = (◊1 →◊k) = (T → ⊥) = ⊥.
However, the converse holds, so only half of Duality is refuted.
PART THREE. How can we generalize this method?
Note that in the above, for all x, ¬x = ¬¬¬x = ¬Twin(x). So the mapping of B’ into B does not need to be defined in terms of ¬.
So we can simply say: we have a map Twin, and we define ¬ and → to be as usual on B, and for x, y in B’ we define (x → y) = (Twin(x) → Twin(y)), and define ¬x = ¬Twin(x).
For x in B, set Twin(x) = x to make it a map of the entire structure into itself.
So that is one map, then choose another map of the structure into itself, call it α , whose values are all in B. (That is necessary to make sure that classical propositional theorems remains valid.) Any other properties you like.
Now you have a model of a classical sentential calculus extended with addition of a single unitary propositional operator, which will satisfy any axioms of your desire.
For example, thinking about the K□ axiom for α, you could specify that if x ≤ y then Twin(x) ≤ Twin(y). But you could do the opposite, so that if p implied q then αq would imply αp, acting like negation (but perhaps not just like negation). Or you could want α to be read “It is so in the story that …” and the story could be by Graham Priest.
Remark: hyper-intentionality
It is remarkable that by such simple means Thomason created a language that is at once classical and hyperintensional:
Hyper-intensionality. For all x in B and in B’, x → ¬ ¬x and ¬¬x → x. But it is not the case that ◊x → ◊¬ ¬x. For example, ◊2’ = V but ◊¬ ¬2’ = ◊2 = ⊥.
Note that if x is in B then so is ¬ ¬x. For how Thomason interprets the language, we can add that if A is any complex sentence then ◊A will imply ◊¬ ¬A. Only by using an atomic sentence (with value in B’) there is a counterexample to Duality.
In the case of axiom ¬ ◊¬ (A → B) → [¬◊¬A → ¬◊¬B], the ◊ operator is applied only to sentences that begin with ¬, hence are complex. So no such way of providing counter-examples applies there.
The created language, at once classical and hyper-intensional, is intriguingly unusual!
REFERENCE
Thomason, Richmond (2018) “Independence of the Dual Axiom in Modal K with Primitive ◊”. Notre Dame Journal of Formal Logic 59: 381-385.