Ramificação de uma teoria impredicativa do tipo

A maioria das teorias de tipos que conheço são predicativas, pelo que quero dizer que

Void : Prop
Void = (x : Prop) -> x

não é bem digitado na maioria dos provadores de teoremas, pois esse tipo pi pertence ao mesmo universo Prope não é o caso Prop : Prop. Isso os torna predicativos e não permite definições impredicativas como as anteriores. No entanto, muitas "linguagens do quadro-negro", como o Sistema F ou o CoC, são de fato impredicativas. De fato, essa impredicatividade é vital para definir a maioria das construções não incluídas primitivamente na linguagem.

Minha pergunta é: por que alguém desejaria desistir da impredicatividade, dado seu poder na definição de construções lógicas? Ouvi algumas pessoas observando que impredicatividade estraga "computação" ou "indução", mas estou tendo problemas para encontrar uma explicação concreta.

Vou elaborar meus comentários em uma resposta. As origens da teoria do tipo predicativo são quase tão antigas quanto a própria teoria do tipo, uma vez que uma das motivações de Russel era proibir definições "circulares" que foram identificadas como parte da fonte das inconsistências e paradoxos do século XIX. Thierry Coquand fornece uma visão geral esclarecida aqui . Nessa teoria, os predicados sobre um "nível" ou tipo pertencem aos tipos do nível "próximo", onde há um número infinito (contável) de níveis.

Embora a hierarquia predicativa de Russel fosse (aparentemente) suficiente para descartar os paradoxos conhecidos, ela se mostrou muito difícil de usar como sistema fundamental. Em particular, definir mesmo algo tão simples quanto o sistema de números reais era extremamente difícil e, portanto, Russel postulou um axioma, o Axioma da Redutibilidade, que postulava que todos os níveis eram "reduzidos" a um. Escusado será dizer que este não foi um desenvolvimento satisfatório.

No entanto, ao contrário das declarações impredicativas "prejudiciais" (como a compreensão irrestrita), esse axioma não parecia apresentar nenhuma inconsistência. As formulações subsequentes das teorias fundamentais ( teoria dos tipos simples , a teoria dos conjuntos de Zermelo ) as aceitaram por atacado, transformando famílias de predicados (quantificando possivelmente todo o universo de conjuntos), predicados no mesmo nível.

Por volta de 1971, Martin-Löf introduziu a teoria do tipo dependente, na qual esse princípio e o axioma adicional se Type : Typemantêm. Esse sistema acabou sendo inconsistente por razões sutis: o paradoxo ingênuo de Russel não pode ser reproduzido (de maneira direta), mas uma codificação inteligente, no entanto, permite encontrar uma contradição. Isso levou a uma crise de fé semelhante à de Russel, resultando na teoria do tipo predicativo com universos que conhecemos e amamos.

Existe uma maneira de reparar a teoria para permitir impredicativo "inocente" a la teoria dos conjuntos Zermelo, resultando em teorias do tipo como o Cálculo de Construções, mas o estrago estava feito, e a "escola sueca" da teoria tipo tende a rejeitar impredicativo.

Vários pontos:

1. O que isso tem a ver com a matemática intuicionista? A resposta não é muita. Na virada do século XX, os matemáticos tendiam a confundir o uso de princípios circulares / impredicativos com o raciocínio não construtivo (a intuição é que o raciocínio impredicativo parece assumir um universo matemático preexistente , assim como os usos do meio excluído). No entanto, existem teorias impredicativas perfeitamente intuicionistas (como a IZF ). Pessoas interessadas em intuicionismo ainda tendem a se interessar em predicativismo por algum motivo (sou culpado disso, é claro).

2. O que você pode fazer em matemática predicativa? Como Martin aponta em sua resposta, Hermann Weyl (que não deve ser confundido com Andre Weil) iniciou um programa que tentou explorar o poder expressivo dos sistemas predicativos, tomando como ponto de partida que os sistemas predicativos eram de força expressiva entre a Aritmética Peano e a Segunda Ordem. Aritmética , que é bastante aceita como impredicativa pela maioria dos padrões (e é comparável ao Sistema F no lado da teoria dos tipos). O programa foi posteriormente apelidado de "matemática reversa", pois tentava classificar a força dos teoremas matemáticos conhecidos em termos dos axiomas necessários para prová-los (o inverso da abordagem usual). oa página da Wikipedia fornece uma boa visão geral; o programa foi bastante bem-sucedido, pois a maior parte da matemática do século XIX pode ser facilmente acomodada em sistemas muito fracos. Ainda é uma questão em aberto se esse programa pode ser dimensionado para resultados mais recentes, digamos, na teoria das categorias mais altas (a suspeita é que a resposta seja "sim, com grande esforço").

Uma dimensão é a inferência de tipo. A inferência de tipo do sistema F, por exemplo, não é decidível, mas alguns de seus fragmentos predicativos têm inferência de tipo decidível (parcial).

Outra dimensão é a consistência como lógica. Pensadores distintos historicamente se sentiram um pouco enjoados por ter fundamentos impredicativos da matemática. Afinal, é uma forma de raciocínio circular. Acho que H. Weyl pode ter sido o primeiro ou, um dos primeiros, que tentou reconstruir o máximo de matemática possível de uma maneira predicativa ... apenas para estar do lado seguro. Aprendemos que as circularidades da impredicatividade não são problemáticas na matemática clássica, no sentido de que nenhuma contradição jamais foi derivada de definições impredicativas 'mansos'. Com o tempo, aprendemos a confiar neles. Note que isso (ausência de paradoxa) é um empíricoobservação! No entanto, grande parte do desenvolvimento da teoria da prova, com suas estranhas construções ordinais, tem como objetivo final o desejo de construir toda a matemática 'de baixo', isto é, sem definições impredicativas. Este programa não está completo. Nos últimos anos, o interesse em fundamentos preditivos da matemática mudou de preocupações com paradoxa para o conteúdo computacional de provas, o que é interessante por várias razões. Acontece que definições impredicativas dificultam a extração de conteúdo computacional. Outro ângulo na preocupação com a consistência vem da tradição Curry-Howard. A teoria do tipo original de Martin-Löf era impredicativa ... e doentia. Após esse choque, ele propôs apenas sistemas predicativos, mas combinado com tipos de dados indutivos para recuperar grande parte do poder da impredicatividade.

As teorias de tipo tendem à predicatividade principalmente por razões sócio-técnicas.

Primeiro, o conceito informal de impredicatividade pode ser formalizado de (pelo menos) duas maneiras diferentes. Primeiro, dizemos que uma teoria de tipos como o Sistema F é impredicativa porque a quantificação de tipos pode variar em todos os tipos (incluindo o tipo ao qual o quantificador pertence). Assim, podemos definir operadores genéricos de identidade e composição:

No entanto, observe que na teoria de conjuntos padrão (por exemplo, ZFC), essas operações não são definíveis como objetos . Não existe "a função de identidade" na teoria dos conjuntos, porque uma função é uma relação entre um conjunto de domínios e um conjunto de códigos, e se uma única função puder ser a função de identidade, você poderá usá-la para construir um conjunto de todos os conjuntos. (Foi assim que John Reynolds mostrou que o polimorfismo no estilo System-F não tinha modelos teóricos dos conjuntos.)

$X$$S$$P$$X$$P$$X$

Portanto, a impredicatividade do estilo F é incompatível com uma visão ingênua dos tipos como conjuntos. Se você estiver usando a teoria dos tipos como um assistente de prova, é bom poder portar matemática padrão facilmente para sua ferramenta, e assim a maioria das pessoas que implementa esses sistemas simplesmente remove a impredicatividade. Dessa forma, tudo tem uma leitura teórica e teórica, e você pode interpretar os tipos da maneira que for mais conveniente para você.