Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

If x or x, then x

  1. Aug 30, 2009 #1
    I am trying to find a simple proof for the apparently simple formula

    (x or x) implies x

    using the axiom system of Lukasiewics. This axiom system uses only -> (implies) and ~ (not) as its primitive connectives. "x or y" stands for the formula ~x -> y.

    A1) x -> (y -> x)
    A2) (x -> (y -> z)) -> ( (x -> y) -> (x -> z) )
    A3) (~x -> ~y) -> (y -> x)

    Along with these are the usual rules of inference: modus ponens and substitution of formulas for variables.

    The first few theorems that follow are:

    T1) x -> x
    T2) (y -> z) -> ( (x -> y) -> (x -> z) )
    T3) ~x -> (x -> y)
    T4) ~~x -> x
    T5) x -> ~~x
    T6) (~x -> y) -> (~y -> x)
    T7) x -> ( (x -> y) -> y)
    T8) (x -> (y -> z) ) -> (y -> (x -> z) )
    T9) (x -> y) -> ( (y -> z) -> (x -> z) )

    I'm trying to prove (x or x) -> x, which stands for (~x -> x) -> x

    Here is a sketch of the proof I found:

    (1) x -> ( (~x -> x) -> x).........................A1
    (2) ~x ->( (~x -> x) -> x)........................T7

    or letting a stand for ( (~x ->x) -> x)

    (1') x -> a
    (2') ~x -> a
    (3) ~a -> x........................................................T6, etc. (omitting appeals to Modus Ponens and more obvious rules)
    (4) ~a -> a.......................................................(1'), (3), T2, ...
    (5) (a -> (~a -> ~y) ) -> (~a -> (~a -> ~y) )........T9, ...
    (6) (~a -> (a -> ~y) ) -> (a -> (~a -> ~y) )..........T8
    (7) (~a -> (~a -> ~y) )........................................(5), (6), T2, T3 ...
    (8) (~a ->~a) -> (~a -> ~y) )....................................A2,...
    (9) (~a -> ~y) )....................................................T1,...
    (10) y -> a...........................................................A3,...
    (11) (z -> z) -> a..................................................Substitution
    (12) a................................................................T1

    That's just a sketch, not listing all the steps. Is there a shorter way to prove this innocuous looking theorem?
     
  2. jcsd
  3. Aug 31, 2009 #2
    This one's shorter and makes use of the first three theorems only:

    (1) ~x -> (x -> ~(x -> x))...................................................T3
    (2) (x -> x) -> ((~x -> x) -> (x -> x))...................................A2
    (3) ((~x -> x) -> (x -> x))...................................................T1, MP
    (4) (~x -> x) -> (~x -> ~(x -> x))........................................(1), A2, MP
    (5) (~x -> ~(x -> x)) -> ((x -> x) -> x).................................A3
    (6) (5) -> ( (4) -> ((~x -> x) -> ((x -> x) -> x )))...................T2
    (7) ((~x -> x) -> ((x -> x) -> x))..........................................MP
    (8) (7) -> ( (3) -> ((~x -> x) -> x))......................................A2

    The point of all this is to convince myself that the axioms of Hilbert and Ackermann are theorems in the system of Lukasiewicz. They are:

    HA1) (x or x) -> x
    HA2) x -> (x or y)
    HA3) (x or y) -> (y or x)
    HA4) (y -> z) -> ( (x or y) -> (x or z) )

    HA2) through 4) follow in just a couple lines from the above theorems. But it was HA1) that was giving me trouble
     
    Last edited: Sep 1, 2009
  4. Sep 3, 2009 #3
    You will soon realise that formal proofs are unknown to forums in general.

    Particularly formal proofs without the help of the deduction theorem

    To make you laugh here is a proof using contradiction

    Let [tex]x\vee x[/tex]

    let [tex]\neg x[/tex]

    Since [tex] (x\vee x)\Longrightarrow (\neg x\rightarrow x)[/tex] ,and using M.Ponens twice we have x,hence a contradiction [tex] x\wedge \neg x[/tex].

    Thus [tex] (x\vee x)\Longrightarrow x[/tex]
     
  5. Sep 4, 2009 #4
    Bummer. Formal proofs are nifty....when you can find'em :rolleyes:. I was going to ask next some questions about Montague and Kalish's 'substitutionless' formalization of first order logic with identity, but maybe I should hold off on that.

    I haven't gotten to the Deduction Theorem yet, but if it makes proofs like that possible, I definitely need to learn about it. thanks.
     
Know someone interested in this topic? Share this thread via Reddit, Google+, Twitter, or Facebook




Similar Discussions: If x or x, then x
  1. {X} in X (Replies: 5)

  2. (x,x] = {x} (Replies: 20)

  3. Does x={x} (Replies: 12)

  4. Var(X) = Cov(X,X) ? (Replies: 5)

  5. E|X|=E(X) ? (Replies: 1)

Loading...