Quote of the Day: logic (CT)

... a logic is always a logic over a type theory. Underlying a logic there is always a calculus of typed terms that one reasons about.

And what about propositional logic? It is included as a border case: it can be seen as a degenerate predicate logic in which all predicates are closed {i.e. do not contain term variables), so one can see propositional logic as a logic over the empty type theory.

-- Jacobs, et al. (1998).