Teoria do tipo intuicionista “mínima”?

Estou surpreso que as pessoas continuem adicionando novos tipos nas teorias de tipos, mas ninguém parece mencionar uma teoria mínima (ou não a consigo encontrar). Eu pensei que os matemáticos amam coisas mínimas, não amam?

Se bem entendi, em uma teoria de tipos com impredicative Prop, a abstração λ e os tipos suff são suficientes. Ao dizer o suficiente, quero dizer que poderia ser usado como lógica intuicionista. Outros tipos podem ser definidos da seguinte maneira:

$$\bot \stackrel{def}{=} \Pi \alpha: Prop. \alpha \\ \neg A \stackrel{def}{=} A \to \bot \\ A \land B \stackrel{def}{=} \Pi C: Prop. (A \to B \to C) \to C \\ A \lor B \stackrel{def}{=} \Pi C: Prop. (A \to C) \to (B \to C) \to C \\ \exists_{x: S}(P(x)) \stackrel{def}{=} \Pi \alpha: Prop. (\Pi x: S. P x \to \alpha) \to \alpha \\ $$

Minha primeira pergunta é: eles ( λ, Π) são realmente suficientes? Minha segunda pergunta é: o que precisamos minimamente se não tivermos um impredicative Prop, como no MLTT? No MLTT, Church / Scott / qualquer codificação não funciona.

Editar: relacionado

Para elaborar os esclarecimentos de gallais, uma teoria de tipos com Prop impredicativo e tipos dependentes pode ser vista como um subsistema do cálculo de construções, tipicamente próximo à teoria de tipos de Church . A relação entre a teoria de tipos da Igreja e o CdC não é tão simples, mas foi explorada, principalmente pelo excelente artigo de Geuvers .

Para a maioria dos propósitos, porém, os sistemas podem ser vistos como equivalentes. Então, de fato, você pode conviver com muito pouco, especialmente se você não estiver interessado em lógica clássica, a única coisa que você realmente precisa é de um axioma do infinito : não é possível no CoC que qualquer tipo tenha mais de um elemento! Mas com apenas um axioma expressando que algum tipo é infinito, digamos um tipo de números naturais com o princípio de indução e o axioma , você pode ir muito longe: a maioria da matemática de graduação pode ser formalizada nesse sistema (tipo, é difícil fazer algumas coisas sem o meio excluído).$0\neq 1$

Sem Prop impredicative, você precisa de um pouco mais de trabalho. Conforme observado nos comentários, um sistema extensional (um sistema com extensionalidade funcional na relação de igualdade) pode obter com apenas e Π -Tipos, B O O G , os vazios e unidade tipos ⊥ e ⊤ , e W-tipos. No cenário intensional, isso não é possível: você precisa de muito mais indutivos. Note-se que para construir W-tipos úteis, você precisa ser capaz de construir tipos por eliminação sobre B o o l assim:$\Sigma$$\Pi$$\mathrm{Bool}$$\bot$$\top$$\mathrm{Bool}$

$$\mathrm{if}\ b\ \mathrm{then}\ \top\ \mathrm{else}\ \bot$$

Para fazer meta-matemática, você provavelmente precisará de pelo menos um universo (por exemplo, para construir um modelo de aritmética de Heyting).

Tudo isso parece muito, e é tentador procurar um sistema mais simples que não tenha a impredicatividade louca do CoC, mas ainda é relativamente fácil de escrever em algumas regras. Uma tentativa recente para fazê-lo é o sistema$\Pi\Sigma$ descrito por Altenkirch et al . Não é totalmente satisfatório, pois a verificação de positividade necessária para consistência não faz parte do sistema "como está". A meta-teoria ainda precisa ser desenvolvida também.

Uma visão geral útil é o artigo A ZF é um hack? de Freek Wiedijk, que na verdade compara os números reais em todos esses sistemas (número de regras e axiomas).

O problema com as codificações da Igreja é que você não pode obter princípios de indução para seus tipos, o que significa que eles são praticamente inúteis quando se trata de provar declarações sobre eles.

Em termos de minimalidade do sistema, um caminho mencionado nos comentários é usar contêineres e tipos (W / M), no entanto, eles são bastante extensivos para que não seja realmente conveniente trabalhar em sistemas como Coq ou Agda.

$\Pi$$\Sigma$$\mu$$\nu$

$\mu$$\nu$