### 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 TrueChopEqvDiamond 4 ⊢ true ; f ; true ≡f 2, 3,EqvChain 5 ⊢ f ≡f 4, def. of

 ⊢ f ≡f DaEqvDiDt

Proof:

 1 ⊢ true ; f ≡f TrueChopEqvDiamond 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 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 ≡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 1,Prop

 ⊢ f ≡¬¬f DaEqvNotBaNot

Proof:

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

 ⊢ f ⊃ f BaElim

Proof:

 1 ⊢ f ≡f BaEqvBtBi 1 ⊢ f ⊃ f 2 ⊢ ( f ⊃f) 1,BoxGen 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 DaEqvNotBaNot 5 ⊢ f ⊃f 2, 3, 4,Prop

 ⊢ f ⊃f BaImpBt

Proof:

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

Here is an easy corollary:

 ⊢ f ⊃f DiamondImpDa

 ⊢ f ⊃f BaImpBi

Proof:

 1 ⊢ f ≡f BaEqvBtBi 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 1,BoxGen 3 ⊢ f 2,BiGen 4 ⊢ f ≡f BaEqvBiBt 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 1,DaEqvDa 10 ⊢ f ≡f 7, 8, 9,Prop

 ⊢ f ≡f BaEqvBaBa

Proof:

 1 ⊢ ¬f ≡¬f 2 ⊢ ¬f ≡¬¬¬f DaEqvNotBaNot 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 BiChopImpChop 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 BoxChopImpChop 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) BoxAndChopImport 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) AndChopAndCommute 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) BaRightChopImpChop 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 4,BiEqvBi 6 ⊢ w ≡w 7 ⊢ w ≡w 2, 3, 5, 6,Prop

 ⊢ ¬f ⊃¬f DiNotBaImpNotBa

Proof:

 1 ⊢ f ≡f BaEqvBaBa 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 DiNotBaImpNotBa 3 ⊢ (¬f) ; g ⊃¬f 1, 2,ImpChain

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