ITL
© 1996-2018







2.3 Properties of Diamond-a and Box-a

f f DaEqvDtDi

Proof:

1
true ; (f ; true) true ; (f ; true)
2
true ; (f ; true) true ; f
1, def. of 
3
true ; f f
4
true ; f ; true f
2, 3,EqvChain
5
f f
4, def. of 

qed

f f DaEqvDiDt

Proof:

1
true ; f f
2
(true ; f) ; true ( f) ; true
3
(true ; f) ; true f
2, def. of 
4
(true ; f) ; true true ; f ; true
5
true ; f ; true f
3, 4,Prop
6
f f
5, def. of 

qed

Here is a corollary of theorems DaEqvDtDi and DaEqvDiDt:

f f DtDiEqvDiDt

f f BaEqvBiBt

Proof:

1
¬f ¬f
2
¬f ≡¬f
3
¬f ¬f
4
¬f ¬f
5
⊢ ¬¬f ≡¬¬f
4,Prop
6
⊢ ¬¬f f
5, def. of 
7
f f
6, def. of 

qed

f f BaEqvBtBi

Proof:

1
¬f ¬f
2
¬f ≡¬f
3
¬f ¬f
4
⊢ ¬¬f f
5
⊢ ¬¬f f
1, 3, 4,Prop
6
f f
5, def. of 

qed

The following is a corollary of theorems BaEqvBtBi and BaEqvBiBt:

f f BtBiEqvBiBt

¬f ≡¬f DaNotEqvNotBa

Proof:

1
f ≡¬¬f
def. of 
2
¬f ≡¬f

qed

f ≡¬¬f DaEqvNotBaNot

Proof:

1
¬f ≡¬¬¬f
def. of 
2
¬¬f ≡¬¬f
1,Prop
3
f ≡¬¬f
4
f ¬¬f
5
f ≡¬¬f

qed

f f BaElim

Proof:

1
f f
1
f f
2
( f f)
3
( f f) f f
4
f f
2, 3,MP
5
f f
6
f f
1, 4, 5,Prop

qed

Here is a corollary:

f f DaIntro

Proof:

1
¬f ¬f
2
⊢ ¬¬f ¬¬f
1,Prop
3
f ≡¬¬f
4
f ≡¬¬f
5
f f
2, 3, 4,Prop

qed

f f BaImpBt

Proof:

1
f f
2
f f
3
f f
1, 2,MP

qed

Here is an easy corollary:

f f DiamondImpDa

f f BaImpBi

Proof:

1
f f
2
f f
3
f f
1, 2,MP

qed

Here is an easy corollary:

f f DiImpDa

f ⇒ ⊢f BaGen

Proof:

1
f
given
2
f
3
f
4
f f
5
f f
4,Prop
6
f
3, 5,MP

qed

(f g) f g BaImpDist

Proof:

1
(f g) ( f g)
2
((f g) ( f g))
3
((f g) ( f g))
( (f g) ( f g))
4
(f g) ( f g)
2, 3,MP
5
(f g) (f g)
6
f f
7
g g
8
(f g) ( f g)
4, 5, 6, 7,Prop

qed

Here are some easy corollaries:

(f g) f g BaImpBaEqvBa

f g f g BaImpBa

f g f g BaEqvBa

f g f g DaImpDa

f g f g DaEqvDa

(f g) f g BaAndEqv

(f1 fn) f1 fn BaAndGroupEqv

f f DaEqvDaDa

Proof:

1
f f
2
f f
3
f f
4
f f
5
f f
6
f f
7
f f
1, 3, 4, 6,EqvChain
8
f f
9
f f
10
f f
7, 8, 9,Prop

qed

f f BaEqvBaBa

Proof:

1
¬f ¬f
2
¬f ≡¬¬¬f
3
⊢ ¬¬f ¬¬f
2,Prop
4
⊢ ¬¬f ¬¬f
1, 3,Prop
5
f f
4, def. of 

qed

(f f1) f ; g f ; g1 BaLeftChopImpChop

Proof:

1
(f f1) (f f1)
2
(f f1) f ; g f1 ; g
3
(f f1) f ; g f1 ; g
1, 2,Prop

qed

(g g1) f ; g f ; g1 BaRightChopImpChop

Proof:

1
(g g1) (g g1)
2
(g g1) f ; g f ; g1
3
(g g1) f ; g f ; g1
1, 2,Prop

qed

f (g ; g1) (f g) ; (f g1) BaAndChopImport

Proof:

1
f f
2
f (g ; g1) (f g) ; g1
3
f f
4
f (f g) ; g1 (f g) ; (f g1)
5
f (g ; g1) (f g) ; (f g1)
1, 2, 3, 4,Prop

qed

(f ; f1) g (f g) ; (f1 g) ChopAndBaImport

Proof:

1
g (f ; f1) (g f) ; (g f1)
2
(g f) ; (g f1) (f g) ; (f1 g)
2
(f ; f1) g (f g) ; (f1 g)
1, 2,Prop

qed

f g ; g1 g ; ( f g1) BaChopImpChopBa

Proof:

1
f (g1 f g1)
2
(g1 f g1) g ; g1 g ; ( f g1)
3
f g ; g1 g ; ( f g1)
1, 2,Prop

qed

w w BoxStateEqvBaBoxState

Proof:

1
w w
2
w w
3
w w
4
w w
5
w w
6
w w
7
w w
2, 3, 5, 6,Prop

qed

¬f ¬f DiNotBaImpNotBa

Proof:

1
f f
2
f f
3
f f
1, 2,Prop
4
f ¬¬f
3, def. of 
5
¬f ¬f
4,Prop

qed

(¬f) ; g ¬f NotBaChopImpNotBa

Proof:

1
(¬f) ; g ¬f
2
¬f ¬f
3
(¬f) ; g ¬f
1, 2,ImpChain

qed







2018-10-21
Contact | Home | ITL home | Course | Proofs | Algebra | FL