Oi Hermógenes,
Obrigado pelas referências.
Eu, pessoalmente, acho ECQ um princípio *muito* suspeito. O difícil é
> que, sem ECQ, um construtivista ficaria basicamente sem negação (ao
> estilo do cálculo mínimo de Johansson), ou a negação cessaria de ser um
> operador *lógico*. Uma exceção interessante é o caso da "Core Logic" de
> Tennant, onde a negação é dada um caráter lógico, mesmo sem ECQ, pela
> admissão de modus tollendo ponens (ou silogismo disjuntivo) e uma regra
> especial para a implicação que permite obter ¬A,A⊢B. Muitos, porém,
> acham o preço a se pagar muito salgado: falha da transitividade
> (monotonicidade, regra de corte).
>
Existe uma maneira mais construtiva de se definir a negação. Basta
tomar \neg A como 'A não é habitado', usando tipos isso seria dado por uma
equivalência homotopica entre A e empty (não precisa de universos para
fazer isso).
b) Um outro problema é que Martin-Löf explica (reduz) o conceito de
> "prova hipotética" ao conceito de "prova categórica" (sem hipóteses
> abertas).
>
Mas essa parece ser a única opção do ponto de vista construtivista, não?
De uma prova hipotética (acho que o ML usa o termo consequências lógica
para esse operador de inferência) se constrói um mapa que transfere provas
categóricas entre as asserções da prova hipotética. Não consigo ver outra
opção.
> Martin-Löf, no artigo de fundamentação filosófica da sua Teoria dos
> Tipos[7], assume que as regras de introdução dão o significado das
> constantes lógicas e, a partir daí, justifica as regras de eliminação.
> Isto demonstra, em terminologia corrente, a correção da lógica
> intuicionista (como sistema formal) com respeito a uma fundamentação
> baseada nas introduções (estilo BHK). Contudo, a contrapartida (a
> questão se todos os princípios de raciocínio justificáveis são de fato
> deriváveis intuicionisticamente), isto é, completude, em terminologia
> corrente, permanece em aberto no artigo, pois Martin-Löf não oferece
> nenhum argumento em seu favor. Os resultados mencionados
> anteriormente mostram que, sob certas condições que parecem razoáveis
> de um ponto de vista construtivo, uma fundamentação estilo BHK, quando
> formulada precisamente (uma vez que BHK é uma espécia de fundamentação
> (semântica) informal), justificaria inferências que não são
> intuicionisticamente deriváveis.
>
Esse é exatamente o ponto que eu queria levantar!
> Na minha opinião, o potencial explanatório e de fundamentação da
> Teoria Intuicionista de Tipos (TIT) se estraçalha a partir do momento
> que se introduz universos. A partir daí, me parece, a TIT assume um
> caráter fortemente ad hoc e muitas da intuições iniciais vão para o
> espaço. Neste ponto, a única vantagem de TIT em comparação à ZF (sua
> concorrente igualmente ad hoc), principalmente se você é um computeiro
> ou matemático preocupado com computabilidade, é o fato de TIT ser
> construtiva. Por outro lado, os argumentos de que ZF seria
> filosoficamente mais robusta e conceitualmente mais coerente (ver, por
> exemplo, Harvey Friedman na FOM) não me convencem. Acontece que, dado
> que ZF é a doutrina ortodoxa, estamos acostumados a fazer vista grossa
> para as aberrações em ZF e maldizer excessivamente qualquer
> idiossincrasia de propostas alternativas, como TIT.
>
O problema que citei ('A true' =' 'A true' true' do ponto de vista
epistêmico) não tem relação com universos (eu não devia ter citado universo
no meu comentário) , apesar de ser mais fácil de internalizar o juízo 'A
true' nas proposições usando universos, i.e., enche o saco escrever a
definição de uma equivalência homotópica para definir 'A é habitado'.
Também acho que a definição de universo univalente é bem intuitiva e
consistente com a pratica matemática. O universo é só um objeto a mais na
teoria que mostra a compatibilidade da identidade com a equivalência
homotópica. Eles fazem o mesmo papel dos V_{\kappa}. E como a TIT deve ser
semântica e sintática ao mesmo tempo, acho natural colocar um universo (ou
melhor, uma estratificação em universos) na teoria. Gostaria, portanto, de
entender o que gera essa tal destruição do potencial explanatório da TIT.
> De qualquer maneira, mesmo num contexto muito elementar, abordar o
> intuicionismo, ou construtivismo, de um ponto de vista epistemológico,
> tal como Martin-Löf faz, me parece um equívoco. Concordo ainda que a
> discussão epistemológica de Martin-Löf em conexão com a fundamentação
> da sua Teoria de Tipos é muito confusa, para se dizer o mínimo.
>
Brouwer não fazia a mesma coisa? Aquela idéia de matemático ideal no
tempo me soa bem similar.
Abs,
Fernando Yamauti
--
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAJGvw-19d0%3Db6VKYJD_-ybq_K33O6tVF-H8Ru9ijEkCaPtkb%3Dw%40mail.gmail.com.
