Atomic formulas consist of a Latin letter optionally followed by more letters or digits. Exception: The English names of connectives (not, and, or, implies, iff) are reserved words and cannot be used as atomic formulas. Also note that the letter v is distinct from the connective ∨.
If φ and ψ are formulas, then so are ¬φ, (φ∧ψ), (φ∨ψ), (φ→ψ), (φ↔ψ).
Several notations for connectives are supported:
Connectives are listed in decreasing order of precedence. All binary connectives are left-associative.