Fix error in problem about duals of characteristic axioms

The biconditionals are not derivable in bare K. I rephrase the claim in
terms of identity of modal systems (seems like the most natural option).

Author: eguindon

content/normal-modal-logic/axioms-systems/duals.tex

@@ -28,9 +28,15 @@
 by~$\Box$. \Ax{D}, i.e., $\Box!A \lif \Diamond!A$ is its own dual in
 that sense.
 
+\begin{prop}\ollabel{prop:dualsys}
+  For each !!{formula}~$!A$ in \olref[nml][prf][dua]{def:duals}:
+  $\Log{K}!A = \Log{K}! A_{\Diamond}$.
+\end{prop}
+\begin{proof}
+  Exercise.
+\end{proof}
 \begin{prob}
-  Show that for each !!{formula}~$!A$ in \olref[nml][prf][dua]{def:duals}:
-  $\Log{K} \Proves !A \liff !A_\Diamond$.
+  Prove \olref[nml][prf][dua]{prop:dualsys}.
 \end{prob}
 
 \end{document}