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.^[1]

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

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.^[4]

Definição

Na linguagem, termos são classificadas de acordo com tipos. A família dos tipos é definida recursivamente a seguir.^[5]

Cada tipo básico $T i, \dots$ (de uma família previamente escolhida) é um tipo.
Se $A$ e $B$ são tipos, então $A \times B$ e $A \to 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 \times B] = [A] \times [B]$ (o produto categorial), $[A \to B] = [B] [A]$ (o objeto exponencial), $[1]$ é o objeto terminal e $[Ω]$ é o classificador de subobjetos.^[5]

Um contexto é uma sequência finita de tipos; denota-se um contexto por $Γ := x 1 : A 1, \dots, 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] \times \dots \times [A n]$ , como produto das interpretações dos tipos constituintes.^[5]

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 \to B$ é bem formado.
Se $Γ ⊢ f : C \to 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 \times B$ é bem formado.
Se $Γ ⊢ e : A \times 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 \to T$ (numa família previamente escolhida), $Γ ⊢ h : S \to T$ é bem formado.^[5]^[6]

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

Supõe-se que toda constante dada $h : S \to T$ recebe interpretação $[h] : [S] \to [T]$ como morfismo em $E$ . Então, cada sequente bem formado $Γ ⊢ e : B$ recebe interpretação como morfismo $[Γ] \to [B]$ , dada recursivamente.

$[x 1 : A 1, \dots, x n : A n ⊢ x i : A i]$ é a projeção $[A 1] \times \dots \times [A n] \to [A i]$ .
$[Γ ⊢ λ (x : C). e : C \to B]$ é o morfismo $[Γ] \to [B] [C]$ transposto de $[Γ, x ⊢ e] : [Γ] \times [C] \to [B]$ pela adjunção exponencial.
$[Γ ⊢ f x] := ap \circ ([Γ ⊢ f], [Γ ⊢ x])$ , onde $ap : [B] [C] \times [C] \to [B]$ é como na adjunção exponencial.
$[Γ ⊢ () : 1] := () : [Γ] \to 1$ .
$[Γ ⊢ (a, b)] := ([Γ ⊢ a], [Γ ⊢ b])$ .
$[Γ ⊢ p 1 e] := p 1 \circ [Γ ⊢ e]$ ; similarmente à segunda projeção.
$[Γ ⊢ (a = b)] := [=] \circ ([Γ ⊢ a], [Γ ⊢ b])$ , onde $[=] : [A] \times [A] \to Ω$ é morfismo característico de $(id, id) : [A] \to [A] \times [A]$ .
$[Γ ⊢ h] := h^\circ ()$ , onde $h^: 1 \to [T] [S]$ é transposto de $[h] \circ p 2 : 1 \times [S] ≅ [S] \to [T]$ .^[5]^[6]

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 \land q := ((p, q) = (vero, vero))$ .
$\forall (x : A), p := ((λ (x : A), p) = (λ (x : A), vero))$ , onde $p$ pode mencionar $x$ .
$falso := \forall (p : Ω), p$ .
$p \Rightarrow q := (p = p \land q)$ .
$\neg p := p \Rightarrow falso$ .
$p \lor q := \forall (r : Ω), (p \Rightarrow r) \Rightarrow ((q \Rightarrow r) \Rightarrow r)$ .
$\exists (x : A), p := \forall (r : Ω), (\forall (x : A), p \Rightarrow r) \Rightarrow r$ , onde $p$ pode mencionar $x$ .

Se $Γ$ é um contexto e $Γ ⊢ φ i : Ω$ são sequentes bem formados, escreve-se

Γ | φ 1, \dots, φ n ⊢ φ 0

quando $m 1 \cap \dots \cap m n \subseteq m 0$ , onde $m i$ é o subobjeto associado a $[Γ ⊢ φ i] : [Γ] \to Ω$ . Com isso, pode-se mostrar que valem as regras usuais da lógica intuicionística de predicados.^[1]

Semântica de Kripke–Joyal

Dado sequente bem formado $Γ ⊢ φ : Ω$ , e dado morfismo $a : U \to [Γ]$ , escreve-se

a ⊩ φ

ou

U ⊩ φ (a)

quando $[Γ ⊢ φ] \circ a = vero \circ ()$ , onde $vero : 1 \to Ω$ é 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$ ".^[7]^[1]

Pode-se mostrar as seguintes regras de semântica de conectivos lógicos.

$U ⊩ φ (a) \land ψ (a)$ se e só se $U ⊩ φ (a)$ e $U ⊩ ψ (a)$ .
$U ⊩ φ (a) \lor ψ (a)$ se e só se existe epimorfismo $⟨ p, q ⟩ : V + W \to U$ tal que $V ⊩ φ (a \circ p)$ e $W ⊩ ψ (a \circ q)$ .
$U ⊩ φ (a) \Rightarrow ψ (a)$ se e só se, para cada seta $p : V \to U$ tal que $V ⊩ φ (a \circ p)$ , vale $V ⊩ ψ (a \circ p)$ .
$U ⊩ falso(a)$ se e só se $U$ é objeto inicial.
$U ⊩ (\forall (y : Y), φ (_, y))(a)$ se e só se, para quaisquer setas $p : V \to U$ e $β : V \to [Y]$ , vale $V ⊩ φ (a \circ p, β)$ .
$U ⊩ (\exists (y : Y), φ (_, y))(a)$ se e só se existem epimorfismo $p : V \to U$ e morfismo $β : V \to [Y]$ tais que $V ⊩ φ (a \circ p, β)$ .
$U ⊩ (σ = τ)(a)$ se e só se $[σ] \circ a = [τ] \circ 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 \lor \neg p$ ).^[7]

A seguir, exemplos de interpretações.

Uma seta $f : X \to Y$ é um monomorfismo se e só se $\forall x, \forall y, f x = f y \Rightarrow x = y$ é válido (isto é, $f$ é "internamente injetivo").^[8]
Um topos $E$ satisfaz $\forall (f : X \to Y), (\forall y, \exists x, f x = y) \Rightarrow \exists s, \forall y, f (s y) = y$ (o "axioma da escolha interno") se e só se, para cada $E \in E$ , o functor $(_) E$ leva epimorfismos a epimorfismos.^[7]
Um objeto de naturais num topos $E$ consiste de morfismos $z : 1 \to N$ e $s : N \to N$ tais que, para quaisquer morfismos $a : 1 \to X$ e $b : X \to X$ , existe único morfismo $j : N \to X$ tal que $j \circ z = a$ e $j \circ s = b \circ 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.^[9]

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 \in A$ . (Aqui, $a$ denota a feixificação.)

Para feixe $X$ , e para $x \in 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)$ .^[4]

Neste caso, existem as regras de manipulações de conectivos lógicos. (Abaixo, $x \in X (A)$ .)

$A ⊩ φ (x) \land ψ (x)$ se e só se $A ⊩ φ (x)$ e $A ⊩ ψ (x)$ .
$A ⊩ φ (x) \lor ψ (x)$ se e só se existe cobertura ${f i : A i \to A}$ tal que, para cada índice $i$ , vale $A i ⊩ φ (x \circ f i)$ ou $A i ⊩ ψ (x \circ f i)$ .
$A ⊩ φ (x) \Rightarrow ψ (x)$ se e só se, para cada $f : B \to A$ , $B ⊩ φ (x \circ f)$ implica $B ⊩ ψ (x \circ f)$ .
$A ⊩ \neg φ (x)$ se e só se, para cada $f : B \to A$ , $B ⊩ φ (x \circ f)$ implica que a família vazia cobre $B$ .
$A ⊩ (\forall (y : Y), φ (_, y))(x)$ se e só se, para cada $f : B \to A$ e cada $b \in [Y](B)$ , vale $B ⊩ φ (x \circ f, b)$ .
$A ⊩ (\exists (y : Y), φ (_, y))(x)$ se e só se existe cobertura ${f i : A i \to A}$ e existem elementos $a i \in [Y](A i)$ tais que $A i ⊩ φ (x \circ f i, a i)$ para cada índice $i$ .^[4]

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 \to 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).^[10]

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.)^[11]

Referências

↑ ^a ^b ^c (Streicher 2004, §13)
↑ Mitchell, William (1972). «Boolean topoi and the theory of sets». Journal of Pure and Applied Algebra. doi:10.1016/0022-4049(72)90006-0
↑ Pierre, Cartier (1979). «Logique, catégories et faisceaux». Séminaire Bourbaki (513). Zbl 0406.03074
↑ ^a ^b ^c (Mac Lane & Moerdijk 1992, §VI.7)
↑ ^a ^b ^c ^d ^e (Streicher 2004, §11.2)
↑ ^a ^b (Mac Lane & Moerdijk 1992, §VI.5)
↑ ^a ^b ^c (Mac Lane & Moerdijk 1992, §VI.6)
↑ (Mac Lane & Moerdijk 1992, exercício VI.10)
↑ (Mac Lane & Moerdijk 1992, §VI.8)
↑ (Mac Lane & Moerdijk 1992, §VI.9)
↑ (Blechschmidt 2017, §II.5)

Bibliografia

Mac Lane, Saunders; Moerdijk, Ieke (1992), Sheaves in Geometry and Logic: A First Introduction to Topos Theory, ISBN 978-0-387-97710-2, Universitext 1 ed. , Springer
Streicher, Thomas (2004), Introduction to Category Theory and Categorical Logic (PDF), consultado em 12 de fevereiro de 2021
Blechschmidt, Ingo (2017), Using the internal language of toposes in algebraic geometry (PDF) (tese), consultado em 3 de março de 2021