Na teoria das categorias, especificamente lógica categórica, a linguagem de Mitchell–Bénabou é uma linguagem formal que permite facilitar a demonstração de propriedades de topos. Com ela é possível tratar os objetos e morfismos de um topos como se fossem conjuntos e funções num universo satisfazendo as regras da lógica intuicionista de ordem superior.

A linguagem foi inicialmente desenvolvida por William Mitchell, com adições por Jean Bénabou e outros.

A determinação de validade de fórmulas na linguagem de Mitchell–Bénabou pode ser feita pela semântica de Kripke–Joyal, desenvolvida por André Joyal, como generalização das semânticas de Kripke.

Definição Na linguagem, termos são classificadas de acordo com tipos. A família dos tipos é definida recursivamente a seguir. Cada tipo básico (de uma família previamente escolhida) é um tipo. Se e são tipos, então e também são tipos. e são tipos.

Se cada tipo básico for associado a um objeto de um topos , então cada tipo associa-se a um objeto de , de acordo com as regras: (o produto categorial), (o objeto exponencial), é o objeto terminal e é o classificador de subobjetos.

Um contexto é uma sequência finita de tipos; denota-se um contexto por , onde são tipos e são símbolos de variáveis, escolhidas arbitrariamente, desde que sejam distintas. Cada contexto tem uma interpretação , como produto das interpretações dos tipos constituintes.

Um sequente é uma expressão do formato , onde é uma expressão possivelmente mencionando as variáveis de e é um tipo. Os sequentes bem formados são definidos recursivamente a seguir. Se é parte do contexto , então é bem formado. Se é bem formado, então é bem formado. Se e são bem formados, então é bem formado. é bem formado. Se e são bem formados, então é bem formado. Se é bem formado, então é bem formado; similarmente à segunda projeção. Se e são bem formados, então é bem formado. Para cada constante dada (numa família previamente escolhida), é bem formado.

A linguagem de Mitchell–Bénabou é a linguagem consistindo dos sequentes bem formados como acima.

Supõe-se que toda constante dada recebe interpretação como morfismo em . Então, cada sequente bem formado recebe interpretação como morfismo , dada recursivamente. é a projeção . é o morfismo transposto de pela adjunção exponencial. , onde é como na adjunção exponencial. . . ; similarmente à segunda projeção. , onde é morfismo característico de . , onde é transposto de .

Conectivos lógicos Expressões de tipo podem ser imaginadas como valores lógicos. A linguagem de Mitchell–Bénabou é suficiente para definir os conectivos lógicos, como a seguir. . . , onde pode mencionar . . . . . , onde pode mencionar .

Se é um contexto e são sequentes bem formados, escreve-se

quando , onde é o subobjeto associado a . Com isso, pode-se mostrar que valem as regras usuais da lógica intuicionística de predicados.

Semântica de Kripke–Joyal Dado sequente bem formado , e dado morfismo , escreve-se ou quando , onde é classificador de subobjetos no topos . Neste caso, diz-se que força . Quando é vazio, de modo que , lê-se como "φ é válido em ".

Pode-se mostrar as seguintes regras de semântica de conectivos lógicos. se e só se e . se e só se existe epimorfismo tal que e . se e só se, para cada seta tal que , vale . se e só se é objeto inicial. se e só se, para quaisquer setas e , vale . se e só se existem epimorfismo e morfismo tais que . se e só se .

A interpretação mais restritiva dos conectivos é o que faz com a que a semântica de Kripke–Joyal seja em geral apenas intuicionista (isto é, sem precisar satisfazer ).

A seguir, exemplos de interpretações. Uma seta é um monomorfismo se e só se é válido (isto é, é "internamente injetivo"). Um topos satisfaz (o "axioma da escolha interno") se e só se, para cada , o functor leva epimorfismos a epimorfismos. Um objeto de naturais num topos consiste de morfismos e tais que, para quaisquer morfismos e , existe único morfismo tal que e . (Este é o princípio de indução.) Se um topos admite um objeto de naturais, também admite um objeto de inteiros, um objeto de racionais e um objeto de reais de Dedekind, dados por fórmulas adequadas.

Semântica de feixes Quando é um topos de Grothendieck , para a semântica de Kripke–Joyal basta analisar os casos especiais , onde é um membro do separador . (Aqui, denota a feixificação.)

Para feixe , e para , denota-se quando . (Lembrar que é o conjunto de peneiras fechadas em , enquanto é a peneira máxima em .) Isto é equivalente à definição anterior pois .

Neste caso, existem as regras de manipulações de conectivos lógicos. (Abaixo, .) se e só se e . se e só se existe cobertura tal que, para cada índice , vale ou . se e só se, para cada , implica . se e só se, para cada , implica que a família vazia cobre . se e só se, para cada e cada , vale . se e só se existe cobertura e existem elementos tais que para cada índice .

Aplicações A linguagem de Mitchell–Bénabou (junto à semântica de Kripke–Joyal) pode ser usada para estudar modelos de sistemas intuicionísticos. Por exemplo, se é uma categoria pequena de espaços topológicos incluindo e satisfaz certas propriedades adicionais, então o topos de Grothendieck (onde é a topologia de Grothendieck das coberturas abertas) valida o teorema de continuidade de Brouwer: "todas as funções são contínuas", onde é o objeto de reais de Dedekind (que neste topos é dado por , o feixe das funções reais contínuas).

Também, a linguagem pode ser usada para provar resultados sobre topos como se fossem universos de conjuntos; um exemplo a seguir. Construtivamente vale que, se é um anel comutativo unitário tal que todo elemento de que não é invertível é zero, então todo -módulo finitamente gerado não não admite base. (Mas não é possível provar que sempre admita base.) Aplicando-se essa afirmação a um topos adequado, prova-se o seguinte. Seja um esquema reduzido, e seja um -módulo de tipo finito; então é localmente finitamente livre num aberto denso. (Mas não o precisa ser em todo o espaço.)

Bibliografia

Categoria:Teoria das categorias Categoria:Lógica