 Propositional connectives and quantifiers can be assigned types and can be denoted by constants of these types. The negation function maps truth values to truth values, so it has type \(({o}{o})\). Similarly, disjunction and conjunction (etc.) are binary functions from truth values to truth values, so they have type \(({o}{o}{o})\).