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.

Visão Geral

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

• Semântica categórica: Lógica categórica introduz a noção de "estrutura valorada numa categoria" C com a noção clássica da teoria dos modelos de uma estrutura aparecendo no caso particular no qual C é uma categoria de conjuntos e funções. Esta abordagem tem se revelado útil quando a noção conjunto-teórica de um modelo não é suficientemente geral e/ou é inconveniente. A modelarem de R.A.G. Seely, de várias teorias impredicativas, como o sistema F é um exemplo de utilidade da semântica categórica.
• Linguagens internas: Esta pode ser vista como a formalização e generalização da prova por diagrama comutativo. Define-se uma linguagem interna, adequada a nomear elementos constituintes de uma categoria, e então aplica-se a semântica categórica para tornar asserções numa lógica acima da linguagem interna, nos padrões categóricos correspondentes. Tem sido mais bem sucedido na teoria dos topos, no quais a linguagem interna dos topos juntamente com a semântica de uma lógica intucionista de ordem superior permite que se pense sobre os objetos e morfismos de topos "como se eles fossem conjuntos e funções". Isso tem sido bem sucedido no lidar com topos que têm "conjuntos" com propriedades incompatíveis com a lógica clássica. Um belo exemplo é o modelo de Dana Scott de cálculo lambda não tipado em termos de objetos que têm como retrato algébrico de suas próprias funções no espaço. Um outro é o modelo do sistema F de Moggi-Hyland por uma subcategoria interna completa de topos efetivos de Martin Hyland.
• Construções modelo-de-termos: Em vários 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 teorias da lógica equacional beta-eta sobre o cálculo lambda simplesmente tipado e categorias cartesianas fechadas. Categorias resultantes de teorias por construções de modelo-de-termos podem, em geral, ser caracterizadas pela equivalência de uma propriedade universal apropriada. Isso permitiu provas de propriedades meta-teóricas de algumas lógicas pelo significado de uma álgebra categórica apropriada. Por exemplo, Freyd apresentou uma prova das propriedades da existência e da disjunção da lógica intuicionística dessa forma.

Perspectiva histórica

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.

Um desenvolvimento análogo foi a ligação entre o cálculo lambda simplesmente tipado e as categorias cartesianas fechadas (Lawvere, Lambek, Scott), que proporcionou um ambiente para o desenvolvimento de teoria dos domínios. Teorias menos expressivas, do ponto de vista lógico matemático, tem suas próprias contrapartidas na teoria das categorias. Por exemplo, o conceito de uma teoria algébrica leva a dualidade de Gabriel-Ulmer. A visão de categorias como uma generalização unificando sintaxe e semântica tem sido produtiva no estudo de lógicas e teorias para aplicações na ciência da computação.

Os fundadores da teoria dos topos elementares foram Lawvere e Tierney. Escritos de Lawvere, às vezes redigidos num jargão filosófico, isolou alguns dos conceitos básicos como funtores adjuntos (que ele explicou como "objetivo" em um sentido Hegeliano, não sem alguma justificação). Um sub-objeto classificador é uma propriedade forte de se exigir de uma categoria, uma vez que com o fechamento cartesiano e limites finitos dá um topos (quebra de axioma mostra o quão forte a suposição é). Ainda mais o trabalho de Lawvere na década de 1960 deu uma teoria de atributos, que em certo sentido é uma teoria de subobjecto mais em sintonia com a teoria de tipos. As principais influências subsequentes foram a teoria de tipos de Martin-Löf no que diz respeito a lógica, polimorfismo de tipos e o cálculo de construções na área de programação funcional, a lógica linear na área da teoria da prova, a semântica de jogos e a teoria dos domínios sintética projetada. A ideia abstrata de fibração categórica tem sido muito aplicada.

Olhando para trás, historicamente, a maior ironia é que, em termos amplos, a lógica intuicionista tinha reaparecido na matemática, em um lugar central no programa Bourbaki-Grothendieck, uma geração depois que a confusa controvérsia Brouwer-Hilbert tinha terminado, com Hilbert como aparente vencedor. Bourbaki, ou mais precisamente Jean Dieudonné, tendo reivindicado o legado de Hilbert e a escola Göttingen, incluindo Emmy Noether, tinha reavivado a credibilidade da lógica intuicionista (embora o próprio Dieudonné tenha achado Lógica Intuicionística ridícula), como a lógica de um topos arbitrário, no qual a lógica clássica foi "o" topos dos conjuntos. Esta foi uma conseqüência, certamente inesperada, do ponto de vista relativo de Grothendieck; e não perdida em Pierre Cartier, um dos mais amplos do núcleo de matemáticos franceses em torno de Bourbaki e IHES. Era para Cartier dar uma exposição de Séminaire Bourbaki da lógica intuicionista.

Em uma perspectiva ainda mais ampla, pode-se tomar a teoria das categorias como sendo a matemática da segunda metade do século XX, o que a teoria da medida foi para a primeira metade. Foi Kolmogorov que aplicou a teoria da medida para a teoria da probabilidade, a primeira convincente (se não a única) abordagem axiomática. Kolmogorov também foi um autor pioneiro no início de 1920 sobre a formulação da lógica intuicionista, num estilo totalmente suportado pela abordagem lógica categórica depois (novamente, uma das formulações, não a única, o conceito realizabilidade de Stephen Kleene é também um candidato sério). Outro caminho para a lógica categórica, portanto, foi através de Kolmogorov, e esta é uma maneira de explicar o isomorfismo variável de Curry-Howard.

Ver também

• História da Teoria dos Topos

Referências

Livros

• Abramsky, Samson; Gabbay, Dov (2001). Handbook of Logic in Computer Science: Logic and algebraic methods. Oxford: Oxford University Press. ISBN 0-19-853781-6 

• Gabbay, Dov (2012). Handbook of the History of Logic: Sets and extensions in the twentieth century. Oxford: Elsevier. ISBN 978-0-444-51621-3 

• Kent, Allen; Williams, James G. (1990). Encyclopedia of Computer Science and Technology. New York: Marcel Dekker Inc. ISBN 0-8247-2272-8 

• Barr, M. and Wells, C. (1990), Category Theory for Computing Science. Hemel Hempstead, UK.
• Lambek, J. and Scott, P.J. (1986), Introduction to Higher Order Categorical Logic. Cambridge University Press, Cambridge, UK.
• Lawvere, F.W., and Rosebrugh, R. (2003), Sets for Mathematics. Cambridge University Press, Cambridge, UK.
• Lawvere, F.W. (2000), and Schanuel, S.H., Conceptual Mathematics: A First Introduction to Categories. Cambridge University Press, Cambridge, UK, 1997. Reprinted with corrections, 2000.

Primeiros artigos

• Lawvere, F.W., Functorial Semantics of Algebraic Theories. In Proceedings of the National Academy of Science 50, No. 5 (November 1963), 869-872.
• Lawvere, F.W., Elementary Theory of the Category of Sets. In Proceedings of the National Academy of Science 52, No. 6 (December 1964), 1506-1511.
• Lawvere, F.W., Quantifiers and Sheaves. In Proceedings of the International Congress on Mathematics (Nice 1970), Gauthier-Villars (1971) 329-334.

Leituras adicionais

• Michael Makkai and Gonzalo E. Reyes, 1977, First order categorical logic, Springer-Verlag.
• Lambek, J. and Scott, P. J., 1986. Introduction to Higher Order Categorical Logic. 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.
• Jacobs, Bart (1999). Categorical Logic and Type Theory. Col: Studies in Logic and the Foundations of Mathematics 141. [S.l.]: North Holland, Elsevier. ISBN 0-444-50170-3  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. According to P.T. Johnstone, this approach is unwieldy for simple types.
• P.T. Johnstone, 2002, Sketches of an Elephant, part D (vol 2) covers both first-order and higher-order logics, but not dependent or polymorphic types, considered by the author of interest mainly to computer science. Because it avoids polymorphic and dependent types, the categorical approach is easier to present in therms of a syntactic category just as in Lambek's book, but Sketches includes more recent developments, like .
• John Lane Bell (2005) The Development of Categorical Logic. Handbook of Philosophical Logic, Volume 12. Springer. Version available online at John Bell's homepage.
• Jean-Pierre Marquis and 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, D. M. Gabbay, A. Kanamori & J. Woods, eds., North-Holland, pp. 689–800. A preliminary version is available at [1].

Ligações externas

• Categorical Logic lecture notes by Steve Awodey