theories via term-model constructions can usually be characterized up to equivalence by a suitable universal property. This has enabled proofs of meta-theoretical properties of some logics by means of an appropriate categorical algebra. For instance, Freyd gave a proof of the existence and disjunction properties of intuitionistic logic this way. See also History of topos theory Notes References Books Seminal papers Further reading Fairly accessible introduction, but somewhat dated. The categorical approach to higher-order logics over polymorphic and dependent types was developed largely after this book was published. A comprehensive monograph written by a computer scientist; it covers both first-order and higher-order logics, and also polymorphic and dependent types. The focus is on fibred category as universal tool in categorical logic, which is necessary in dealing with polymorphic and dependent types. Version available online at John Bell's homepage. A preliminary version. External links Systems of formal logic Theoretical computer science