Salve, Hermógenes: Obrigado pela resposta.
>>> 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. :-) Assim que tivermos um critério de logicidade em mãos, portanto, poderemos discutir melhor. :-) Uma maneira de resumir o meu comentário seria: antes de dizer que algo não é "razoável", convém deixar claras as nossas expectativas e as regras do jogo. (Tenho a impressão de que falhar repetidamente nesta tarefa converte muito do que se faz em Teoria das Demonstrações em pregação com caráter puramente ideológico.) No caso da negação, o mínimo que eu esperaria, do ponto de vista abstrato, é que não valham a asserção segundo a qual "p é consequência de não-p" nem a asserção segundo a qual "não-p é consequência de p". Alternativamente, para lógicas tarskianas, isto consistiria em dizer que se há de aceitar a negação de certas sentenças rejeitadas, e rejeitar a negação de certas sentenças aceitas --- usando assim a negação para converter "certas sentenças verdadeiras" em sentenças falsas e vice-versa. Tal expectativa, de fato, é um caso particular das propriedades de uma negação "minimamente decente", que discuti na página 204 do seguinte artigo: http://www.sciencedirect.com/science/article/pii/S1570868304000576 >> 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. Se você preferir, podemos transformar o conectivo nulário em um conectivo unário # tal que #(p) é equivalente a ⊥. Ou um conectivo n-ário com o mesmo efeito. Neste(s) caso(s) você claramente concordaria que faz menos sentido falar em aplicar substituição sobre tal conectivo. A propósito, eu discuto um pouco a interpretação não-determinística conectivo ⊥ (que chamo "botop"), típica da lógica de Johánsson, na seção final deste artigo: https://link.springer.com/article/10.1007/s11225-009-9196-z A discussão diz respeito à figurinha que se encontra um pouco antes, na página 232, que herdei essencialmente de Curry 1963. Moral: um conectivo não é uma proposição atômica --- nem quando ambos se parecem. Note, a propósito, que tal conectivo não teria regras de introdução (para além das regras artificiais que o Martin-Löf aparentemente inventaria só para manter o slogan sobre introdução+eliminação). Joao Marcos -- 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_LhU1-PZ0a6nrSjj1FMG%3D7o%3DT0ETw8gJo-1Y_6%3Dvd-9sNg%40mail.gmail.com.
