I am trying to find a simple proof for the apparently simple formula(adsbygoogle = window.adsbygoogle || []).push({});

(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 lettingastand 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?

**Physics Forums - The Fusion of Science and Community**

The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

# If x or x, then x

**Physics Forums - The Fusion of Science and Community**