Properties of Diamond-a and Box-a

Prev-tail

Tail

5 Properties of Diamond-a and Box-a

⊢

f ≡

DaEqvDtDi

Proof:

1	⊢ true ; (f ; true) ≡ true ; (f ; true)	Prop
2	⊢ true ; (f ; true) ≡ true ; f	1, def. of
3	⊢ true ; f ≡f	TrueChopEqvDiamond
4	⊢ true ; f ; true ≡f	2, 3,EqvChain
5	⊢ f ≡f	4, def. of

⊢

f ≡

DaEqvDiDt

Proof:

1	⊢ true ; f ≡f	TrueChopEqvDiamond
2	⊢ (true ; f) ; true ≡ ( f) ; true	1,LeftChopEqvChop
3	⊢ (true ; f) ; true ≡f	2, def. of
4	⊢ (true ; f) ; true ≡ true ; f ; true	ChopAssoc
5	⊢ true ; f ; true ≡f	3, 4,Prop
6	⊢ f ≡f	5, def. of

Here is a corollary of theorems DaEqvDtDi and DaEqvDiDt:

⊢

f ≡

DtDiEqvDiDt

⊢

f ≡

BaEqvBiBt

Proof:

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

⊢

f ≡

BaEqvBtBi

Proof:

1	⊢ ¬f ≡¬f	DaEqvDtDi
2	⊢ ¬f ≡¬f	DiNotEqvNotBi
3	⊢ ¬f ≡¬f	2,DiamondEqvDiamond
4	⊢ ¬¬f ≡f	PTL
5	⊢ ¬¬f ≡f	1, 3, 4,Prop
6	⊢ f ≡f	5, def. of

The following is a corollary of theorems BaEqvBtBi and BaEqvBiBt:

⊢

f ≡

BtBiEqvBiBt

⊢

¬f ≡¬

DaNotEqvNotBa

Proof:

1	⊢ f ≡¬¬f	def. of
2	⊢ ¬f ≡¬f	1,Prop

⊢

f ≡¬

¬f

DaEqvNotBaNot

Proof:

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

⊢

f ⊃ f

BaElim

Proof:

1	⊢ f ≡f	BaEqvBtBi
1	⊢ f ⊃ f	BiElim
2	⊢ ( f ⊃f)	1,BoxGen
3	⊢ ( f ⊃f) ⊃f ⊃f	PTL
4	⊢ f ⊃f	2, 3,MP
5	⊢ f ⊃ f	PTL
6	⊢ f ⊃ f	1, 4, 5,Prop

Here is a corollary:

⊢

f ⊃

DaIntro

Proof:

1	⊢ ¬f ⊃¬f	BaElim
2	⊢ ¬¬f ⊃¬¬f	1,Prop
3	⊢ f ≡¬¬f	Prop
4	⊢ f ≡¬¬f	DaEqvNotBaNot
5	⊢ f ⊃f	2, 3, 4,Prop

⊢

f ⊃

BaImpBt

Proof:

1	⊢ f ≡f	BaEqvBiBt
2	⊢ f ⊃f	BiElim
3	⊢ f ⊃f	1, 2,MP

Here is an easy corollary:

⊢

f ⊃

DiamondImpDa

⊢

f ⊃

BaImpBi

Proof:

1	⊢ f ≡f	BaEqvBtBi
2	⊢ f ⊃f	PTL
3	⊢ f ⊃f	1, 2,MP

Here is an easy corollary:

⊢

f ⊃

DiImpDa

⊢

f ⇒ ⊢

BaGen

Proof:

1	⊢ f	given
2	⊢ f	1,BoxGen
3	⊢ f	2,BiGen
4	⊢ f ≡f	BaEqvBiBt
5	⊢ f ⊃f	4,Prop
6	⊢ f	3, 5,MP

⊢

(f ⊃g) ⊃

f ⊃

BaImpDist

Proof:

1	⊢ (f ⊃g) ⊃ ( f ⊃g)	BiImpDist
2	⊢ ((f ⊃g) ⊃( f ⊃g))	BoxGen
3	⊢ ((f ⊃g) ⊃( f ⊃g)) ⊃
	( (f ⊃g) ⊃( f ⊃g))	PTL
4	⊢ (f ⊃g) ⊃ ( f ⊃g)	2, 3,MP
5	⊢ (f ⊃g) ≡(f ⊃g)	BaEqvBtBi
6	⊢ f ≡f	BaEqvBtBi
7	⊢ g ≡g	BaEqvBtBi
8	⊢ (f ⊃g) ⊃ ( f ⊃g)	4, 5, 6, 7,Prop

Here are some easy corollaries:

⊢

(f ≡ g) ⊃

f ≡

BaImpBaEqvBa

⊢

(f ⊃g) ⊃

f ⊃

DaImpDaImpDa

⊢

(f ≡ g) ⊃

f ≡

DaImpDaEqvDa

⊢

f ⊃g ⇒

f ⊃

BaImpBa

⊢

f ≡ g ⇒

f ≡

BaEqvBa

⊢

f ⊃g ⇒

f ⊃

DaImpDa

⊢

f ≡ g ⇒

f ≡

DaEqvDa

⊢

(f ∧ g) ≡

f ∧

BaAndEqv

⊢

(f₁ ∧… ∧ f_n) ≡

f₁ ∧… ∧

f_n

BaAndGroupEqv

⊢

f ≡

DaEqvDaDa

Proof:

1	⊢ f ≡f	DaEqvDtDi
2	⊢ f ≡f	DiEqvDiDi
3	⊢ f ≡f	2,DiamondImpDiamond
4	⊢ f ≡f	PTL
5	⊢ f ≡f	DtDiEqvDiDt
6	⊢ f ≡f	5,DiamondEqvDiamond
7	⊢ f ≡f	1, 3, 4, 6,EqvChain
8	⊢ f ≡f	DaEqvDtDi
9	⊢ f ≡f	1,DaEqvDa
10	⊢ f ≡f	7, 8, 9,Prop

⊢

f ≡

BaEqvBaBa

Proof:

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

⊢

(f ⊃f₁) ⊃ f ; g ⊃f ; g₁

BaLeftChopImpChop

Proof:

1	⊢ (f ⊃f₁) ⊃(f ⊃f₁)	BaImpBi
2	⊢ (f ⊃f₁) ⊃ f ; g ⊃f₁ ; g	BiChopImpChop
3	⊢ (f ⊃f₁) ⊃ f ; g ⊃f₁ ; g	1, 2,Prop

⊢

(g ⊃g₁) ⊃ f ; g ⊃f ; g₁

BaRightChopImpChop

Proof:

1	⊢ (g ⊃g₁) ⊃(g ⊃g₁)	BaImpBt
2	⊢ (g ⊃g₁) ⊃ f ; g ⊃f ; g₁	BoxChopImpChop
3	⊢ (g ⊃g₁) ⊃ f ; g ⊃f ; g₁	1, 2,Prop

⊢

f ∧ (g ; g₁) ⊃ (f ∧ g) ; (f ∧ g₁)

BaAndChopImport

Proof:

1	⊢ f ⊃f	BaImpBi
2	⊢ f ∧ (g ; g₁) ⊃ (f ∧ g) ; g₁	BiAndChopImport
3	⊢ f ⊃f	BaImpBt
4	⊢ f ∧ (f ∧ g) ; g₁ ⊃ (f ∧ g) ; (f ∧ g₁)	BoxAndChopImport
5	⊢ f ∧ (g ; g₁) ⊃ (f ∧ g) ; (f ∧ g₁)	1, 2, 3, 4,Prop

⊢

(f ; f₁) ∧

g ⊃ (f ∧ g) ; (f₁ ∧ g)

ChopAndBaImport

Proof:

1	⊢ g ∧ (f ; f₁) ⊃ (g ∧ f) ; (g ∧ f₁)	BaAndChopImport
2	⊢ (g ∧ f) ; (g ∧ f₁) ≡ (f ∧ g) ; (f₁ ∧ g)	AndChopAndCommute
2	⊢ (f ; f₁) ∧g ⊃ (f ∧ g) ; (f₁ ∧ g)	1, 2,Prop

⊢

f ⊃ g ; g₁ ⊃g ; (

f ∧ g₁)

BaChopImpChopBa

Proof:

1	⊢ f ⊃(g₁ ⊃f ∧ g₁)	PTL
2	⊢ (g₁ ⊃f ∧ g₁) ⊃ g ; g₁ ⊃g ; ( f ∧ g₁)	BaRightChopImpChop
3	⊢ f ⊃ g ; g₁ ⊃g ; ( f ∧ g₁)	1, 2,Prop

⊢

w ≡

BoxStateEqvBaBoxState

Proof:

1	⊢ w ≡w	StateEqvBi
2	⊢ w ≡w	1,BoxEqvBox
3	⊢ w ≡w	BtBiEqvBiBt
4	⊢ w ≡w	PTL
5	⊢ w ≡w	4,BiEqvBi
6	⊢ w ≡w	BaEqvBiBt
7	⊢ w ≡w	2, 3, 5, 6,Prop

⊢

f ⊃¬

DiNotBaImpNotBa

Proof:

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

⊢

(¬

f) ; g ⊃¬

NotBaChopImpNotBa

Proof:

1	⊢ (¬f) ; g ⊃¬f	ChopImpDi
2	⊢ ¬f ⊃¬f	DiNotBaImpNotBa
3	⊢ (¬f) ; g ⊃¬f	1, 2,ImpChain

Prev-tail

Front

2018-02-26