No, the system $D$ is not strongly complete. Indeed, consider the formula $((X \to Y) \to X) \to X$ where $X$ and $Y$ are propositional variables.
It is immediate to verify that $\models ((X \to Y) \to X) \to X$ by means of a truth table: for every truth assignment to $X$ and $Y$, the formula $((X \to Y) \to X) \to X$ turns out to be true.
However $\not\vdash_D ((X \to Y) \to X) \to X$ for the following reason:
- the formula $((X \to Y) \to X) \to X$ is not an instance of any axiom of system $D$, and
- the formula $((X \to Y) \to X) \to X$ cannot be derived by applying the only inference rule in system $D$, because any conclusion of such a rule has the form $\lnot \varphi$, which is not the form of the formula $((X \to Y) \to X) \to X$.
The formal argument to answer question 3 is what I wrote above. Here I give an informal explanation, which contextualizes the answer.
Intuitively, the idea is that the only inference rule in system $D$ does not allow the number of $\lnot$ to decrease, when reading it top-down: if $\psi$ is a formula in one of the two premises in the only inference rule of system $D$, and $\varphi$ is its conclusion, then the number of $\lnot$ occurring in $\varphi$ cannot be less than the number of $\lnot$ occurring in $\psi$.
Therefore, the fact that $ \vdash_D \lnot \lnot \varphi$ (i.e. $\lnot \lnot \varphi$ is provable in system $D$) does not imply that $\vdash_D \varphi$. This fact could seem counterintuitive because $\varphi$ and $\lnot \lnot \varphi$ are logically equivalent, that is, they have the same truth table (formally, $\models \lnot \lnot \varphi$ if and only if $\models \varphi$). Logical equivalence is a semantic notion, while provability $\vdash_D$ is a syntactic notion: the only means you have to conclude that $\vdash_D \varphi$ are the axioms and the only inference rule of system $D$. It does not matter if $\lnot \lnot \varphi$ is logically equivalent to $\varphi$, in system $D$ you do not have any rule that allows you to go from $\lnot\lnot \varphi$ to $\varphi$.
If system $D$ were strongly complete (and sound), then you could freely interchange $\models$ (semantic validity) with $\vdash_D$ (syntactic provability in system $D$), and so you could say that, since $\lnot \lnot \varphi$ is logically equivalent to $\varphi$, the fact that $\vdash_D \lnot \lnot \varphi$ (i.e. $\lnot\lnot \varphi$ is provable in system $D$) would imply that $\vdash_D \varphi$. But in fact system $D$ is not strongly complete, and so $\models$ and $\vdash_D$ cannot be freely interchanged.
