¬ ∧ ∨ ⊃ ≡ ∀ ∃ ( ) ⊢ position decides: p(…) is a predicate, f(…) in the brackets a function. A quantifier reaches over one unit; the dot in forall x. widens it