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 | Science Articles, Homework Help, Discussion**

Join Physics Forums Today!

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

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 | Science Articles, Homework Help, Discussion**