Teoria dos tipos e matemática construtivista com lógica paraconsistente?
A teoria dos tipos, junto com a correspondência de Curry-Howard, é um sistema formal para apresentar provas formais da lógica intuicionista, que é usado na matemática construtiva. A lógica intuicionista difere da lógica clássica por não ter a lei do meio excluído como um axioma lógico / regra de derivação. Mas tem o princípio de explosão: a partir de uma prova de falso, qualquer coisa pode ser derivada. Existe uma tentativa séria de estudar o que pode e não pode ser provado dentro da matemática se alguém adotar a lógica intuicionista e abandonar o axioma de que qualquer coisa pode ser derivada de uma prova do falso?
Respostas
Em geral, há tentativas iniciais credíveis de estudar aspectos da matemática no contexto de cálculos paraconsistentes (há muitos, basta olhar para o livro texto do ToC of Priest ).
Dito isso, a resposta para a pergunta precisa que você realmente fez, aquela sobre a teoria dos tipos, é negativa.
Na teoria dos tipos (como na maioria dos sistemas fundamentais), a declaração $0=1$ é naturalmente explosivo, no sentido de que você pode provar qualquer coisa usando $0=1$ sem nunca invocar $\bot$-eliminação. Por quê? Como na minha resposta à sua outra pergunta sobre a teoria dos tipos, determinados tipos$A,B$, você pode usar $\mathbb{N}$-indução para construir uma função $f: \mathbb{N} \rightarrow \mathcal{U}$ de tal modo que $f(0)$ reduz a $A$ e $f(Sn)$ reduz a $B$. Aplicando a regra de congruência a$0=1$ rendimentos $A = B$, então todos os tipos são iguais e, em particular $A \rightarrow B$detém. Na verdade, a teoria de tipo de Martin-Löf é maximamente explosiva: se você pode habitar um tipo$T$ no contexto vazio sem usar $\bot$-eliminação, uma indução na estrutura da prova mostra que você poderia ter habitado o tipo $T^{\bot \leftarrow 0=1}$, o tipo obtido de $T$ substituindo cada ocorrência de $\bot$ com $0=1$. Não há nada específico sobre$0=1$ aqui: a teoria do tipo Martin-Löf sem explosão é realmente apenas um mundo onde $\bot$denota uma proposição arbitrária. Em particular, se$A$ não menciona $\bot$, então MLTT sem explosão prova $A \rightarrow \bot$ precisamente se $A$ é explosivo.
Isso significa que, desde que você não pretenda adicionar novos princípios classicamente inadmissíveis, não há muito sentido em estudar essas teorias de tipo "mínimo" com base na lógica mínima. A situação é mais interessante, por exemplo, na variante da aritmética de Heyting que usa lógica mínima em vez da lógica intuicionista como seu substrato lógico. Esta teoria é quase, mas não exatamente, a mesma que a aritmética de Heyting intuicionista completa, uma vez$0=1$ é explosivo.
Por exemplo, se você quiser provar usando $0=1$ que cada número é par, você pode multiplicar a igualdade inconsistente por $2$ para obter $0=2$, aplique transitividade para obter $1=2$, então substitua $1$ com $2$ dentro $\forall x. 1x = x$ concluir $\forall x. 2x=x$, e depois $\forall x. \exists y. 2y=x$. Você pode fazer isso sistematicamente (por indução na estrutura da fórmula$A$) para provar que $0 = 1 \rightarrow A$.
Desta vez, o inverso não é válido, e a aritmética de Heyting formulada na lógica mínima não é maximamente explosiva: há afirmações positivas que se prova falsas, mas que não são explosivas. Isso porque um dos axiomas da aritmética de Heyting diz algo não trivial sobre$\bot$. Existem duas maneiras de concluir$\bot$ na aritmética de Heyting:
De um axioma de indução. Isso não é um problema: quando você substitui todas as ocorrências de$\bot$ com $0=1$em um axioma de indução, o resultado é outro axioma de indução. (Este é o único caso em MLTT, e é por isso que justifica a explosão.)
Aplicando o axioma não lógico $\forall x. 0 = Sx \rightarrow \bot$ para alguns $St = 0$. O problema é que você não pode substituir este axioma por$\forall x. 0 = Sx \rightarrow 0 = 1$: é preciso algum trabalho para mostrar que isso realmente não pode ser feito: acontece que $0 = 2$ não implica comprovadamente $0=1$se você formular a aritmética de Heyting dentro da lógica mínima. Para obter detalhes, você pode consultar a tese de mestrado da Heerkens .
Este é, no entanto, o único obstáculo: você substitui $\forall x. 0 = Sx \rightarrow \bot$ com $\forall x. 0 = Sx \rightarrow 0 = 1$, e você obtém uma aritmética mínima que coincide perfeitamente com a aritmética de Heyting intuicionista. Pode-se argumentar que esse axioma modificado é filosoficamente justificado puramente com base no que queremos que a aritmética seja.