Law of Clavius explained 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? 
 A: ''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
A: 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
https://www.jstor.org/stable/628635?seq=1
A: " ∼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
and
--> 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).
Meta-theorem:
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.
