Joao Marcos <botoc...@gmail.com> escreveu: >> 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
Uma maneira de resumir o meu comentário nesse contexto seria: Até que ponto seria razoável chamar isso de *operador lógico*? Isto é, eu hesitaria em chamar o conectivo que você descreve acima de operador lógico (assumindo que o entendi corretamente). No fim das contas, me parece, a questão é ideológica: uns vêem lógica em tudo, outros a procuram de dia com uma lâmpada na mão. :-) > 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. Bem, a regra de substituição uniforme não se aplica, de qualquer maneira, a conectivos (o quão marivolhoso seria se pudéssemos substituir conectivos à vontade, não é mesmo? :-D). Mas, considerando a *sentença* formada usando o conectivo nulário, não consigo ver porquê a regra de substituição seria problemática, assumindo, é claro, que esse conectivo não seja governado por ECQ ou qualquer outra regra de inferência, que era o caso que eu tinha em mente. Afinal, neste caso, o absurdo seria apenas uma sentença, embora pudéssemos conferí-la, extra-logicamente, um significado especial. > 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. De acordo. >> 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. Eu diria que não é apenas aparência... -- 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/87zifscpcm.fsf%40camelot.oliveira.
