Joao Marcos <botoc...@gmail.com> escreveu: >> 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*. > > Por quê, Hermógenes?
Bem, o problema é o que colocar no lugar de ECQ que, ao mesmo tempo, (1) seja razoável se chamar de "negação" (ou, melhor, "absurdo", no caso da negação definida pelo absurdo), e (2) seja construtivamente justificável. Se permanecemos com a negação definida como ¬A≡A→⊥ *e não colocamos nada no lugar de ECQ*, então as nossas inferências dedutivas corretas são exatamente aquelas do fragmento mínimo sem negação e, do ponto de vista inferencial, não é possível distinguir o absurdo (⊥) de outra sentença qualquer: nós basicamente não teríamos a negação no âmbito das inferências lógicas. Obviamente, poderiamos ainda introduzir uma noção de incompatibilidade entre sentenças e, mantendo apenas as regras de inferência do fragmento mínimo, tratar a negação no âmbito extra-lógico: a negação deixa de ser um operador lógico (se entendemos por lógica apenas aquilo que está sendo capturado pelas nossas regras de inferência). Espero que agora esteja mais claro. Ou você estaria perguntando o porquê de eu achar ECQ um princípio suspeito? >> 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. > > E o que dizer do conectivo nulário de absurdo, que não possui regra > de introdução? Bem, segundo Martin-Löf, há uma regra de introdução para o absurdo (⊥): sob nenhuma circunstância podemos introduzir o absurdo (⊥). Isto é uma regra de introdução no sentido em que diz algo sobre as circunstâncias em que teríamos uma prova do absurdo (similar à cláusula BHK para o absurdo). Daí, ele justifica ECQ como regra de eliminação usando, inclusive, um exemplo não muito convincente envolvendo um chapéu. :-o 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) -- 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/87k26wimgm.fsf%40camelot.oliveira.
