| | 5 Properties of Diamond-a
and Box-a
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 | |
5 | ⊢ f ≡f | 4, def. of |
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 | |
6 | ⊢ f ≡f | 5, def. of |
Here is a corollary of theorems DaEqvDtDi and DaEqvDiDt:
Proof:
1 | ⊢ ¬f ≡¬f | |
2 | ⊢ ¬f ≡¬f | |
3 | ⊢ ¬f ≡¬f | |
4 | ⊢ ¬f ≡¬f | |
5 | ⊢ ¬¬f ≡¬¬f | |
6 | ⊢ ¬¬f ≡f | 5, def. of |
7 | ⊢ f ≡f | 6, def. of |
Proof:
1 | ⊢ ¬f ≡¬f | |
2 | ⊢ ¬f ≡¬f | |
3 | ⊢ ¬f ≡¬f | |
4 | ⊢ ¬¬f ≡f | |
5 | ⊢ ¬¬f ≡f | |
6 | ⊢ f ≡f | 5, def. of |
The following is a corollary of theorems BaEqvBtBi and BaEqvBiBt:
Proof:
1 | ⊢ f ≡¬¬f | def. of |
2 | ⊢ ¬f ≡¬f | |
Proof:
1 | ⊢ ¬f ≡¬¬¬f | def. of |
2 | ⊢ ¬¬f ≡¬¬f | |
3 | ⊢ f ≡¬¬f | |
4 | ⊢ f ≡¬¬f | |
5 | ⊢ f ≡¬¬f | |
Proof:
1 | ⊢ f ≡f | |
1 | ⊢ f ⊃ f | |
2 | ⊢ ( f ⊃f) | |
3 | ⊢ ( f ⊃f) ⊃f ⊃f | |
4 | ⊢ f ⊃f | |
5 | ⊢ f ⊃ f | |
6 | ⊢ f ⊃ f | |
Here is a corollary:
Proof:
1 | ⊢ ¬f ⊃¬f | |
2 | ⊢ ¬¬f ⊃¬¬f | |
3 | ⊢ f ≡¬¬f | |
4 | ⊢ f ≡¬¬f | |
5 | ⊢ f ⊃f | |
Proof:
1 | ⊢ f ≡f | |
2 | ⊢ f ⊃f | |
3 | ⊢ f ⊃f | |
Here is an easy corollary:
Proof:
1 | ⊢ f ≡f | |
2 | ⊢ f ⊃f | |
3 | ⊢ f ⊃f | |
Here is an easy corollary:
Proof:
1 | ⊢ f | given |
2 | ⊢ f | |
3 | ⊢ f | |
4 | ⊢ f ≡f | |
5 | ⊢ f ⊃f | |
6 | ⊢ f | |
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) | |
5 | ⊢ (f ⊃g) ≡(f ⊃g) | |
6 | ⊢ f ≡f | |
7 | ⊢ g ≡g | |
8 | ⊢ (f ⊃g) ⊃ ( f ⊃g) | |
Here are some easy corollaries:
⊢ | (f ≡ g) ⊃f ≡g | | BaImpBaEqvBa |
⊢ | (f ⊃g) ⊃f ⊃g | | DaImpDaImpDa |
⊢ | (f ≡ g) ⊃f ≡g | | DaImpDaEqvDa |
⊢ | (f1 ∧… ∧ fn) ≡f1 ∧… ∧fn | | BaAndGroupEqv |
Proof:
1 | ⊢ f ≡f | |
2 | ⊢ f ≡f | |
3 | ⊢ f ≡f | |
4 | ⊢ f ≡f | |
5 | ⊢ f ≡f | |
6 | ⊢ f ≡f | |
7 | ⊢ f ≡f | |
8 | ⊢ f ≡f | |
9 | ⊢ f ≡f | |
10 | ⊢ f ≡f | |
|
Proof:
1 | ⊢ ¬f ≡¬f | |
2 | ⊢ ¬f ≡¬¬¬f | |
3 | ⊢ ¬¬f ≡¬¬f | |
4 | ⊢ ¬¬f ≡¬¬f | |
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 | |
⊢ | (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 | |
⊢ | 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) | |
⊢ | (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) | |
⊢ | 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) | |
⊢ | 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 | |
Proof:
1 | ⊢ f ≡f | |
2 | ⊢ f ⊃f | |
3 | ⊢ f ⊃f | |
4 | ⊢ f ⊃¬¬f | 3, def. of |
5 | ⊢ ¬f ⊃¬f | |
⊢ | (¬f) ; g ⊃¬f | | NotBaChopImpNotBa |
Proof:
1 | ⊢ (¬f) ; g ⊃¬f | |
2 | ⊢ ¬f ⊃¬f | |
3 | ⊢ (¬f) ; g ⊃¬f | |
| | |