Oi JM e Hermógenes, Um breve comentário sobre o top. Em uma mensagem anterior, JM escreveu:
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. Podemos eliminá-lo sim e inferir qualquer proposição A, desde que A seja verdadeira. Simbolicamente, podemos expressar sua regra de eliminação da seguinte maneira: ⊤ true A true -------------------- ⊤-elim A true No entanto, uma vez que já temos uma derivação de A, essa é claramente uma regra redundante. Este é o único sentido que conheço em que podemos dizer, dualmente, que "top não possui uma regra de eliminação". :) ---- Hermógenes escreveu: 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). Este questionamento é sem dúvidas legítimo e pode ser problemático em BHK dado a sua falta de rigorosidade. Contudo, só temo que seja muito injusto tirar daí que... [...] Confesso que, às vezes, me pergunto se o > intuicionismo tradicional, como exemplificado pela tradição BHK, seria > mesmo uma posição filosoficamente coerente. (Trecho de uma mensagem anterior do Hermógenes) ...a escola intuicionista ofereça uma posição filosoficamente insatisfatória, uma vez que BHK é uma tentativa relaxada de representar apenas uma pequena fatia desta corrente de pensamento. Pessoalmente, acredito que haja desenvolvimentos filosoficamente interessantes e rigorosos do intuicionismo desde a emergência da MLETT e das teorias de tipo computacionais mencionadas em minha mensagem anterior. O artigo 'Constructive mathematics and computer programming' (1982) do Martin-Löf, que você deve conhecer, é a referência canônica no assunto. Abraços lógicos, Bruno -- Bruno Bentzen https://sites.google.com/site/bbentzena/ On Friday, April 7, 2017 at 5:58:57 PM UTC+8, Joao Marcos wrote: > > 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 [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/f88f1fe1-6469-42ed-bf0e-5dba4a3f75b4%40dimap.ufrn.br.
