Só uma pequena observação en passant, trivial, porém, se for esquecida, pode levar a confusões. As definições que costumam ser escritas por A -> *bot* nas lógicas clássicas e intuicionista são de fato duas distintas, uma vez que -> tem dois diferentes significados, ok? Claro, todo mundo sabe disso, foi só um lembrete. No mais, vou pensar quando der. Bjs, Andrea
Em 18 de maio de 2018 17:52, Abílio <abilio.rodrig...@gmail.com> escreveu: > 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. > -- 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/CACHAqB%3DJhcYo--C_PigH%3DYGBn2ZPScNeV-XvAeWTGnhqhNY3_A%40mail.gmail.com.
