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.