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!)
(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!)