strong completeness of a formal system

Question

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:

1. Is the system sound (if $\vdash_D \varphi$ then $\models \varphi$)?
2. Is the system strongly sound (if $\Sigma\vdash_D \varphi$ then $\Sigma\models \varphi$ for every $\Sigma$ set of propositions)?
3. 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.

Answer 1

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.

Answer 2

$$ \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.