Oi João Aqui vai uma opinião talvez muito simplista de um não-especialista. A propriedade meta-logica que me parece relevante para sua questão é a comutatividade com “é demonstrável que”.
Em um contexto construtivo usual, conjunção, disjunção e implicação comutam com “é demonstrável que”. Por exemplo, é demonstrável que A\vee B sse é demonstrável que A ou é demonstrável que B. Como se “é demonstrável que” fosse um morfismo da lógica na metalógica. Isso não vale para a negação, claro. De modo mais geral, entender a negação em termos de condições de demonstrabilidade, como é tentado em contextos construtivos mainstream, é sempre complicado porque as condições de demonstrabilidade de \neg A não são as condições de não demonstrabilidade de A. Abraço Rodrigo Enviado do meu iPhone Em 17 de mai de 2018, à(s) 21:48, Walter Carnielli <walter.carnie...@gmail.com> escreveu: > Oi João, respondendo só metade da sua pergunta, a metade mais fácil: > na verdade, a bi-implicação na lógica clássica (e em varias > outras) corresponde à soma no anel Booleano onde a conjunção é o > produto. Dessa forma, fica claro porque a bi-implicação, sendo soma, > é associativa, comutativa, tem elemento neutro (o top), etc. A > coisa se generaliza bem naturalmente para lógicas multivaloradas, > modais, etc. Tenho alguns artigos com diversos co-autores a esse > respeito, como vc talvez se lembre. > > Essa é uma vantagem de se preferir anéis de polinômios em > detrimento de álgebras de Boole (ao menos acredito eu). > > O resto da questão ainda não sei... e não sei se vou saber. > > Abraços, > Walter > > Em 17 de maio de 2018 20:30, Joao Marcos <botoc...@gmail.com> escreveu: >> 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ê recebeu essa mensagem porque está inscrito 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 nesse grupo, envie um e-mail para logica-l@dimap.ufrn.br. >> Acesse esse grupo em >> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. >> Para ver essa discussão na Web, acesse >> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LjFidFDHSaxFpJwYfhEf13gsoEG8g2YYi9iFtPVY2e9NQ%40mail.gmail.com. > > > > -- > ----------------------------------------------- > Walter Carnielli > Centre for Logic, Epistemology and the History of Science and > Department of Philosophy > State University of Campinas –UNICAMP > 13083-859 Campinas -SP, Brazil > > > http://www.cambridge.org/br/academic/subjects/philosophy/twentieth-century-philosophy/significance-new-logic?format=HB&isbn=9781107179028 > > > Institutional e-mail: walter.carnie...@cle.unicamp.br > Website: http://www.cle.unicamp.br/prof/carnielli > CV Lattes : http://lattes.cnpq.br/1055555496835379 > > -- > 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/CA%2Bob58NkeY%3DvtCu5jHEeJnTaVNS7Z%2BQfvBZ2K1Jnw1n%3DpSLVMg%40mail.gmail.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/8EE8898A-037F-4E48-9F77-3955CAB376BE%40gmail.com.