Law of Clavius states $ \sim P \Rightarrow P \vdash P$

And the only explanation I sort of understand is

"If we ought to philosophise, then we ought to philosophise; and if we ought not to philosophise, then we ought to philosophise (i.e. in order to justify this view); in any case, therefore, we ought to philosophise."

which to me reads as $(P \Rightarrow P)\wedge (\sim P \Rightarrow P ) \vdash P $
where P is "we ought to philosophise" Which is not quite the same.

I am aware of the following relationship
$(\sim P \Rightarrow P ) \Leftrightarrow \; (\sim(\sim P)\; \vee \: P)$

and combining this with the above would basically be a form of "Or Elimination" or proof by cases. But this is just an explanation of how its proof would be worked out.

Anyway the above is more of a digression, but perhaps it may have some weight on my question. Really what I am interested in is an intuitive understanding of Clavius' law. What are some common examples in everyday logic?

  • $\begingroup$ To be clear, I understand the formal def, but would like some colloquial usage. The whole "we ought to philosophize" example seemed liked "Or Elimination" $\endgroup$ – skyfire Jul 26 '15 at 1:20
  • $\begingroup$ There are two possibilities: Either $P$, or $\lnot P$. But by the premise, if $\lnot P$, then $P$. So in either case, $P$. $\endgroup$ – user856 Jul 26 '15 at 2:59
  • $\begingroup$ Clavius' Law is a form of reductio ad absurdum: suppose $\neg P$. if you derive a contradiction from it (that is, $P$), then $P$ must be the case. (Note that it assumes the double-negation elimination rule, hence it's not intuitionistically valid). $\endgroup$ – Bruno Bentzen Jul 26 '15 at 4:35

''Clavius' law'' is just a variant of proof by contradiction or reductio ad absurdum: If $\sim\! P$ implies $P$, then $\sim\! P$ is inconsistent (because it then also implies the contradiction $\sim\! P\land P$). Therefore $P$.

Formally: $\sim\! P \Rightarrow P\vdash P$.

You should be able to formulate any proof by contradiction as an instance of Clavius'law, but it might read a bit awkward in some cases.

Cantor's diagonal argument that $\mathbb R$ is not enumerable, written as an instance of Clavius' law:

Assume you have an enumeration of $\mathbb R$. Then, by diagonalization you can construct a real number that is not in that enumeration. Therefore you don't have an enumeration of $\mathbb R$. Therefore: $\mathbb R$ is not enumerable.

(Doubly negate the first premise to exactly match the logical form of Clavius' law, if you are picky.)

Argument against (absolute) Relativism, written as an instance of Clavius' law:

"No sentence is true" $\Rightarrow$ "There are true sentences" (for instance: "No sentence is true"). Therefore there are true sentences. ref

  • $\begingroup$ I don't understand how you can have a contradiction without a conjunction, or without having some proposition "p" and another "not p". You don't have either of those in the law of Clavius. $\endgroup$ – Doug Spoonwood Jul 26 '15 at 1:21
  • $\begingroup$ Well, write reductio in law form as $\sim\!P \Rightarrow (\sim \!Q\land Q) \vdash P$ for any $P,Q$. In any minimal deductive system it is interderivable with Clavius' law: First assume the reductio law and the premise of Clavius' law, $\sim\!P\Rightarrow P$. From there infer $\sim\! P\Rightarrow (P\land\sim\! P)$ and by reductio $P$, the conclusion of Clavius' law. Conversely, assume Clavius' law and $\sim\!P \Rightarrow (\sim \!Q\land Q)$. Using ex falso ($(Q\land \sim\! Q)\vdash P$, for any $Q,P$) we can infer $\sim\! P\Rightarrow P$ and then by Clavius' law $P$, the conclusion of reductio. $\endgroup$ – lodrik Jul 26 '15 at 2:07
  • $\begingroup$ Consequently Clavius' law is, like reductio, intuitionistically invalid. $\endgroup$ – lodrik Jul 26 '15 at 2:12
  • $\begingroup$ In laymans terms you assume ~p, derive p as per standard normal fwd proofs go, conditionalize, use clavius' law and conclude p. $\endgroup$ – skyfire Jul 26 '15 at 2:21
  • $\begingroup$ i.e. Clavius' law is more general than contradiction rule. $\endgroup$ – skyfire Jul 26 '15 at 2:23

" ∼P⇒P⊢P"

You can read this as meaning "Suppose that the negation of a proposition implies that proposition. It follows that the proposition is provable."

Or equivalently in Polish notation:

CNpp $\vdash$ p.

No one less than Aristotle himself did not understand the law of Clavius.

With the principle of bivalence in mind, the only way that the negation of a proposition can imply a proposition is when the proposition is true also. We'll informally prove this by contradiction.

Suppose that 'CNpp' is true (1). Suppose that 'p' is false (0). Then

CNpp = CN00.

CN00 = C10.

C10 = 0.

Thus, CNpp will end up as false. But, this contradicts our first hypothesis, and thus we conclude that 'p' is true when 'CNpp' is true. Therefore, the law of Clavius is correct.

The law of Clavius got used by Euclid when proving a theorem of number theory. p. 50-51 of J. Lukasiewicz's book on Aristotle's Syllogistic reads as follows:

"If the product of two integers, a and b, is divisible by a prime number n, then if a is not divisible by n, b should be divisible by n'. Let us now suppose that a = b and the product a x a (a^2) is divisible by n. It results from this supposition that 'If a is not divisible by n, then a is divisible by n'. Here we have an example of a true implication of the antecedent of which is the negation of the consequent. From this implication Euclid derives the theorem: 'If a^2 is divisible by a prime number n, then a is divisible by n.'

Or in more symbolic notation the ideas might get rendered as follows:

Suppose ab | n, and n is prime. Then if a | n is false, b | n is true. Suppose that a = b. Thus, aa | n. It follows that if a | n is false, a | n is true. Consequently let us suppose that aa | n, and n is prime. Then by the law of Clavius a | n is true.

As an example of the application of the theorem, since 36 is divisible by 3, it follows that 6 is divisible by 3. Or as one which might not seem too obvious, 50,625 is square. It's divisible by the prime number 5. So,

(50,625 / 5) = 10,125 is divisible by 5. Also, 50,625 is divisible by 3. So, 50,625 / 3 = 16,875 which is divisible by 3 also.

Additionally, the law of Clavius is a "weak" law. In other words, we can reverse the turnstile. Not only do we have

CNpp $\vdash$ p

but we also have

p $\vdash$ CNpp.

Thus, anytime you have a subformula of the type "CNpp" in any formula, you can replace it by a subformula of the type "p" anywhere in the formula and the truth value of the formula will not change. Or instead of evaluating shorter formulas, you can evaluate longer formulas by replacing any instance of a subformula of the type 'p' with a subformula of the type 'CNpp' in the formula, and the truth value of the formula will not change.

The law of Clavius can also get applied to determining whether or not a formula is a tautology, if it has only conditional and negation symbols (and variables or constants). The general pattern goes to assume that such a formula is not a tautology. Then you show that under that assumption it is a tautology. Discharging the hypothesis we have an implication which gives us the left-hand side of the law of Clavius. We thus conclude that the formula in mind is a tautology.

For example, suppose that we want to prove that

C CCpqr C Crp C s p

is a tautology.

We'll assume that it's not a tautology. Under that assumption, the consequent is false. Or in symbols we have that

C Crp C s p = 0.

If C Crp C s p = 0, then

Crp = 1 and

C s p = 0.

If C s p = 0, then

--> s = 1


--> p = 0.

Crp = 1 also, so

--> r = 0.

Since p = 0,

Cpq = 1.

Since Cpq = 1 and r = 0,

CCpqr = 0.

Thus, if C Crp C s p = 0, CCpqr = 0 also.

It follows that C CCpqr C Crp C s p = 1.

Thus, from the assumption of C CCpqr C Crp C s p not being a tautology, we've found that C CCpqr C Crp C s p is a tautology. Discharging the hypothesis we have that if C CCpqr C Crp C s p is not a tautology, then it is a tautology. By the law of Clavius we now conclude that C CCpqr C Crp C s p is a tautology.

Note that we didn't use proof by contradiction here in the form of deriving "p and not p", because nowhere did we derive a conjunction. Nor did we derive two conditionals, one of which implies a proposition, and the other it's negation. And you CANNOT logically infer from a proposition and it's negation, any tautology directly (you have to do more work first).


If a formula is a tautology, and it is a conditional, it can get informally proved using the method indicated above using the law of Clavius. Thus, if you want more practice with the law of Clavius, I'll suggest picking any conditional which any textbook says is a tautology and proving it in a way similar to the above. For example, try proving that any of the following are tautologies using the above method and the law of Clavius

CCpqCCqrCpr, CpCNpq, CpCqp, CCpCqrCCpqCpr, CCpCpqCpq, CCpqCCrpCrq, CCNpqCCNpNqp, CCpCqrCqCpr.


Clavius Law aka Consequentia Mirabilis is an instance of the more common Proof by Cases. Proof by Cases is the axiom schema:

/* Proof by Cases */
(¬ B → A) → ((B → A) → A)

If you now instantiate B = A, you get:

/* Clavius Law aka Consequentia Mirabilis */
(¬ A → A) → A

Interestingly you can go backwards and derive Proof by Cases from Consequentia Mirabilis as well. The interderivability holds over minimal logic. The instantiation B = A is also mentioned here:

Aristotle and the Consequentia Mirabilis
William Kneale - 1957


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.