ITL
© 1996-2018







5 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 


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 

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 


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 

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


f ≡¬¬f DaEqvNotBaNot


Proof:

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


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

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


f f BaImpBt


Proof:

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

Here is an easy corollary:


f f DiamondImpDa



f f BaImpBi


Proof:

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

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


(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

Here are some easy corollaries:


(f g) f g BaImpBaEqvBa



(f g) f g DaImpDaImpDa



(f g) f g DaImpDaEqvDa



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


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 


(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


(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


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


(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


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


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


¬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


(¬f) ; g ¬f NotBaChopImpNotBa


Proof:

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







2018-02-26
Contact | Home | ITL home | Course | Proofs | Algebra | FL