# If x or x, then x

1. Aug 30, 2009

### techmologist

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. Aug 31, 2009

### techmologist

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
3. Sep 3, 2009

### evagelos

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 $$x\vee x$$

let $$\neg x$$

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

Thus $$(x\vee x)\Longrightarrow x$$

4. Sep 4, 2009

### techmologist

Bummer. Formal proofs are nifty....when you can find'em . 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.