Otima pergunta, Joao Marcos! uma que eu tb tenho carregado comigo ha algum tempo. Como voce disse, nao ha resposta certa, mas queria dar o meu palpite.
Eu acho, (e espero que isso seja junto com o Gentzen e o Prawitz ) que a gente quer pensar nos conectivos constructivos de forma que eles sejam tao independentes uns dos outros quanto possivel. a gente sabe que precisa ter conjuncao, disjuncao e implicacao independentes em logica intuitionista proposicional. e me parece que isso 'e bom. a independencia dos conectivos mostra que eles correspondem a intuicoes diferentes, que devem ser modulares. e a gente sabe que a negacao *pode* ser definida em termos de implicacao no falso. em termos de que teoremas sao provados, a gente precisa de pelo menos esses ingredientes. a gente tb sabe que pra logica classica, as bases sao menores, (e.g. negacao e disjuncao sao suficientes), bem como varias outras possibilidades. ate' o famoso Scheffer stroke que faz tudo sozinho mesmo e ninguem entende nada. mas a negacao que temos definida em termos de implicacao no falso, 'e muito ruim, na minha opiniao. ela nao nos da' muita informacao. ate mesmo na semantica categorica, ela colapsa todas as provas diferentes de uma mesma proposicao, jogando fora uma das razoes pra fazer semantica categorica. >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? acho que nao. acho que ao contrario, a negação introduzida por abreviatura 'e um problema, eu preferiria te-la como um conectivo independente. mas nao sei como introduzi-la por si mesma num sistema construtivo, mantendo as propriedades que quero. o que eu gostaria mesmo era de ter era uma versao de logica proposicional intuicionista onde a negacao das proposicoes basicas fosse atomica, e a gente comecasse sempre de uma versao onde as coisas fossem verdadeiras e falsas. eu gostaria muito de uma versao da logica do Nelson N4 onde eu soubesse que substituicao de variaveis proposicionais funciona e onde eu conseguisse provar as coisas basicas tipo cut-elimination, propriedade de sub-formula, interpolacao, etc. mas eu nao sei fazer isso. e sobre a bi-implicacao, eu nao me preocupo com ela. acho que a matematica de algebras de todos os tipos 'e legal, gosto de aneis, de espacos vetoriais, de corpos , de modulos, de espacos topologicos, de fiber bundles, de feixes, de homotopias, de variedades diferenciais, etc.. mas nao acho que bi-implicacao seja muito importante logicamente nao... abracos Valeria 2018-05-17 16:30 GMT-07:00 Joao Marcos <botoc...@gmail.com>: > 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_LjFidFDHSaxFpJwYfhEf13gsoEG8g2 > YYi9iFtPVY2e9NQ%40mail.gmail.com > <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LjFidFDHSaxFpJwYfhEf13gsoEG8g2YYi9iFtPVY2e9NQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- Valeria de Paiva http://vcvpaiva.github.io/ http://research.nuance.com/author/valeria-de-paiva/ http://www.cs.bham.ac.uk/~vdp/ -- 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/CAESt%3DXuhaxCkAph-HOETb2i9d0yP%2Bzb2dE9aODcjJnouq2gsWQ%40mail.gmail.com.
