strong completeness of a formal system Given a formal system $D$ where the axioms are the same as in Hilbert system for propositional logic and the inference rule is $$\frac{a\rightarrow b, \quad a\rightarrow \neg b}{\neg a}$$ I need to answer:

*

*Is the system sound (if $\vdash_D \varphi$ then $\models \varphi$)?

*Is the system strongly sound (if $\Sigma\vdash_D \varphi$ then $\Sigma\models \varphi$ for every $\Sigma$ set of propositions)?

*Is the system strongly complete (if $\models \varphi$ then $\vdash_D \varphi$)?

I managed to answer questions 1 & 2, but I can't find an answer for 3, neither prove strong completeness nor find a counterexample.
 A: 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.
A: 
$$ \frac{a\rightarrow b, \quad a\rightarrow \neg b}{\neg a}$$

This axiom doesn't prevent defining $\lnot X = \top$ .  So you won't be able to prove any theorem that distinguishes $\top$ from $\lnot$.  For example,
$$P \to \lnot P \to Q$$
holds under the intended meaning of $\lnot$, but $P \to \top \to Q$ is not going to be provable from sound axioms.

Another way of putting it is that any theorem provable from the given axioms will also be soundly true when any expression $\lnot X$ is replaced by $\top$ (true).  So any tautology, which is not a tautology after a replacement, will not be provable.
