Logic axiom of simplification.

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

{a}\rightarrow{({b}\rightarrow{a})}

Thanks. Matheinste.

[CRGreathouse]

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]

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]

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]

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.

{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).