Fernando Yamauti <fgyama...@gmail.com> escreveu:
> Oi Hermógenes,
Olá, Fernando.
> 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).
Sim, claro. Em termos lógicos, essa é exatamente a definição padrão de
¬A como A→⊥. Como você observou, meu comentário acima realmente não diz
respeito a universos. Estava comentando o seu incômodo com o fato de
A→B ser construtivamente válido quando A é falso (quando temos ¬A). Eu
havia observado que esse seu incômodo também aparece na literatura
construtivista, especialmente em conexão com objeções à ECQ.
Note que a definição ¬A≡A→⊥ não é suficiente para definir a negação, mas
apenas define a negação em termos de ⊥. É necessário ainda caracterizar
⊥. O princípio construtivista padrão que caracteriza ⊥ é ECQ. A
inferência que incomodava (¬A,A⊢B) é obtida por modus ponens e ECQ. Um
construtivista que queira rejeitá-la, portanto, teria que rejeitar modus
ponens ou ECQ. O candidato mais óbvio é ECQ. Daí, eu comentei sobre
algumas propostas "construtivas" que rejeitam ECQ.
Espero que agora tenha ficado mais claro (há alguns detalhes adicionais
na minha resposta ao João Marcos).
> 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.
Uma outra opção seria trabalhar exclusivamente com deduções (provas
hipotéticas), sem reduzí-las a provas categóricas. É importante
observar que provas categóricas são um caso particular de deduções
(provas hipotéticas). A circularidade pode ser evitada por meio dos
conhecidos argumentos envolvendo harmonia (normalização, canonicidade)
que já servem de base para as propostas atuais reducionistas (estilo
Martin-Löf).
Em poucas palavras, o que quero dizer é o seguinte: Por que o mapa
transfere, necessariamente, provas *categóricas* das hipóteses? Por que
não mapear provas *hipotéticas* das hipóteses, isto é, por que não
considerar também deduções baseadas em hipóteses, das quais as provas
categóricas (fechadas) são apenas um caso particular?
Normalização vale para *deduções*, não somente para "provas" fechadas!
Ademais, se temos uma fundamentação baseadas em deduções (a partir de
hipóteses) em vez de provas categóricas (fechadas), desaparece todo o
problema filosófico de se explicar a correção de certas inferências por
apelo à impossíveis provas categóricas do absurdo.
Agora, poderia uma proposta assim ser considerada "construtivista" ou
"intuicionista"? Depende do que se entende por "construtivismo" ou
"intuicionismo". Se o critério aqui é BHK juntamente com o ponto de
vista epistemológico de Martin-Löf, é provável que a resposta seja
"Não". Mas, se abordamos o intuicionismo por meio de um inferencialismo
apoiado tecnicamente nos trabalhos de Gentzen, a resposta talvez seja
"Sim".
BHK está morta! Longa vida ao inferencialismo gentzeniano! :-)
> 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'.
Hum... Não consigo ver uma maneira de fazê-lo sem universos. Poderia me
fornecer detalhes? Pode ser em privado, se você preferir.
É possível ainda que eu não tenha compreendido muito bem o seu
comentário.
> 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.
O principal problema com os universos é que eles borram a distinção
entre os juízos "A é um tipo" e "x tem o tipo A" (i.e. A é habitado).
Na presença de universos, o juízo "B é um tipo" se reduz a um juízo da
forma "x tem o tipo A" ou "x é um termo do tipo A", onde A é um
universo. Tecnicamente, isso pode até ser muito conveniente, mas,
filosoficamente, é desastroso.
Sem me alongar muito, creio que a gravidade do problema pode ser
depreendida de uma leitura atenta e refletiva do artigo de fundamentação
do Martin-Löf[1]. Ali, ele discorre sobre a importância em se
distinguir entre os juízos "A prop" ("A é um tipo", pois ali o único
tipo tratado é o tipo das proposições) e "A true" ("x tem o tipo A", "o
tipo proposicional A é habitado", "x é uma prova de A"). Esta distinção
me parece importantíssima para o funcionamento da teoria como
fundamentação filosófica. Quando se introduz universos, toda as
intuições e coerência filosófica que estavam apoiadas nesta distinção
vão para o espaço.
Qual seria o valor como fundamentação filosófica de uma teoria
construtiva se, todas as vezes que efetuo uma construção com base nos
princípios básicos da teoria, tenho que verificar, *caso a caso*, se as
construções são bem tipadas sob pena de inconsistência?
A justificativa para a adição de universos é basicamente ad hoc: por que
eles são necessários para se fazer matemática para além da
aritméticazinha de primeira ordem. Nesse sentido, TIT+universos não me
parece menos ad hoc do que ZF. Eu, particularmente, tenho a impressão
de que a introdução irrestrita de universos é a maneira dos
construtivistas de jogar a toalha, após o que Martin-Löf chamou de
"segundo fracasso do programa de Hilbert"[2].
Agora, pode ser que universos sejam intuitivos e essenciais de um ponto
de vista homotópico, mas, até o momento, a aspiração da Teoria
Homotópica dos Tipos (THT) como fundamentação alternativa para a
matemática está apoiada na Teoria Intuicionista de Tipos adjacente, uma
vez que, até o momento, como você mesmo observou, as tentativas de
oferecer explicações e justificativas para os elementos básicos da
teoria por vias diretamente homotópicas, contornando a teoria de tipos,
são insatisfatórias.
> 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.
Brouwer não fazia a mesma coisa. Fazia muito pior!
De qualquer maneira, não considero Brouwer, Heyting, Martin-Löf, ou
qualquer outro, como donos do intuicionismo. Creio que há razões para
ser um intuicionista ou construtivista que independe da exegese desses
autores.
Referências:
[1] Per Martin-Löf. On the Meanings of the Logical Constants and the
Justifications of the Logical Laws. Nordic Journal of Philosophical
Logic 1 (1), 11-60, 1996.
(disponível em https://github.com/michaelt/martin-lof)
[2] Per Martin-Löf. The Hilbert-Brouwer Controversy Resolved? In: One
Hundred Years of Intuitionism (1907-2007), 243-256, 2008.
(disponível em https://github.com/michaelt/martin-lof)
--
Hermógenes Oliveira
--
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/87fuhkilsk.fsf%40camelot.oliveira.
