Lógica categórica - Categorical logic

Este artigo é sobre lógica matemática no contexto da teoria das categorias. Para o sistema lógico de Aristóteles, veja o termo lógica .

A lógica categórica é o ramo da matemática em que ferramentas e conceitos da teoria das categorias são aplicados ao estudo da lógica matemática . Também é notável por suas conexões com a ciência da computação teórica . Em termos gerais, a lógica categórica representa a sintaxe e a semântica por uma categoria e uma interpretação por um functor . A estrutura categórica fornece uma base conceitual rica para construções lógicas e teóricas de tipo . O assunto é reconhecível nesses termos desde cerca de 1970.

Visão geral

Existem três temas importantes na abordagem categórica da lógica:

Semântica categórica
A lógica categórica introduz a noção de estrutura avaliada em uma categoria C com a noção teórica do modelo clássico de uma estrutura que aparece no caso particular em que C é a categoria de conjuntos e funções . Esta noção tem se mostrado útil quando a noção teórica dos conjuntos de um modelo carece de generalidade e / ou é inconveniente. A modelagem de RAG Seely de várias teorias impredicativas , como o sistema F, é um exemplo da utilidade da semântica categórica.
Verificou-se que os conectivos da lógica pré-categórica foram mais claramente compreendidos usando o conceito de functor adjunto, e que os quantificadores também foram mais bem compreendidos usando functores adjunto.
Linguagens internas
Isso pode ser visto como uma formalização e generalização da prova por busca de diagramas . Um define uma linguagem interna adequada nomeando constituintes relevantes de uma categoria e, em seguida, aplica a semântica categórica para transformar asserções em uma lógica sobre a linguagem interna em declarações categóricas correspondentes. Isso tem sido mais bem-sucedido na teoria dos topos , onde a linguagem interna de um topos, juntamente com a semântica da lógica intuicionista de ordem superior em um topos, permite raciocinar sobre os objetos e morfismos de um topos "como se fossem conjuntos e funções". Isso tem sido bem-sucedido no tratamento de topos que possuem "conjuntos" com propriedades incompatíveis com a lógica clássica. Um bom exemplo é o modelo de cálculo lambda não tipado de Dana Scott em termos de objetos que se retraem em seu próprio espaço de função. Outro é o modelo Moggi-Hyland do sistema F por uma subcategoria completa interna do topos efetivo de Martin Hyland .
Construções de modelo de termo
Em muitos casos, a semântica categórica de uma lógica fornece uma base para estabelecer uma correspondência entre teorias na lógica e instâncias de um tipo apropriado de categoria. Um exemplo clássico é a correspondência entre as teorias de βη - lógica equacional sobre cálculo lambda simplesmente digitado e categorias fechadas cartesianas . As categorias que surgem de teorias por meio de construções de modelos de termos podem geralmente ser caracterizadas até a equivalência por uma propriedade universal adequada . Isso permitiu provas de propriedades metateóricas de algumas lógicas por meio de uma álgebra categórica apropriada . Por exemplo, Freyd deu uma prova das propriedades de existência e disjunção da lógica intuicionista dessa maneira.

Veja também

Notas

Referências

Livros
  • Abramsky, Samson; Gabbay, Dov (2001). Manual de Lógica em Ciência da Computação: Métodos lógicos e algébricos . Oxford: Oxford University Press. ISBN 0-19-853781-6.
  • Gabbay, Dov (2012). Manual da História da Lógica: Conjuntos e extensões no século XX . Oxford: Elsevier. ISBN 978-0-444-51621-3.
  • Kent, Allen; Williams, James G. (1990). Enciclopédia de Ciência e Tecnologia da Computação . Nova York: Marcel Dekker Inc. ISBN 0-8247-2272-8.
  • Barr, M. e Wells, C. (1990), Category Theory for Computing Science . Hemel Hempstead , Reino Unido.
  • Lambek, J. e Scott, PJ (1986), Introduction to Higher Order Categorical Logic . Cambridge University Press, Cambridge, Reino Unido.
  • Lawvere, FW e Rosebrugh, R. (2003), Sets for Mathematics . Cambridge University Press, Cambridge, Reino Unido.
  • Lawvere, FW (2000) e Schanuel, SH , Conceptual Mathematics: A First Introduction to Categories . Cambridge University Press, Cambridge, UK, 1997. Reimpresso com correções, 2000.

Artigos seminais

  • Lawvere, FW , Functorial Semantics of Algebraic Theories . Em Proceedings of the National Academy of Sciences 50, No. 5 (novembro de 1963), 869-872.
  • Lawvere, FW , Teoria Elementar da Categoria de Conjuntos . Em Proceedings of the National Academy of Sciences 52 , No. 6 (dezembro de 1964), 1506-1511.
  • Lawvere, FW , Quantifiers and Sheaves . Em Proceedings of the International Congress on Mathematics (Nice 1970) , Gauthier-Villars (1971) 329-334.

Leitura adicional

  • Michael Makkai e Gonzalo E. Reyes, 1977, Lógica categórica de primeira ordem , Springer-Verlag.
  • Lambek, J. e Scott, PJ, 1986. Introduction to Higher Order Categorical Logic . Introdução razoavelmente acessível, mas um tanto desatualizada. A abordagem categórica à lógica de ordem superior sobre os tipos polimórficos e dependentes foi desenvolvida amplamente após a publicação deste livro.
  • Jacobs, Bart (1999). Lógica categórica e teoria dos tipos . Studies in Logic and the Foundations of Mathematics 141. North Holland, Elsevier. ISBN 0-444-50170-3.Uma monografia abrangente escrita por um cientista da computação; ele cobre as lógicas de primeira e de ordem superior e também os tipos polimórficos e dependentes. O foco está na categoria fibrosa como ferramenta universal na lógica categórica, que é necessária para lidar com tipos polimórficos e dependentes.
  • John Lane Bell (2005) The Development of Categorical Logic . Handbook of Philosophical Logic, Volume 12. Springer. Versão disponível online na página inicial de John Bell.
  • Jean-Pierre Marquis e Gonzalo E. Reyes (2012). The History of Categorical Logic 1963–1977 . Handbook of the History of Logic: Sets and Extensions in the Twentieth Century, Volume 6, DM Gabbay, A. Kanamori & J. Woods, eds., North-Holland, pp. 689-800. Uma versão preliminar está disponível em [1] .

links externos