Results 1 to 7 of 7

Math Help - Formal proof of "Law of ecxluded middle"

  1. #1
    Newbie
    Joined
    Mar 2011
    Posts
    12

    Formal proof of "Law of ecxluded middle"

    I wonder how to give a formal, Fitch-style, proof of P v \neg P ..?

    I am able to prove it by contradiction when I use that \neg P & P is a tautological consequence of \neg (P v \neg P ) . But in order to prove this (one of the DeMorgan's laws I think?) formally I have to use the law of excluded middle itself...

    I also know how to show these tautologies with truth tables, but an exercise explicitly ask for a formal proof of P v \neg P .

    All help is appreciated
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,528
    Thanks
    773
    Good question. Classical reasoning in natural deduction may be nonobvious. I'll describe it informally at first. I believe you can use double-negation elimination rule (DNE), which derives Q from ~~Q.

    Assume ~(P \/ ~P). Then assuming P leads to a contradiction, so ~P. However, this also leads to a contradiction. Thus, ~~(P \/ ~P), from where you get P \/ ~P by DNE.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Mar 2011
    Posts
    12
    Thank you emakarov, great help! Problem solved
    Follow Math Help Forum on Facebook and Google+

  4. #4
    Member
    Joined
    May 2011
    From
    Sacramento, CA
    Posts
    165
    I assume the formal system you want to use is natural deduction in the classical sense. Intuitionist logic, for instance, has problems with negation elimination rules, which results in questioning the law of excluded middle (LEM) altogether. In such a system, there would be no formal proof of the LEM. Instead, you could prove in that system up to step 7 below.

    0 | (p v p) [assumption]
    1 || p [assumption]
    2 || p v p [disjunction introduction, 1]
    3 || FALSE [contradiction, 0 2]
    4 | p [negation introduction, 1-3]
    5 | p v p [disjunction introduction, 4]
    6 | FALSE [contradiction, 0 5]
    7 (p v p) [negation introduction, 0-6]
    8 p v p [negation elimination, 7]

    Notice how everything up to step 8 was either an assumption or an introduction rule. Also notice that the only two lines that had their assumptions terminated (no spacer lines at the beginning) are the last two. The intuitionist has no problem with everything up to 7. The problem is only in the last step. In that step we have to eliminate the negations. For the intuitionist, p → p, but they disallow p → p, which by that and modus ponens would give us 8. Classically all statements are taken to possess either a true or false truth value. Thus, the LEM has to obtain because something either is or it is not, classically. However, other systems like intuitionism takes truth to be congruent with construction. Something is true only if we can define an algorithm or process to produce it. A sentence is false if its assumption leads to a contradiction. Classically, the law of double negation (negation elimination) says that both the above implications holds. Thus p is equivalent to p. Therefore, we can conclude 8 by the above natural deduction proof.
    Last edited by bryangoodrich; May 21st 2011 at 11:09 AM.
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Newbie
    Joined
    May 2011
    Posts
    10

    A shorter proof of the formal law of the excluded middle

    A shorter way to construct a proof here comes as to use a rule of single-negation elimination instead of double-negation elimination... "From a sub-derivation which starts with Np and derives a contradiction, we may immediately infer p." Jaskowski, one of the founders of natural deduction, and whose proof boxes lead to Fitch-style proofs, used this rule instead of double-negation elimination. But, I digress. In prefix notation a proof can go:

    0 | NApNp hypothesis
    1 || Np hypothesis
    2 || ApNp 2 alternation introduction
    3 || KApNpNApNp 3, 1 conjunction introduction
    4 | p 2-4 negation elimination
    5 | ApNp 5 alternation-introduction
    6 | KApNpNApNp 6, 1 conjunction introduction
    7 ApNp 1-7 negation elimination

    This does hold in some non-classical logics, and works as a proof in any non-classical logic where the rules of inference here used here work out as sound. If you want to consider all non-classical logics at once, this formal law neither holds nor does not hold.
    Follow Math Help Forum on Facebook and Google+

  6. #6
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,528
    Thanks
    773
    Spoonwood, welcome to the forum.

    Could you clarify your notation? I am not sure what A, K and N mean.
    Follow Math Help Forum on Facebook and Google+

  7. #7
    Newbie
    Joined
    May 2011
    Posts
    10
    Quote Originally Posted by emakarov View Post
    Spoonwood, welcome to the forum.

    Could you clarify your notation? I am not sure what A, K and N mean.
    Sure, sorry about that. "A" stands for alternation, or equivalently disjunction. In classical (2-valued logic) if Axy is true, then at least one of the alternates "x" or "y" is true. One might also say that if Axy is true, then either x is true, otherwise y is true. The term "alter" basically means "other", hence alternation. "K" stands for conjunction. In Polish, Jan Lukasiewicz a Pole invented this notation, the English word "conjunction" gets translated as "konjunction". Also, read aloud, the "c" in conjunction has a hard "k" sound to it. N stands for negation.

    So, in a more standard infix notation one might write Kxy as (x^y), Axy as
    (x v y), and Nx as ~(x). Actually, ~(x) isn't in infix notation, it comes in prefix notation. Unary functions, operations, and connectives simply don't exist in prefix (or suffix) notation since you need two symbols for an infix notation.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Replies: 1
    Last Post: September 16th 2011, 01:08 AM
  2. Replies: 2
    Last Post: June 4th 2011, 12:11 PM
  3. Replies: 2
    Last Post: April 24th 2011, 07:01 AM
  4. Replies: 1
    Last Post: October 25th 2010, 04:45 AM
  5. Replies: 1
    Last Post: June 4th 2010, 10:26 PM

Search Tags


/mathhelpforum @mathhelpforum