PessoALL: Em axiomatizações da lógica clássica, a *bi-implicação* frequentemente é introduzida como uma mera abreviatura a partir, digamos, de fórmulas contendo conjunções e implicações, ou contendo conjunções, disjunções e negações, apropriadamente combinadas. Tal situação nem sempre é ideal, mas não é inteiramente fora de propósito: se a bi-implicação é tomada como um conectivo primitivo, de fato, suas axiomatizações terão de dar conta de propriedades pouco intuitivas da bi-implicação clássica, tais como a associatividade deste conectivo (poder-se-ia argumentar neste caso que se trata de um mero "efeito colateral" do princípio da casa do pombo, tendo em vista a bivalência da lógica subjacente). Além disso, vale notar que tais definições alternativas não resistem ao enfraquecimento da lógica original, pois em fragmentos dedutivos da lógica clássica duas fórmulas classicamente equivalentes podem deixar de ser equivalentes, e passa assim a fazer diferença qual abreviatura é escolhida para introduzir o conectivo em questão.
Estendendo o exemplo propriamente para o domínio não-clássico, gostaria de colher reações dos especialistas aqui sobre o seguinte ponto. Na lógica intuicionista a negação $\neg A$ de uma sentença $A$ é frequentemente introduzida *por definição* como a sentença $A\to\bot$, onde $\to$ é a "implicação intuicionista" e $\bot$ o "absurdo intuicionista", tomados como conectivos primitivos. Como consequência, ao enfraquecermos a implicação ou o absurdo, pela consideração de um fragmento dedutivo da lógica intuicionista, pode ocorrer que a interpretação de $\neg$ como algo que mereça o título de "negação" seja prejudicada. Obviamente, para fragmentos da lógica intuicionista a abordagem supra-citada só faz sentido quando $\to$ e $\bot$ estão disponíveis. De todo modo, tendo em vista o fato de que os conectivos intuicionistas não são em geral interdefiníveis, não é inconcebível que a introdução de certos conectivos por meio de abreviaturas possa em certas situações ser conveniente, por alguma razão... embora isto possa também passar a impressão de que tais conectivos assim introduzidos "não existem de verdade". A pergunta que lanço aqui é: ao trabalhar com *lógicas construtivas* (que sejam fragmentos da lógica clássica ou, digamos, de alguma extensão modal da lógica clássica), haverá alguma justificativa meta-lógica _razoável_ (em oposição a justificativas meramente ad hoc, formuladas convenientemente para "explicar" a teoria a posteriori) para considerarmos a negação como sendo preferencialmente introduzida por abreviatura, sempre que isto é possível? Situações em que tal abordagem pareceria não ser atraente, por exemplo, seriam aquelas em que a implicação e o bottom são suficientemente fortes para que a definição seja útil, mas a negação que se pretende introduzir é na realidade tanto paracompleta quanto paraconsistente (exemplo: lógica N4 de Nelson). (A pergunta acima ---para a qual não há resposta certa ou errada--- é propositalmente vaga, de modo a tentar não tomar partido de nenhuma posição específica. Com alguma sorte, contudo, a pergunta estará suficientemente clara para que os colegas possam emitir suas *opiniões* a respeito do assunto!) 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 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_LjFidFDHSaxFpJwYfhEf13gsoEG8g2YYi9iFtPVY2e9NQ%40mail.gmail.com.
