Expanded a bit on the eliminability of non-constructive proofs with respect to geometric theories and sequents.

]]>created stub for Barr’s theorem (If a statement in geometric logic is deducible from a geometric theory using classical logic and the axiom of choice, then it is also deducible from it in constructive mathematics.)

]]>