Antique handling of consequentia mirabilis? Would Aristotle deem the following classically valid [DE, DE-to-EN] conclusion
$$\lnot A \rightarrow A \vdash A$$
a petitio principii? How would he go about showing it?
 A: 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.
A: 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)

Take:
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.
Bye
