# Linguagem de Mitchell–Bénabou

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 T$_i$, … (de uma família previamente escolhida) é um tipo.
* Se A e B são tipos, então A × B e A → B também são tipos.
* 1 e Ω são tipos.
Se cada tipo básico T$_i$ for associado a um objeto [T$_i$] de um topos E, então cada tipo associa-se a um objeto de E, de acordo com as regras:
* [A × B] = [A] × [B] (o produto categorial), [A → B] = [B]$^{[A]}$ (o objeto exponencial), [1] é o objeto terminal e [Ω] é o classificador de subobjetos.
Um contexto é uma sequência finita de tipos; denota-se um contexto por Γ := x$_1$ : A$_1$, …, x$_n$ : A$_n$, onde A$_i$ são tipos e x$_i$ são símbolos de variáveis, escolhidas arbitrariamente, desde que sejam distintas. Cada contexto Γ tem uma interpretação [Γ] = [A$_1$] × … × [A$_n$], como produto das interpretações dos tipos constituintes.
Um sequente é uma expressão do formato Γ ⊢ e : B, onde e é uma expressão possivelmente mencionando as variáveis de Γ e B é um tipo. Os sequentes bem formados são definidos recursivamente a seguir.
* Se x$_i$ : A$_i$ é parte do contexto Γ, então Γ ⊢ x$_i$ : A$_i$ é bem formado.
* Se Γ, x : C ⊢ e : B é bem formado, então Γ ⊢ λ (x : C). e : C → B é bem formado.
* Se Γ ⊢ f : C → B e Γ ⊢ x : C são bem formados, então Γ ⊢ f x : B é bem formado.
* Γ ⊢ : 1 é bem formado.
* Se Γ ⊢ a : A e Γ ⊢ b : B são bem formados, então Γ ⊢ (a, b) : A × B é bem formado.
* Se Γ ⊢ e : A × B é bem formado, então Γ ⊢ p$_1$ e : A é bem formado; similarmente à segunda projeção.
* Se Γ ⊢ a : A e Γ ⊢ b : A são bem formados, então Γ ⊢ (a = b) : Ω é bem formado.
* Para cada constante dada h : S → T (numa família previamente escolhida), Γ ⊢ h : S → T é bem formado.
A linguagem de Mitchell–Bénabou é a linguagem consistindo dos sequentes bem formados como acima.
Supõe-se que toda constante dada h : S → T recebe interpretação [h] : [S] → [T] como morfismo em E. Então, cada sequente bem formado Γ ⊢ e : B recebe interpretação como morfismo [Γ] → [B], dada recursivamente.
* [x$_1$ : A$_1$, …, x$_n$ : A$_n$ ⊢ x$_i$ : A$_i$] é a projeção [A$_1$] × … × [A$_n$] → [A$_i$].
* [Γ ⊢ λ (x : C). e : C → B] é o morfismo [Γ] → [B]$^{[C]}$ transposto de [Γ, x ⊢ e] : [Γ] × [C] → [B] pela adjunção exponencial.
* [Γ ⊢ f x] := ap ∘ ([Γ ⊢ f], [Γ ⊢ x]), onde ap : [B]$^{[C]}$ × [C] → [B] é como na adjunção exponencial.
* [Γ ⊢ : 1] := : [Γ] → 1.
* [Γ ⊢ (a, b)] := ([Γ ⊢ a], [Γ ⊢ b]).
* [Γ ⊢ p$_1$ e] := p$_1$ ∘ [Γ ⊢ e]; similarmente à segunda projeção.
* [Γ ⊢ (a = b)] := [=] ∘ ([Γ ⊢ a], [Γ ⊢ b]), onde [=] : [A] × [A] → Ω é morfismo característico de (id, id) : [A] → [A] × [A].
* [Γ ⊢ h] := h$^^$ ∘, onde h$^^$ : 1 → [T]$^{[S]}$ é transposto de [h] ∘ p$_2$ : 1 × [S] ≅ [S] → [T].

### 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.
* vero := ( =) : Ω.
* p ∧ q := ((p, q) = (vero, vero)).
* ∀ (x : A), p := ((λ (x : A), p) = (λ (x : A), vero)), onde p pode mencionar x.
* falso := ∀ (p : Ω), p.
* p ⇒ q := (p = p ∧ q).
* ¬ p := p ⇒ falso.
* p ∨ q := ∀ (r : Ω), (p ⇒ r) ⇒ ((q ⇒ r) ⇒ r).
* ∃ (x : A), p := ∀ (r : Ω), (∀ (x : A), p ⇒ r) ⇒ r, onde p pode mencionar x.
Se Γ é um contexto e Γ ⊢ φ$_i$ : Ω são sequentes bem formados, escreve-se
    Γ | φ$_1$, …, φ$_n$ ⊢ φ$_0$
quando m$_1$ ∩ … ∩ m$_n$ ⊆ m$_0$, onde m$_i$ é o subobjeto associado a [Γ ⊢ φ$_i$] : [Γ] → Ω. 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 a : U → [Γ], escreve-se
    a ⊩ φ ou U ⊩ φ(a)
quando [Γ ⊢ φ] ∘ a = vero ∘, onde vero : 1 → Ω é classificador de subobjetos no topos E. Neste caso, diz-se que a força φ. Quando Γ é vazio, de modo que a =, lê-se ⊩ φ como "φ é válido em E".
Pode-se mostrar as seguintes regras de semântica de conectivos lógicos.
* U ⊩ φ(a) ∧ ψ(a) se e só se U ⊩ φ(a) e U ⊩ ψ(a).
* U ⊩ φ(a) ∨ ψ(a) se e só se existe epimorfismo ⟨p, q⟩ : V + W → U tal que V ⊩ φ(a ∘ p) e W ⊩ ψ(a ∘ q).
* U ⊩ φ(a) ⇒ ψ(a) se e só se, para cada seta p : V → U tal que V ⊩ φ(a ∘ p), vale V ⊩ ψ(a ∘ p).
* U ⊩ falso(a) se e só se U é objeto inicial.
* U ⊩ (∀ (y : Y), φ(_, y))(a) se e só se, para quaisquer setas p : V → U e β : V → [Y], vale V ⊩ φ(a ∘ p, β).
* U ⊩ (∃ (y : Y), φ(_, y))(a) se e só se existem epimorfismo p : V → U e morfismo β : V → [Y] tais que V ⊩ φ(a ∘ p, β).
* U ⊩ (σ = τ)(a) se e só se [σ] ∘ a = [τ] ∘ a.
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 p ∨ ¬ p).
A seguir, exemplos de interpretações.
* Uma seta f : X → Y é um monomorfismo se e só se ∀ x, ∀ y, f x = f y ⇒ x = y é válido (isto é, f é "internamente injetivo").
* Um topos E satisfaz ∀ (f : X → Y), (∀ y, ∃ x, f x = y) ⇒ ∃ s, ∀ y, f (s y) = y (o "axioma da escolha interno") se e só se, para cada E ∈ E, o functor (_)$^E$ leva epimorfismos a epimorfismos.
* Um objeto de naturais num topos E consiste de morfismos z : 1 → N e s : N → N tais que, para quaisquer morfismos a : 1 → X e b : X → X, existe único morfismo j : N → X tal que j ∘ z = a e j ∘ s = b ∘ j. (Este é o princípio de indução.) Se um topos E 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 E é um topos de Grothendieck Fx(A, J), para a semântica de Kripke–Joyal basta analisar os casos especiais U ⊩ φ(a), onde U é um membro do separador {a y A}$_{A∈A}$. (Aqui, a denota a feixificação.)
Para feixe X, e para x ∈ X(A), denota-se A ⊩ φ(x) quando [φ](x) = t$_A$. (Lembrar que Ω(A) é o conjunto de peneiras fechadas em A, enquanto t$_A$ é a peneira máxima em A.) Isto é equivalente à definição anterior pois X(A) ≅ hom(a y A, X).
Neste caso, existem as regras de manipulações de conectivos lógicos. (Abaixo, x ∈ X(A).)
* A ⊩ φ(x) ∧ ψ(x) se e só se A ⊩ φ(x) e A ⊩ ψ(x).
* A ⊩ φ(x) ∨ ψ(x) se e só se existe cobertura {f$_i$ : A$_i$ → A} tal que, para cada índice i, vale A$_i$ ⊩ φ(x ∘ f$_i$) ou A$_i$ ⊩ ψ(x ∘ f$_i$).
* A ⊩ φ(x) ⇒ ψ(x) se e só se, para cada f : B → A, B ⊩ φ(x ∘ f) implica B ⊩ ψ(x ∘ f).
* A ⊩ ¬ φ(x) se e só se, para cada f : B → A, B ⊩ φ(x ∘ f) implica que a família vazia cobre B.
* A ⊩ (∀ (y : Y), φ(_, y))(x) se e só se, para cada f : B → A e cada b ∈ [Y](B), vale B ⊩ φ(x ∘ f, b).
* A ⊩ (∃ (y : Y), φ(_, y))(x) se e só se existe cobertura {f$_i$ : A$_i$ → A} e existem elementos a$_i$ ∈ [Y](A$_i$) tais que A$_i$ ⊩ φ(x ∘ f$_i$, a$_i$) para cada índice i.

## 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 T é uma categoria pequena de espaços topológicos incluindo ℝ e satisfaz certas propriedades adicionais, então o topos de Grothendieck Fx(T, J) (onde J é a topologia de Grothendieck das coberturas abertas) valida o teorema de continuidade de Brouwer: "todas as funções R → R são contínuas", onde R é o objeto de reais de Dedekind (que neste topos é dado por R := hom(_, ℝ), 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 R é um anel comutativo unitário tal que todo elemento de R que não é invertível é zero, então todo R-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 X um esquema reduzido, e seja F um O$_X$-módulo de tipo finito; então F é localmente finitamente livre num aberto denso. (Mas não o precisa ser em todo o espaço.)