# How can a proof system be unsound?

I have recently started learning propositional logic. I stumbled upon the concepts of soundness and completeness.

According to http://intrologic.stanford.edu/chapters/chapter_04.html, a proof system is sound if and only if every provable conclusion is logically entailed (if Δ ⊢ Φ, then Δ ⊨ Φ); a proof system is complete if and only if every logical conclusion is provable (if Δ ⊨ Φ, then Δ ⊢ Φ).

I can see examples of incomplete proof systems. The same document referred to the Mendelson system. Because the Mendelson system fails to use operators other than negations and implications, it cannot be complete for a propositional language.

I fail to see how a proof system can be unsound. Are there any common examples of unsound proof systems? Furthermore, what effects arise from the fact that a proof system is unsound?

• I suspect this has something to do with the rules; so if we are working with classical logic, and in addition to all the usual natural deduction rules, we have the classic Tonk rule, which has the intro of a disjunction but the elim of a conjunction, then we can pretty much prove anything with Tonk. en.wikipedia.org/wiki/Logical_harmony – Daniel Mak Aug 9 '20 at 10:42
• So for example, given a single premise P, I can use disjunction intro/Tonk intro to get P(Tonk)¬P, and use conjunction elim/Tonk elim to get ¬P. This is obviously not true given a classical logic system. – Daniel Mak Aug 9 '20 at 10:44
• So to go back to your question, a classical logic proof system with the Tonk rule is definitely not sound. In addition, we can also prove anything with it. This will trivialise our logic because while we can prove everything, the proof system does not give us anything useful. – Daniel Mak Aug 9 '20 at 10:48

Soundness

If Δ ⊢ Φ, then Δ ⊨ Φ

has an implicit universal quantification to it:

For all Δ, Φ: if Δ ⊢ Φ, then Δ ⊨ Φ

Unsoundness of a proof system then means

Not for all Δ, Φ: if Δ ⊢ Φ, then Δ ⊨ Φ

This is equivalent to

There exist Δ, Φ such that not: if Δ ⊢ Φ, then Δ ⊨ Φ

which is in turn equivalent to

There exist Δ, Φ such that Δ ⊢ Φ but not Δ ⊨ Φ

That is, an unsound proof system produces proofs for inferences that are not actually valid. Of course, this makes the proof system rather useless, since you want a proof system as a device to show that an inference holds, but in an unsound proof system the situation is precisely that you do not have the guarantee that the proved inference actually holds.

Since unsound proof systems are not very useful, you won't commonly run into them when studying logic. I don't know off the top of my mind of any real-life example, but of course, it can well happen (and most likely has happend throughout history) that the developer of the proof system had the intention of a sound proof system but made a mistake in the design of the rules and had them not adequately reflect the semantics, so that it later turned out to actually be unsound (and didn't make it to popularity for that reason).

And of course, it is easily possible to just ad hoc define some random nonsensical proof system on purpose, e.g., by inventing a rule that says

``````A
--
¬A
``````

or the like. Any proof system with such a rule included will be unsound because obviously A ⊭ ¬A. Note that this again encompasses an implicit universal quantification: Adding this rule results in A ⊢ ¬A for all formulas A, while we do not have for all formulas that A ⊨ ¬A, which is why the rule is unsound; though there may be some formula instances for which the inference does hold (e.g. with A = ⊥). And of course, the proof system may well encompass other rules that are sound and produce proofs for inferences that hold for any instance of formulas. So unsoundness doesn't automatically mean that all of its proofs are wrong.

Neither does it mean that it proves any contradictory formulas. A formula being valid means that it is true in all structures; if a proof system proves, say, ⊢ A v B --> A, it is unsound because A v B --> A is not valid, i.e. not true in all structures. But neither is it contradictory; there do exist structures and instances of A and B in which A v B --> A does hold (e.g. any structure in which A is true).

And unsoundness doesn't automatically make the proof system inconsistent: A proof system is insoncistent iff it proves both A and ¬A for some formula A, that is, if it proves a contradiction. Suppose A is valid (hence ¬A is contradictory), and the proof system proves ¬A but not A. Then the proof system is unsound, because with ¬A it proves a formula that not actually valid, but it is not inconsistent, because it doesn't prove A which would be necessary to derive a contradiction.

For the combination complete + unsound, see also here: What is true about a proof system that is complete but not sound?

TL;DR:
Unsoundness means that the system proves inferences that aren't actually valid, i.e. there exist sequents Δ ⊢ Φ for which Δ ⊭ Φ (= there exist structures in which all formulas in Δ are true but Φ is false).
Unsoundness makes a proof system somewhat pointless and will usually only happen by accident or for demonstrative purposes.

• Good summary, but unsound systems can be useful when they offer a technical convenience for precision tradeoff. Even classical logic is, strictly speaking, unsound as judged against "natural reasoning". Many modal logics are intentionally unsound, and it is roughly known where they go wrong, but technical benefits are worth it. – Conifold Aug 10 '20 at 4:52
• @Conifold Do you just mean that standard logic doesn't always match our intuitions, or are there actually common syntactic proof systems that are unsound w.r.t. the underlying formal semantics? In that case, I'd be interested in some reading pointers. – lemontree Aug 10 '20 at 10:56
• The former, but it doesn't have to be intuitions, the effect is the same if we compare it to formal intuitionistic or relevance semantics. The usual procedure (a la Kripke) of designing semantics to match the formalism pretty much makes "soundness" a given, but that is the kind of soundness that does not add usefulness to what is already there. – Conifold Aug 10 '20 at 20:50