Viva, Hermógenes: Obrigado pela resposta.
>>> 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. Por um lado, vale notar que há sim uma maneira neste caso de distinguir a negação, vista como um conectivo com interpretação parcialmente não-determinística aplicada a uma outra sentença qualquer (note-se que a negação de uma sentença falsa é perfeitamente determinística, usando a definição acima; o "problema" está apenas na negação de sentenças verdadeiras), de uma sentença atômica arbitrária: note com efeito que a regra de substituição uniforme não se aplica ao símbolo de absurdo, como um *conectivo* nulário, tal como se aplica a sentenças atômicas. Por outro lado, não vejo porque deveríamos pensar sempre na negação como conectivo *derivado*. Aliás, isto parece até uma ideia bem ruinzinha, do ponto de vista de lógicas não-clássicas em que a interdefinibilidade entre conectivos clássicos usualmente se perde pelo caminho. > 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? Não. Concordamos que ECQ é muito suspeito. :-) Aliás, o papel do símbolo ⊥ em Dedução Natural é frequentemente artificial e "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 Hummm... Dualmente, qual seria a regra de eliminação do top? A regra de que "sob nenhuma circunstância podemos eliminar o top"? Parece-me um simples forçação de barra. Abraços, Joao Marcos -- http://sequiturquodlibet.googlepages.com/ -- 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/CAO6j_LhGn2S3XU_VQfQRijLO6W2hu-tQbN33eKRmqzMEV1KKog%40mail.gmail.com.
