Lógica categórica
Lógica categórica é uma ramificação da teoria categórica dentro da matemática, adjacente a lógica matemática, mas mais notável pela sua conexão com a teoria da computação. Em termos gerais, lógica categórica representa tanto sintaxe e semântica por uma categoria, e uma interpretação por um functor. O framework categórico propicia um rico contexto conceitual para as construções lógicas e tipo-teóricas. O assunto tem sido reconhecido nestes termos desde 1970.
Existem três importantes temas na abordagem categórica à lógica:
Lógica categórica originou-se com a Functorial Semantics of Algebraic Theories (1963) e a Elementary Theory of the Category of Sets (1964) de William Lawvere. Lawvere reconheceu os topos de Grothendieck, introduziu na topologia algébrica, como um espaço generalizado, como uma generalização da categoria de conjuntos (Quantifiers and Sheaves (1970)). Com Myles Tierney, Lawvere então desenvolveu a noção de topos elementares, assim estabilizando o frutífero campo da teoria dos topos, que proporciona um tratamento categórico unificado da sintaxe e semântica da lógica de predicados de ordem superior.. A lógica resultante é formalmente intuicionística. Andre Joyal é creditado, no termo semântico de Kripke-Joyal, com a observação de que os modelos de feixe para a lógica de predicados, fornecido pela teoria de topos, generalizam a semântica de Kripke. Joyal e outros aplicaram estes modelos para estudar conceitos de ordem superior, como os números reais nos moldes intuicionísticos.
