Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

> 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.



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


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...




Consider applying for YC's Summer 2026 batch! Applications are open till May 4

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: