> 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? > 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? Abraços, JM -- 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 [email protected]. Para postar neste grupo, envie um e-mail para [email protected]. 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_Lj4N-_Lhs4y%2BcmMaLhCoMdQ7LMQ0ie3%2B%2BGFLJuOH9mTpA%40mail.gmail.com.
