Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Would Aristotele deem the following classically valid (*) conclusion

$$\lnot A \rightarrow A \vdash A$$

a petitio principii? How would he go about showing it?

http://en.wikipedia.org/wiki/Consequentia_mirabilis (English)

http://de.wikipedia.org/wiki/Consequentia_mirabilis (German - more complete)

Google's English translation of the German page.

share|improve this question
Are you asking how to prove $\lnot A \to A \vdash A$, or asking the historical question of how Aristotle, who did not have modern notation for propositional logic, would have thought about it? –  Carl Mummert Jan 11 '13 at 14:04
Good question, @CarlMummert. Thanks for the comment: I just woke up a little while ago! :-) –  amWhy Jan 11 '13 at 14:05
Any reason you linked to a German language article? True, the contents of the English equivalent is quite unhelpful, but not more so than the German one. –  Marc van Leeuwen Jan 11 '13 at 14:10

2 Answers 2

up vote 7 down vote accepted

I thought the principle of the consequentia mirabilis was this:

If the supposition that $\varphi$ is false in fact implies that $\varphi$ is true, then we can conclude that $\varphi$ is indeed true.

If you want symbols, then it is the rule

$$(A)\quad\frac{\Gamma, \not{\!A}\vdash A}{\Gamma \vdash A}$$

where $\not{\!A}$ indicates the contradictory of $A$, and $\Gamma$ are your background assumptions.

First, contra @amWhy, this is not begging the question or circular reasoning: it belongs to the same family of perfectly respectable reasoning as (indeed, is simply the dual of) the reductio proof rule

$$(B)\quad\frac{\Gamma, A \vdash \not{\!A}}{\Gamma \vdash \not{\!A}}$$

Second, contra @CarlMummert this is nothing specifically to do with the propositional calculus. You could have the rule as a rule of a syllogistic logic which lacks propositional connectives but knows when a pair of wffs are contradictory (so fit the schema with $A$ and $\not{\!A}$).

I'm not sure whether Aristotle himself ever uses either rule. In his derivation of the validity of Baroco in the Prior Analytics he comes close to the first, for he uses this rule

$$\frac{\Gamma, A, B \vdash \not{\!B}}{\Gamma, B \vdash \not{\!A}}$$

But that's not quite the same. Still, the rules $(A)$ and $(B)$ would seem to be available to Aristotle.

share|improve this answer
Yes, the natural deduction formulation does the same. Any particular reason to use /A instead of ~A? Is this historical more adequate? –  Cookie Monster Jan 11 '13 at 14:59
Traditional syllogistic lacks a negation sign, but does have rules for telling us when a pair of propositions are contradictories (e.g. All A are B and Some A are not B). –  Peter Smith Jan 11 '13 at 15:08
@CookieMonster Not so. The second rule is NOT implied by cut and the deduction theorem which say nothing about contradictories. –  Peter Smith Jan 11 '13 at 18:07
Why did you write $\not A$ instead of $\lnot A$? –  MJD Jan 11 '13 at 18:32
@PeterSmith sorry, my fault. Was thinking in terms of minimal logic where one additionally assumes /A = A -> f. –  Cookie Monster Jan 11 '13 at 20:19

I guess it is an instance of refutation already observed by Aristotele. I read:

Hence if the admitted proposition is contrary to the conclusion, refutation must result, since refutation is a syllogism which proves the contradictory conclusion. (Prior Analytics, II. xx, Tredennick 1949, p.499 , http://de.scribd.com/doc/34807238/Aristotle-Vol-01-Prior-Analytics-v-Tredennick-Loeb-1962)


f = contradictory conclusion
/A = admitted proposition
A = conclusion

Than in modern cast with /A = A -> f:

                -------- (Id)
G, /A |- A      /A |- /A
------------------------ (Modus Ponens)
       G, /A |- f
       ---------- (Reductio Ad Absurdum)
         G |- A

But I am not sure, since I am not an extensive Aristoteles reader, and since I stepped over this passage by chance.

But if the derivation is done as above, then the consequentia mirabilis is effectively deduced via double negation elimination, not doing justice to it.


share|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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