[ArtB]

> a single inconsistency in a formal logical system means you can prove anything. if both A and !A are true, then you can prove anything you wish via contradiction.

I believe this has been solved in intuitionistic logic (http://en.wikipedia.org/wiki/Intuitionistic_logic). If you don't except the law of the excluded middle and require constructive proofs you avoid many of these shenanigans.

[quchen]

Although intuitionistic logic does not have the axiom

    ------ (LEM)
    A ∨ ¬A

that is, the law of the exluded middle (LEM) can not be derived "from nothing" for all propositions, it is still an inconsistency if you can prove A ∧ ¬A to be true, since

                             ------ (Assumption)
                             A ∧ ¬A
    ------ (Assumption)      ------ (∧E2)
    A ∧ ¬A                     ¬A
    ------ (∧E1)             ------ (Definition of ¬)
        A                    A ⇒ ⊥
       ---------------------------- (⇒E)
                  ⊥
           --------------- (⇒I, discharge assumption)
              A ∧ ¬A ⇒ ⊥
           --------------- (Definition of ¬)
              ¬(A ∧ ¬A)

In other words, assuming A ∧ ¬A holds you can prove the false proposition ⊥ (from which you can prove anything).

(Note that the De Morgan's law ¬(A ∧ ¬A) ⇒ A ∨ ¬A does not hold without the LEM, so the above proof cannot be simplified in terms of it!)

[MereInterest]

A question. Wouldn't this line of reasoning still work? It is entirely a constructive proof, as opposed to the GP's proof by contradiction.

http://en.wikipedia.org/wiki/Principle_of_explosion#The_proo...