X and Y are equivalent iff X ↔ Y is a tautology
X entails Y iff X → Y is a tautology
The symbol "∴" is pronounced "therefore" and means "everything that precedes this combines to prove what follows this."
The symbol "⊨" is pronounced "entails" (or "double turnstile") and means "if everything that precedes this is true, what follows must also be true."
The symbol "⊢" is pronounced "proves", "yields", or "turnstile" and means "because I know the things before this, I also know the things after it."
Use
→ inside a logical expression or formula
⊨ to express a derivation rule
⊢ to mean both ⊨ and "both sides are true"
∴ to mean both ⊢ and "and the right-hand side is our goal"