Olá, João Marcos! Joao Marcos <botoc...@gmail.com> escreveu:
> > [...] > > Na lógica intuicionista a negação ¬A de uma sentença A é > frequentemente introduzida *por definição* como a sentença A→⊥, onde → > é a "implicação intuicionista" e ⊥ 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 ¬ 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 → e ⊥ 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? Antes de mais nada, devo avisar que os meus preconceitos, ahã, perdão, *convicções* filosóficas se alinham com a "impressão de que tais conectivos assim introduzidos não existem de verdade". Isto é, creio que a negação, caso insistirmos seja mesmo um conectivo lógico, não está no mesmo patamar dos outros conectivos, mas se relaciona primariamente com restrições externas e/ou globais (trivialidade), mais do que com restrições internas e/ou locais (contradição). Contudo, não creio que seja pertinente expor meus sermões, ahã, quero dizer, minhas *argumentações* filosóficas nesse sentido, embora esteja tentado em fazê-lo. Duvido que possam ser consideradas "justificativas meta-lógicas razoáveis". Para aqueles que não compartilham das minhas opiniões esquisitas sobre a negação, eu diria que as evidências metalógicas apontam na direção oposta, isto é, *contra* a negação como abreviatura. Uma ilustração interessante surgiu nas discussões do nosso grupo em Tübingen algumas semanas atrás. Nós examinávamos dois teoremas de Grigori Mints sobre regras admissíveis em lógica intuicionista. Um dos teoremas afirma que regras admissíveis que não figuram → são deriváveis (o outro teorema afirma o correspondente sobre ∨). Aqui, regras admissíveis que figuram ¬ estão incluídas, pois a negação é considerada primitiva. Alguém que desenvolvesse investigação similar com base num sistema com a negação definida, seria naturalmente conduzido a um resultado mais fraco. As demonstrações de Mints são bem complicadas. Elas combinam argumentações semânticas com argumentações sintáticas envolvendo traduções entre lógica clássica e intuicionista. Em conversa com o Luca alguns dias depois, eu tentava esboçar uma demonstração mais nominalista do resultado considerando regras primitivas para a negação em dedução natural. Por alguma razão, a conversa ficou girando em torno da negação, e eu cheguei a mencionar a nossa discussão sobre ex contradictione quodlibet algum tempo atrás aqui na lista. Eu apresentei o que imagino ser a tua posição sobre o assunto. Fosse o que apresentei a tua real posição ou um mero espantalho teu, eu acabei me encontrando sozinho do outro lado do argumento... Bem, de qualquer maneira, o Luca mencionou algumas coisas interessantes (ele também estava interessado, por outros motivos, na questão da negação como abreviatura): na axiomatização pioneira de Heyting (1930) a negação era primitiva; Gentzen (1934) teria sido o primeiro a propor explicitamente um sistema com a negação definida em termos da implicação e do absurdo, embora a ideia já estivesse presente implicitamente em escritos anteriores de Brouwer e outros precursores intuicionistas. Eu penso que a proposta abreviativa Gentzeniana com respeito à negação não é gratuita. Uma concepção primitiva de negação apresenta dificuldades consideráveis com respeito à harmonia dedutiva e resultados relacionados (normalização e etc.)[1][2], apesar do cálculo de sequentes sugerir aqui uma saída sofisticada[3][4]. Contudo, embora de caráter técnico, essa limitação pode ser relegada à uma mera questão pragmática de métodos e resultados, e, para os que preferem, em todo caso, métodos semânticos, talvez mesmo uma questão inócua. Ademais, como indico acima, para os que não compartilham das minhas convicções religiosas, digo, filosóficas, pode ser mesmo que razões metalógicas conduzam à posição oposta. Por razões históricas, no entanto, as matérias técnicas que preocupavam Gentzen ainda carregam um peso considerável nas investigações em lógicas construtivas, de maneira que ainda é comum encontrar a negação abreviada na literatura. Referências: [1] Dag Prawitz. Natural Deduction: A Proof-Theoretic Study, 1965, Almqvist & Wiksell. Chapter II, § 1, Remark on pp. 34-35. [2] Michael Dummett. The Logical Basis of Metaphysics, 1991, Harvard University Press. Chapter 13, Negation, pp. 291-296. [3] Ian Rumfitt. "Yes" and "No". Mind, 109, 781-823. [4] Stepen Read. Harmony and Autonomy in Classical Logic. Journal of Philosophical Logic, 29 (2), 123-154. -- Hermógenes Oliveira »Wir sind leicht bereit, uns selbst zu tadeln, unter der Bedingung, dass niemand einstimmt.« -- Marie von Ebner-Eschenbach -- 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/87fu2p6sgl.fsf%40camelot.oliveira.
