According to the definitions I have been taught, if a proof system is complete, $\text{If}\ A \Rightarrow B\ \text{then}\ A \vdash B$, and if a proof system is sound, $\text{If}\ A \vdash B\ \text{then}\ A \Rightarrow B$.

Given a proof system that is complete but not sound, let A, B be two propositions. Is it necessarily correct to say that $\text{If}\ A \Rightarrow B\ \text{then}\ A \mkern-2mu\not\mkern2mu\vdash B$ and also $\text{If}\ A \vdash B\ \text{then}\ A \mkern-2mu\not\mkern2mu\Rightarrow B\ $?

My reasoning is as follows:

If the system is not sound then it's not true that $(\text{If}\ A \vdash B\ \text{then}\ A \Rightarrow B)$. Therefore: $$\lnot((A \vdash B) \rightarrow (A \Rightarrow B))$$ $$\lnot(\lnot(A\vdash B) \lor (A \Rightarrow B))$$ $$(A\vdash B) \land \lnot(A \Rightarrow B)$$ $$(A\vdash B)$$ $$(A \mkern-2mu\not\mkern2mu\Rightarrow B)$$

Since $A \Rightarrow B$ is False, it can be the left-hand-side of any implication and make it true. Since $(A\vdash B)$ and $(A \mkern-2mu\not\mkern2mu\Rightarrow B)$, therefore, $\text{If}\ A \vdash B\ \text{then}\ A \mkern-2mu\not\mkern2mu\Rightarrow B$ can be concluded. Is my reasoning correct?

  • 1
    $\begingroup$ Well, obviously it means you can't hear it, so it is more efficient from a thermodynamic point of view, as no energy is dissipated as sound. $\endgroup$
    – Asaf Karagila
    Feb 6, 2020 at 19:44

2 Answers 2


Your basic idea is correct, but you are missing an important bit: There is an implicit universal quantification in the definitions:

Soundness: For all formulas $A, B$, if $A \vdash B$, then $A \Rightarrow B$
Completeness: For all formuas $A, B$, if $A \Rightarrow B$, then $A \vdash B$

So when a proof system is not sound, what is negated is the universality of the implication:

Unsoundness: Not for all formulas $A, B$, if $A \vdash B$, then $A \Rightarrow B$
Incompleteness: Not for all formuas $A, B$, if $A \Rightarrow B$, then $A \vdash B$

This is in turn equivalent to an existential negated statement:

Unsoundness: There exist formulas $A, B$ such that not if $A \vdash B$, then $A \Rightarrow B$
Incompleteness: There exist formuas $A, B$ such that not if $A \Rightarrow B$, then $A \vdash B$

And this is in turn equivalent ot the following:

Unsoundness: There exist formulas $A, B$ such that $A \vdash B$ but not $A \Rightarrow B$
Inompleteness: There exist formuas $A, B$ such that $A \Rightarrow B$ but not $A \vdash B$

So if a proof system is unsound, then some of the proofs it produces are not semantically valid. It doesn't have to be per se that everything it proves is nonsense.
This may be even more convincing on the incompleteness side: The word "incomplete" just means that some sequents are missing from the proof system; it doesn't have to be that that it fails to prove all sequents whatsoever.

If a proof sytem is unsound and complete, then all the semantically valid inferences can be proven, but in addition it proves some sequents that are not actually valid.

Edit (changing my last pargraph thanks to Malice Vendrine's comment):
Note also that those provable but invalid sequents do not have to be contradictory: It might just be that they are not true in all structures. For example, a system that proves $\vdash A \lor B \to A$ would be unsound, because this inference is not universally valid. But neither is its negation (there may well be structures in which the formula is satisfied, for example, in any structure in which $A$ is true).
So proving non-valid formulas does not immediately lead to an inconsistency. Only if we can prove the negation of a formula that is valid (and hence, by completeness, also provable) or, vice versa, a formula whose negation is valid, unsoundness in combination with completeness makes the system inconsistent.

  • 3
    $\begingroup$ Don't we have to be a little careful about this last point regarding inconsistency? For example, any formula true in every Heyting valued model is provable in classical first order logic, but obviously there are theorems of classical logic that are not intuitionistically valid; with respect to Heyting semantics, we have completeness and not soundness. Failure of soundness says that there is a provable formula that is not true in every model; it doesn't necessarily follow that its negation is true in every model, right? $\endgroup$ Feb 6, 2020 at 20:04
  • 2
    $\begingroup$ @Malice Vidrine You are right. Thanks for pointing it out; I changed that paragraph. $\endgroup$ Feb 6, 2020 at 23:34

Since $(A\vdash B)$ and $(A \mkern-2mu\not\mkern2mu\Rightarrow B)$, therefore, $\text{If}\ A \vdash B\ \text{then}\ A \mkern-2mu\not\mkern2mu\Rightarrow B$ can be concluded.

Careful! If you are trying to say that this "If $A \vdash B$, then $A \not \Rightarrow B$" holds for any $A$ and $B$, then you are clearly mistaken. For example, we have that $A \vdash A$, but we also have that $A \Rightarrow A$

Indeed, since soundness means that for every $A$ and $B$ we have that "If $A \vdash B$, then $A \Rightarrow B$", the system being unsound means that we don't have "If $A \vdash B$, then $A \Rightarrow B$" for some $A$ and $B$.

OK, so should we say that we can conclude that for some $A$ and $B$, we have "If $A \vdash B$, then $A \not \Rightarrow B$"?

Well, technically, that is true ... but it is not very interesting at all! Note that $A \not \Rightarrow \neg A$, and since any conditional is trivially true as soon as its consequent is true, you'd immediately have that "If $A \vdash \neg A$, then $A \not \Rightarrow \neg A$", and thus that we have "If $A \vdash B$, then $A \not \Rightarrow B$" for some $A$ and $B$. So note that the latter is true also for systems that are perfectly sound!

Indeed, the much stronger and more interesting claim would be to say that for some $A$ and $B$, we have both $A \vdash B$ and $A \not \Rightarrow B$: that is the characteristic feature of an unsound system.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .