Proof of "x or x implies x" using Lukasiewics Axiom System

[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?

 

[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

 

[evagelos]

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

You will soon realize 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

 

[techmologist]

You will soon realize that formal proofs are unknown to forums in general.

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.

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

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.