Bruno Bentzen <b.bent...@hotmail.com> escreveu: > Oi Hermógenes,
Olá, Bruno. > [...] > > PS: Posso estar enganado, mas acho um pouco equivocado e confuso usar > a palavra “completude” (um termo de cunho técnico ou meta-matemático) > neste caso quando estamos nos tratando de uma semântica informal ou > justificativa filosófica (até onde sei, o estudo de semânticas formais > para a lógica intuicionista nunca foi uma das preocupações principais > do Martin-Löf). De qualquer forma, não vejo porque as explicações de > significado não seriam “completas”, no sentido informal, para a MLETT, > que, repito, é a única das duas vertentes tradicionais de sua teoria > de tipos que interessa ao intuicionista. Você está correto em observar que as explicações semânticas de Martin-Löf não foram propostas como uma semântica formal e que o estudo de semânticas formais não tem lugar no espectro da obra dele. Porém, a questão da adequação das explicações semânticas pode ser levantada também no âmbito informal, como tentei indicar na minha mensagem original. Nas suas explicações semânticas, Martin-Löf toma as regras de introdução como primitivas (como aquelas que conferem significado às constantes lógicas) e justifica as regras de eliminação com base nelas. Se as regras de eliminação também fossem consideradas primitivas, ele não teria porquê se dar o trabalho de justificá-las com base nas regras de introdução. A questão agora surge: Será que as regras de eliminação justificadas por Martin-Löf são, de fato, as regras mais fortes que podem ser justificadas, tomando como base as regras de introdução? Isto é, seria possível fornecer regras de eliminação mais fortes que também sejam justificadas com base nas regras de introdução? Como se trata de uma semântica (explicação, fundamentação) informal, esta questão não pode ser respondida, no caso de Martin-Löf, com um teorema. Mas isso não significa que a questão é inócua ou desimportante, e, certamente, é uma questão que não pode ser afastada simplesmente sob o pretexto de que a semântica é informal. Martin-Löf fornece uma justificação, informal, obviamente, para as suas regras de eliminação (suas regras de eliminação estão *corretas*). Mas, é perfeitamente razoável se perguntar se haveriam outras regras de eliminação que pudessem ser justificadas e que resultariam numa lógica diferente da lógica intuicionista, que é a lógica alvo da semântica informal em questão. O que, com respeito a Martin-Löf, é um mero questionamento informal, se torna, no caso de Prawitz, uma conjectura[1], pois Prawitz, ainda que num estilo similar ao de Martin-Löf, fornece definições rigorosas que resultam, de fato, numa semântica formal. A conjectura de Prawitz é justamente uma versão formal da questão que estou discutindo: Seriam as regras de eliminação padrões as regras mais fortes que podem ser validadas do ponto de vista das regras de introdução? Os resultados que mencionei anteriormente sugerem que a resposta a essa conjectura possa ser "não". E, como esses resultados negativos incluem mesmo contraexemplos, é fácil traduzir os contraexemplos na forma de justificativas informais nos termos de semânticas informais como BHK e as explicações semânticas de Martin-Löf. De fato, eu já forneci a você, em conversa privada, uma justificativa informal em termos de BHK de uma inferência que não é intuicionisticamente derivável. Eu entendo a objeção que faz ao meu uso do *termo* "completude" no contexto de Martin-Löf, mas espero que tenha conseguido deixar claro que o uso que fiz de "completude" e "correção" naquele contexto se referia à *adequação* das explicações semânticas de Martin-Löf ao sistema de regras de inferência dedutivas que conhecemos como lógica intuicionista. Esta questão da adequação é legítima, não importa o quão informal seja a sua fundamentação (explicação, semântica). Gostaria ainda de deixar claro que estas minhas observações não afetam em nada a *utilidade* da TIT como teoria matemática e o fato de que suas propriedades construtivas, concordo com a Valéria nesse ponto, podem ser razões mais do que suficientes para favorecê-la em detrimento de ZF. Referências: [1] Dag Prawitz. An Approach to General Proof Theory and a Conjecture of a Kind of Completeness of Intuitionistic Logic Revisited. In: Advances in Natural Deduction, 269-279, 2014. -- 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/874ly0e5sz.fsf%40camelot.oliveira.
