Só duas consideração provavelmente irrelevantes e que não interessam a ninguem. Na pratica matemática, se prova a negação de algo assumindo esse algo e chegando a uma contradição. Mas do ponto de vista do significado da proposição \neg A, ele é completamente determinado pela regra de introdução e, portanto, \neg A tem já algum significado independente de 0 e --> a priori (talvez seja isso que a Valéria tenha dito acima, não sei)
Como o Abilio mencionou acima, seria melhor (na verdade, seria a única maneira realmente construtiva) tomar um ponto de vista paraconsistente (igual originalmente o Brouwer e o Kolmogorov pensavam) quando se define a negação como A --> 0. Minha sugestao seria colocar termos em 0. Afinal, é assim que se pensa na matemática. Qualquer contradição deveria ser um termo canônico de 0. Abs., Fernando Em 19 de maio de 2018 21:26, Valeria de Paiva <valeria.depa...@gmail.com> escreveu: > obrigada, Abilio! > > 2018-05-19 14:03 GMT-07:00 Abílio <abilio.rodrig...@gmail.com>: > >> oi valeria >> aqui >> >> On the hypothetical judgement in the history of intuitionistic logic. >> In: glymour, c.; wang, w.; westerstahl, d. (eds.) Logic, methodology, >> and philosophy of science: proceedings of the thirteenth international >> congress. London: king's college publications, 2009. >> >> >> 2018-05-19 19:51 GMT+01:00 Valeria de Paiva <valeria.depa...@gmail.com>: >> > qual 'e a referencia, Abilio? >> >>(van Atten fala sobre). >> > >> > >> > 2018-05-18 13:52 GMT-07:00 Abílio <abilio.rodrig...@gmail.com>: >> >> >> >> Colegas, vou tentar uns 'pitacos filosoficos' aqui. >> >> >> >> 1. De fato, ~A nao tem sentido construtivo, ao passo q A -> \bot parece >> >> ter. >> >> >> >> 2. Me parece q construtivamente nem o ex falso nem A -> (B ->A) >> >> deveriam ser validos. Ha razoes para achar q uma 'logica de Brouwer' >> >> deveria ser paraconsistente e relevante. Mas nao pq isso parece ser a >> >> melhor interpretacao do q Brouwer diz, mas sim pq ~A -> (A -> B) e A >> >> -> (B ->A) nao parecem validos do pto de vista construtivo (van Atten >> >> fala sobre). >> >> >> >> 3. Sobre definir ~ com \bot. Dentre os conceitos de ~ e \bot, qual >> >> parece ser intuitivamente mais plausivel? Me parece q o \bot. A ~ traz >> >> todos aqueles velhos problemas filosoficos de nao ser etc. O \bot eh >> >> algo ruim, inconcebivel, catastrofico, inaceitavel (ok Daniel?) - o >> >> conceito, a ideia de algo ruim, inconcebivel, catastrofico, >> >> inaceitavel me parece ser bastante clara. >> >> >> >> Abracos >> >> >> >> Abilio >> >> >> >> >> >> 2018-05-18 20:59 GMT+01:00 Durante <dura...@ufrnet.br>: >> >> > Oi João e colegas, >> >> > >> >> > Concordo com o Rodrigo. Usando outras palavras eu diria: ~A não faz >> >> > sentido >> >> > construtivo. Como apresentar a construção do que não se constrói? Não >> >> > dá. A >> >> > alternativa é, então, mostrar as consequências de uma suposta >> >> > construção. Ao >> >> > assumirmos como construído o que não se constrói, devemos ter como >> >> > consequência algo ruim, catastrófico, negativo (trocadilho >> inevitável). >> >> > Daí >> >> > o A -> ⊥. >> >> > >> >> > Saudações, >> >> > Daniel. >> >> > >> >> > PS: só para registrar, como você sabe, o A -> ⊥ funciona também como >> >> > definição da negação clássica. E há vários motivos, mas que eu saiba >> >> > todos >> >> > ad hoc, para usa-la. >> >> > >> >> > >> >> > Em quinta-feira, 17 de maio de 2018 20:30:57 UTC-3, Joao Marcos >> >> > 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/ >> 6f8a7ae5-4185-438a-9a5f-ddeac5da0105%40dimap.ufrn.br. >> >> >> >> -- >> >> 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/ >> CALtFD22m%2BhZdK6GgUZ1Egfuvq3w9Jrzx%3DNRbBPGk%2B16e8z2NWQ% >> 40mail.gmail.com. >> > >> > >> > >> > >> > -- >> > Valeria de Paiva >> > http://vcvpaiva.github.io/ >> > http://research.nuance.com/author/valeria-de-paiva/ >> > http://www.cs.bham.ac.uk/~vdp/ >> > >> > -- >> > 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/ >> CAESt%3DXuTwxNo0vGqj%3DnzLaGhnTn%2By%2BQLhiOcAJtUgxVQ7UPuTQ% >> 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/di >> map.ufrn.br/group/logica-l/. >> Para ver esta discussão na web, acesse https://groups.google.com/a/di >> map.ufrn.br/d/msgid/logica-l/CALtFD23Rz94-C-ErVcUd2Ze2qM%2B >> qZxuPo1tcJ6ocVomM6Li%2Bqw%40mail.gmail.com. >> > > > > -- > Valeria de Paiva > http://vcvpaiva.github.io/ > http://research.nuance.com/author/valeria-de-paiva/ > http://www.cs.bham.ac.uk/~vdp/ > > -- > 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/CAESt%3DXtA1zye2PL4%2B6GhUeTQmbdaLH7_XP6_ > EPBK6RSfE6OW5A%40mail.gmail.com > <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXtA1zye2PL4%2B6GhUeTQmbdaLH7_XP6_EPBK6RSfE6OW5A%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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/CAJGvw-3ARZUuGVOnxh77WGwmJK%3DQM7V32TwdmQLKufub9-werQ%40mail.gmail.com.
