Consequentia Mirabilis

Theorem

Consequentia Mirabilis (also known as Clavius's Law) is a particular case of reduction ad absurdum.

It states that:

If, from the negation of a proposition $p \,$ we can derive $p \,$, we can conclude $p \,$.

In symbolic form:

$\neg p \implies p \vdash p$

It can alternatively be rendered as:

$\vdash \left({\neg p \implies p}\right) \implies p$

Proof

Proof using natural deduction:

$\left({\neg p \implies p}\right) \implies p$

Line		Pool	Formula	Rule	Depends upon	Notes
1		1	$\neg p \implies p$	P	(None)
2			$p \lor \neg p$	LEM	(None)
3		3	$\neg p$	A	(None)	Either $p$ is false ...
4		1, 3	$p \,$	$\implies \mathcal E$	1, 3
5		5	$p \,$	A	(None)	... or it's true ...
6		1	$p \,$	$\lor \mathcal E$	2, 3-4, 6-6	... but either way it's true.

$\blacksquare$

Source of name

The name Consequentia Mirabilis is Latin for "marvellous (or admirable) consequence".

The name Clavius's Law (or Clavius' Law) is for Christopher Clavius.

Sources

• Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning (1964): $\text{I}: \S 5$: Theorem $\text{T19}$
• E.J. Lemmon: Beginning Logic (1965): $\S 1.3$: Exercise $1 \ \text{(j)}$