Logic axiom of simplification.

**matheinste** · Jun19-09, 11:44 AM

Hello all

I cannot find a simple explanation of the meaning of this axiom, probably because it is considered so obvioius that it needs no explanation. Can anyone explain in words.

$LaTeX Code: {a}\\rightarrow{({b}\\rightarrow{a})}$

Thanks. Matheinste.

**CRGreathouse** · Jun19-09, 12:52 PM

I'm not sure what you're looking for.

If a is false, then the statement reduces to "false implies stuff" which is by definition true. If a is true the statement reduces to "b implies true" which is also by definition true.

**honestrosewater** · Jun19-09, 02:08 PM

a -> (b -> a) is also equivalent to (a & b) -> a:

a -> (b -> a)
~a v (~b v a) [p -> q <=> ~p v q]
(~a v ~b) v a [(p v q) v r <=> p v (q v r)]
~(a & b) v a [~(p & q) <=> ~p v ~q]
(a & b) -> a

This formula also follows from the assumptions that (i) a formula always implies itself (p -> p) and (ii) lengthening a formula doesn't remove any of the formulas that the original implied ((p -> q) -> ((p & r) -> q)).

**matheinste** · Jun19-09, 02:45 PM

Originally Posted by honestrosewater

a -> (b -> a) is also equivalent to (a & b) -> a:

a -> (b -> a)
~a v (~b v a) [p -> q <=> ~p v q]
(~a v ~b) v a [(p v q) v r <=> p v (q v r)]
~(a & b) v a [~(p & q) <=> ~p v ~q]
(a & b) -> a

This formula also follows from the assumptions that (i) a formula always implies itself (p -> p) and (ii) lengthening a formula doesn't remove any of the formulas that the original implied ((p -> q) -> ((p & r) -> q)).

Thanks also to GRGreathouse. I see it now.

To Compuchip. Yes, I mistakenly repeated the thread but did not know how to remove the second posting.

Thanks. Matheinste.

**Preno** · Jun20-09, 09:31 AM

Originally Posted by matheinste

Hello all

I cannot find a simple explanation of the meaning of this axiom, probably because it is considered so obvioius that it needs no explanation. Can anyone explain in words.

$LaTeX Code: {a}\\rightarrow{({b}\\rightarrow{a})}$

Thanks. Matheinste.

It's a formula expressing the fact that a is deducible from a,b. It's a particular instance of the structural rule of weakening (which says that if A |- B, then A,phi |- B).