Summary of the syntax of Propositional Logic:
Boolean operators:
| ∧ |  (And),           | 
| ∨ |  (Or),             | 
| ¬ |  (Not),            | 
| ⊃ |  (Implication),  | 
| ≡ |  (Equivalence)  | 
Syntax of propositional formulae in BNF (grammar):
| f ::= | true | P |¬f | f1 ∧ f2 | 
Derived Boolean operators:
| false     | ≜ | ¬true                       | 
| f1 ∨ f2 | ≜ | ¬(¬f1 ∧¬f2)            | 
| f1 ⊃ f2 | ≜ | ¬f
1 ∨ f2                      | 
| f1 ≡ f2 | ≜ | (f1 ⊃ f2) ∧ (f2 ⊃ f1) |