# Antique handling of consequentia mirabilis?

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://de.wikipedia.org/wiki/Consequentia_mirabilis (German - more complete)

Google's English translation of the German page.

-
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

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.

-
Yes, the natural deduction formulation does the same. Any particular reason to use /A instead of ~A? Is this historical more adequate? –  j4n bur53 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. –  j4n bur53 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)

Take:

A = conclusion

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

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