# 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:

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.

• What do you mean by "sound", "strongly sound" and "strongly complete"? Jun 28, 2021 at 18:12
• 1. sound/soundness - if $\vdash \varphi$ then $\models \varphi$ 2. strong soundness - if $\Sigma \vdash \varphi$ then $\Sigma \models \varphi$ where $\Sigma$ is a set of propositions 3. strongly completeness - if $\models \varphi$ then $\vdash \varphi$ Jun 28, 2021 at 18:28
• What are the axioms and the other inference rules in your Hilbert system? Jun 28, 2021 at 18:45
• there are no other inference rules, the axioms are the same as the Hilbert system i.e $$(\varphi\rightarrow (\psi\rightarrow\varphi))$$ $$(\varphi\rightarrow (\psi\rightarrow\theta))\rightarrow ((\varphi \rightarrow \psi ) \rightarrow (\varphi\rightarrow\theta))$$ $$(\neg\psi\rightarrow\neg\varphi )\rightarrow (\varphi\rightarrow\psi)$$ Jun 28, 2021 at 19:08

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.

• but what if $\vdash_D (\neg a \rightarrow b)$ and $\vdash_D (\neg a \rightarrow \neg b)$ then $\vdash_D a$? can you prove that there isn't proposition $b$ such that $\vdash_D (\neg ((( X \rightarrow Y) \rightarrow X) \rightarrow X) \rightarrow b)$ and $\vdash_D (\neg ((( X \rightarrow Y) \rightarrow X) \rightarrow X) \rightarrow \neg b)$ and therefore $\nvdash_D (( X \rightarrow Y) \rightarrow X) \rightarrow X$? Jun 28, 2021 at 22:02
• @CforLinux - In system $D$, from $\lnot a \to b$ and $\lnot a \to \lnot b$ you can only deduce $\lnot \lnot a$, which is different from $a$. And in system $D$ there is no rule to derive $a$ from $\lnot \lnot a$. Jun 28, 2021 at 22:17
• Not sure I understand, isn't $\neg\neg a\equiv a$? Therefore $a$ is proven? Jun 28, 2021 at 23:23
• @CforLinux - Yes, $\lnot \lnot \varphi$ and $\varphi$ are logically equivalent (i.e. $\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 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$. Jun 29, 2021 at 4:39

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

• What is $\top$? There are no axioms for it. If you want to use $\top$ as a constant for "always true", you need to add some axioms and so the system won't be $D$ anymore. Jun 29, 2021 at 8:35
• $\top$ a semantic concept, it doesn't need axioms. Jun 29, 2021 at 15:46