Re: [Logica-l] Ontologia SUMO, ATP, ITP e Explicação de provas
Alexandre Rademaker <aradema...@gmail.com> escreve: > Prezados, Olá, Alexandre. > Estamos fazendo vários experimentos com a SUMO [1], sua tradução para > TPTP/FOL [2] e verificação automática em provadores como E, Vampire > etc. Estamos reportando várias inconsistencias [3] e dificuldades de > obter provas que deveriam ser simples como o exemplo de Banana Slug > [4]. > > Em especial, estou procurando agora boas ferramentas interativas que > aceitei como entrada TPTP, debugar provas longas de refutação não é > tarefa fácil... Dicas? Alguém conhece algo pronto?! Eu não conheço absolutamente nada sobre ontologia (informática), mas tenho alguma experiência com o formato TPTP/ILTP. Se entendi bem o que você precisa, tenho algumas informações que possam ser relevantes. Primeiro, baseado numa rápida passada de olhos, me parece que para resolver o Banana Slug não basta lógica de primeira ordem (TPTP-FOF), mas é necessário lógica de ordem superior (TPTP-THF)[1]. Quanto a assistentes interativos que trabalhem com o formato TPTP, sei que o Isabelle contém uma ferramenta tptp_isabelle e que o Matita também seria capaz de trabalhar com TPTP. Porém, embora já tenha usado tanto Isabelle quanto Matita, nunca trabalhei neles com problemas no formato TPTP. Portanto, não sei dizer se o suporte para TPTP está limitado a FOF ou inclui a extensão para ordem superior THF. Dê uma olhada no SystemonTPTP do Prof. Sutcliffe[2]. Talvez encontre ali no meio um ATP/ITP que satisfaça suas demandas. Saudações, Notas: [1] Imagino que funções indutivamente definidas são necessárias para a parte aritmética, não? [2] http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP -- Hermógenes Oliveira -- 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/87shwgnpuv.fsf%40camelot.oliveira.
Re: [Logica-l] votação eletrônica de classificação de periódicos da área de lógica
Prezados, O período de votação terminou. O resultado pode ser conferido em http://civs.cs.cornell.edu/cgi-bin/results.pl?id=E_b8a67f80d6df72ec Com apenas 19 votos contabilizados, o resultado dificilmente pode ser tomado como representativo da comunidade de lógica brasileira, mas talvez possa revelar algo de interessante. Saudações, -- Hermógenes Oliveira -- 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/87mvmjnkq9.fsf%40camelot.oliveira.
Re: [Logica-l] Re: Is there a model of ZFC inside which ZFC does not have a model?
Samuel Gomes escreveu: > Olás, Olá. > Hermógenes: [...] Novamente, obrigado pela resposta. > João Marcos: > > * > Mas no segundo sentido (assumindo que, para eliminar inteiramente a > semântica desta conversa, por "refutação de S" estamos nos referindo à > "demonstração de ~S") nem mesmo a própria teoria correspondente à > *lógica clássica de primeira ordem* seria completa, né? > * > > ... Imagino que aí tenha gente que consiga explicar melhor do que eu, > mas essencialmente os teoremas de incompletude necessitam de um pouco > de Aritmética, não ? Então, só pegando a Lógica de primeira ordem, não > vejo (pelo menos não agora de imediato) como justificar uma > incompletude sintática. Ué. Eu pensei a coisa muito mais simples do que isso: A lógica de primeira ordem pura, na sua formulação padrão, é obviamente incompleta (sintaticamente), pois, dada uma variável proposicional p, não é possível obter uma demonstração ou refutação de p. A questão da completude sintática só faz mesmo sentido quando temos uma teoria formal na qual a lógica de primeira ordem é calibrada para própositos aritméticos (matemáticos). Por exemplo, na aritmética de Peano, onde não há variáveis proposicionais e todas as sentenças atômicas são compostas usando a constante 0, a função sucessor S e demais funções artiméticas. Ou em ZF, onde as sentenças atômicas tratam de conjuntos e suas relações de pertinência. Em outras palavras, na AP todos os termos e variáveis estão para números, a igualdade e os predicados se aplicam a números. Analogamente para ZF, mas com conjuntos. Para teorias aritméticas (matemáticas), faz sentido esperar que, dada uma sentença qualquer A, A ou ¬A seja demonstrável, pois não há nenhuma sentença contingente. Estou sendo ingênuo? Ou não entendi direito a pergunta do João Marcos? -- Hermógenes Oliveira -- 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/877fdplz57.fsf%40camelot.oliveira.
Re: [Logica-l] Re: Is there a model of ZFC inside which ZFC does not have a model?
Dankness asked > Is there a model of ZFC inside which ZFC does not have a model? Noah Schweber answered: > Yes. > Recall that by the Completeness Theorem, having a model and being > consistent are the same thing. Also, by Incompleteness, ZFC doesn't > prove its own consistency. Finally, ZFC can prove the Soundness > Theorem - that an inconsistent theory has no models! > So - assuming ZFC has a model - ZFC is consistent. If ZFC is > consistent, then ZFC can't prove "ZFC is consistent." By completeness, > this means there's a model of ZFC satisfying "ZFC is inconsistent." > Since ZFC proves the Soundness Theorem, this model must think that ZFC > has no model! Algém teria a bondade de esclarecer o que significam "modelos pensantes" e por quê o teorema de *completude* está sendo invocado para *ZFC*? -- Hermógenes Oliveira -- 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/877fdp62nn.fsf%40camelot.oliveira.
Re: [Logica-l] [META] Proposta de princípios e regras de convívio para a LOGICA-L, parte 1/3
Joao Marcos <botoc...@gmail.com> escreveu: > 2016-07-12 11:24 GMT-03:00 LOGICA-L <logica-l@dimap.ufrn.br>: >> Na mensagem de hoje proponho discutir especificamente as quatro >> primeiras regras de convívio do nosso documento. Prazo para >> manifestações: uma semana. >> >> REGRA 1. desaprovação da anonimidade: a lista é de livre inscrição, >> mas postagens feitas a partir de perfis que aparentem ser fake podem >> vir a ser moderadas pela administração > > O colega Carlos Gonzalez sugeriu uma redação bastante mais precisa > para a REGRA 1, que foi registrada no nosso documento [...] Se é que ainda há tempo, gostaria de expressar minhas desconfianças com relação à *utilidade* da REGRA 1 no estado atual. Primeiro, suponho que a justificativa para a regra da identificação (REGRA 1) seja, conforme João Marcos apontou, que os participantes assumam publicamente responsabilidade pelas mensagens que veiculam na lista (incluindo, mas não limitado, aos efeito sofridos em termos de reputação, prestígio e demais mecanismos sociais supostamente úteis). Para isso, concordo, deve ser possível determinar a autoria das mensagens. Para tanto, porém, a autoria deve ser conhecida pela *comunidade* e não somente pela administração. Um perfil identificável somente pela administração é, para todos efeitos e propósitos sociais e comunitários, anônimo. Segundo, se a regra da identificação é somente para propósitos de responsabilização civil e criminal, devo lembrar que administrador de lista não é capaz (tecnicamente falando) nem competente (legalmente falando) de determinar a autoria de mensagens para esse propósito. Isso é papel da polícia e dos tribunais. Neste contexto, sequer a sugestão de que o administrador seria responsável pelo conteúdo ou identificação da autoria de mensagens veiculadas na lista me soa demasiadamente paternalista. Assim, a REGRA 1, no seu estado atual, me parece despropositada e inócua. Me parece que devemos escolher: obrigatoriedade da ficha do JYB ou permissão da anonimidade. Para mim, tanto faz. -- Hermógenes Oliveira «Plus d'un, comme moi sans doute, écrivent pour n'avoir plus de visage. Ne me demandez pas qui je suis et ne me dites pas de rester le même : c'est une morale d'état civil; elle régit nos papiers. Qu'elle nous laisse libre quand il s'agit d'écrire.» Michel Foucault -- 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/87vazxachx.fsf%40camelot.oliveira.
Re: [Logica-l] [OFF] "It is time to delete your Academia.edu account"
cê pode seguir outros pesquisadores e receber notificações quando elas publicam algum artigo bem como receber notificações de artigos em suas áreas de interesse (ou periódicos de interesse). Não sei como ele se compara com o Academia.edu (pois nunca usei este último), mas estou bastante satisfeito (e o portal tem melhorado a cada ano que passa). > Eu continuo na rede. De fato, a decisão é sua, meu amigo. -- Hermógenes Oliveira »Der Grundsatz, nach dem ich entscheide, ist: Die Schuld ist immer zweifellos.« Der Offizier, Franz Kafkas »In der Strafkolonie« -- 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/87tw8h3ala.fsf%40camelot.oliveira.
Re: [Logica-l] da matemática alemã
Joao Marcos <botoc...@gmail.com> escreveu: > [...] > > Recebi da Cláudia Nalon, entretanto, um link para um artigo > relacionado e bem mais interessante: uma entrevista com Abraham > Fraenkel, que apareceu no seu livro de memórias publicado recentemente > em inglês (com um pouco mais de 50 anos de atraso). > > Hitler’s Math > http://www.tabletmag.com/jewish-arts-and-culture/224161/hitlers-math > > Vale a pena observar o depoimento elogioso de Fraenkel a respeito de > Hilbert e Landau, que possivelmente lhe fizeram nutrir simpatia pelo > formalismo, e sua crítica política a Brouwer e idiotas como Ludwig > Bieberbach (fundador da "Deutsche Mathematik" > https://de.wikipedia.org/wiki/Deutsche_Mathematik), que eventualmente > levaram Fraenkel a abominar o intuicionismo. Por que você acha que questões pessoais, éticas e/ou políticas teriam influenciado a atitude de Fraenkel com relação ao formalismo ou ao intuicionismo? Você leu isso em algum lugar, ou é apenas uma impressão sua? Dei uma olhada na edição alemã das memórias do Fraenkel aqui na biblioteca e não consegui achar nada que indicasse isso... Pelo contrário, pelo menos na passagem reproduzida no artigo que você indicou, Fraenkel diz que o intuicionismo é "importante", "original" e "interessante". Contudo, ele censura implicitamente *o comportamento de Brouwer* e critica sua abordagem dogmática e mística do intuicionismo (enquanto elogia implicitamente o comportamento de outros construtivistas como Weyl). Esse negócio de julgar ideias com base em quem as professa é muito curioso. Algo que, inclusive, estava no centro dos movimentos pela "Deutsche Mathematik" e "Deutsche Physik". Assim, é possível que as motivações por trás das críticas do "Círculo de Munique" fossem de caráter ideológico nazista (esse círculo girava em torno de Hugo Dingler[1] que na sua empolgação com o socionacionalismo alemão chegou a ser denunciado por usar emblema da NSDAP antes de ser formalmente aceito no partido): atacavam a teria da relatividade (Einstein era judeu), a escola de Hilbert (Hilbert era "protetor" de judeus) e etc, embora essas motivações geralmente não estivessem explícitas e as críticas fossem feitas no âmbito teórico. O interessante é que Heinrich Scholz, elogiado por Fraenkel nas referidas memórias e amigo próximo de Fraenkel até a sua morte, *publicou artigo na Deutsche Mathematik*. Esse foi um artigo em defesa da escola hilbertiana contra os ataques do Círculo de Munique (especialmente Max Steck), um artigo escrito à convite do "idiota" Bierberbach, que, neste caso, pode ter contribuído para que o centro de pesquisas liderado por Scholz em Münster (um dos poucos em território alemão após a decadência de Göttingen) não sofresse consequências de motivação ideológica. Esse artigo do Scholz foi inclusive resenhado por Bernays no "Journal of Symbolic Logic". O ambiente na matemática e, particularmente, na lógica durante o período nazista é discutido em detalhes no livrinho de Eckart Menzler-Trott, "Gentzens Problem", particularmente no capítulo 4, "A briga por uma lógica alemã". Contudo, alguém comentou comigo que a edição em língua inglesa (à qual não tenho acesso) foi editada num formato mais puramente biográfico, com discussões sobre o socionacionalismo removidas completa ou parcialmente. Vale lembrar que algumas coisas ali são mesmo controversas. Quando se trata desse tipo de assunto, as coisas nunca são tão preto no branco. Em geral, intelectuais e acadêmicos são comumente desligados de questões políticas e são facilmente manipuláveis ideologicamente, isso quando não são ativamente oportunistas. Os poucos que arriscam arregaçar as mangas nesse quesito, pagam muitas vezes um preço caro em termos de suas carreiras, e podem mesmo acabar na cadeia (como aconteceu com Bertrand Russel e Michael Dummett). Interessante ainda é que a questão que provocou essa discussão, a da "decadência da matemática alemã" após a segunda guerra, apresenta como pressuposto implícito uma ligação entre nação e ciência, à exemplo da ideologia nazista. Muita gente acha que o problema principal com o socionacionalismo alemão eram coisas como o Rassengünther[2] e campos de concentração. Esquecemos que o nacionalismo em si mesmo é problemático, embora seja normalmente tolerado ou mesmo visto com bons olhos. Notas: [1] https://de.wikipedia.org/wiki/Hugo_Dingler [2] https://de.wikipedia.org/wiki/Hans_F._K._G%C3%BCnther -- Hermógenes Oliveira "Just publish it. If you're afraid that the population will be seduced by it, you have bigger problems than the book." Someone on the availability of Hitler's "Mein Kampf" on German book stores after the expiration of the copyright in 2016. -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGIC
Re: [Logica-l] da matemática alemã
Joao Marcos <botoc...@gmail.com> escreveu: > [...] > >> O interessante é que Heinrich Scholz, elogiado por Fraenkel nas >> referidas memórias e amigo próximo de Fraenkel até a sua morte, > > Estranho, sem dúvida, que eles fossem tão amigos. Eu não sabia. Como > disse anteriormente, não li muita coisa de pessoal do Fraenkel, ou > sobre o Fraenkel, além deste texto. Pois é. No trecho das memórias que você indicou, Fraenkel anuncia que vai falar sob Otto e Scholz, mas essa parte foi cortada e não aparece no trecho. Ambos os teólogos são lembrados de forma elogiosa no seu livro de memórias. Scholz é um caso peculiar, pois há relatos aparentemente contraditórios a respeito da relação dele com os nazistas: alguns relatam simpatia, ou, pelo menos, tolerância, com relação a NSDAP, principalmente antes da ascensão do partido ao poder; outros relatam que Scholz era um dos poucos com os quais se pudesse conversar francamente e criticamente sobre a NSDAP durante o auge do nazismo. Conta-se também que a intervenção de Scholz teria sido decisiva no resgate de um certo discípulo de Łukasiewicz (Salamucha) dos campos de concentração, tendo ele inclusive corrido riscos pessoais por fazê-lo. Eckart Menzler-Trott escreve que "Scholz war anfänglich ein starker Sympathisant des Nationalsozialismus [...]" mas que, contudo, "[...] aus seiner protestantischen Theologie schöpfte er ---im Gegensatz zu seinen Kollegen Emmanuel Hirsch und vielen anderen--- die Kraft gegen den Nationalsozialismus." > Aparentemente o idiota do Bieberbach não era tão dogmático com relação > ao que aceitava publicar na sua revista? Ou o alinhamento ideológico > lhe era mais caro do que o alinhamento matemático? Vai saber. Pelo pouco que sei a respeito, tendo a concordar com o diagnóstico do Courant: o sujeito parecia ser meio desmiolado. >> Vale lembrar que algumas coisas ali são mesmo controversas. Quando >> se trata desse tipo de assunto, as coisas nunca são tão preto no >> branco. Em geral, intelectuais e acadêmicos são comumente desligados >> de questões políticas e são facilmente manipuláveis ideologicamente, >> isso quando não são ativamente oportunistas. Os poucos que arriscam >> arregaçar as mangas nesse quesito, pagam muitas vezes um preço caro >> em termos de suas carreiras, e podem mesmo acabar na cadeia (como >> aconteceu com Bertrand Russell e Michael Dummett). > > Hilbert não parece ter sido uma figura muito desligada das questões > políticas... Não conheço muito da biografia de Hilbert, mas a impressão que tenho é que ele era bem engajado quando se tratava de questões políticas que afetavam o meio acadêmico. Não obstante, intelectuais que se engajam ativamente em questões políticas de interesse geral como anti-militarismo (Bertrand Russell) ou racismo (Michael Dummett) são bem mais raros. > Por acaso, o que vinha à minha mente enquanto eu lia sobre isto era a > história dos EUA, país que faturou cerca de 40% de todos os prêmios > Nobel da história. Destes, 31% foram dados a cientistas que não > nasceram lá. O recrudescimento do nacionalismo e da xenofobia, nos > EUA e fora de lá, pode vir a causar danos nesta fronte, e em várias > outras. Eu pensei algo similar... -- Hermógenes Oliveira -- 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/87zihowmta.fsf%40camelot.oliveira.
Re: [Logica-l] (In)decidibilidade e (In)completude
nônica > A_mn que descreve a operação de m com entrada n na interpretação > padrão. A sentença A_mn tem modelo finito se e somente se m para com a > entrada n. De fato, por um lado, A_mn é satisfeita na subestrutura da > interpretação padrão cujo domínio é o intervalo de operação de m com a > entrada n. Por outro lado, é fácil ver que se m não para com a entrada > n então A_mn só tem modelos infinitos. Segue-se do problema da parada > que a satisfatibilidade em estruturas finitas não é recursiva. Como a > satisfatibilidade em estruturas finitas é recursivamente enumerável (a > satisfatibilidade em cada estrutura finita é recursiva), temos que a > validade em estruturas finitas não é recursivamente enumerável. > Portando, não há sistema dedutivo (recursivamente enumerável) que > tenha como teoremas exatamente as sentenças válidas em todas as > estruturas finitas. Fim. Isso demonstra a *indecidibilidade* do conjunto das sentenças válidas em todas as estruturas finitas. > Referências: Alguns livros de lógica "undergraduate" contém os > detalhes. Ebbinghaus, Flum e Thomas é um deles. Pessoalmente, gosto > (mais) do Boolos, Burgess e Jeffrey, mas neste o teorema de > Trakhtenbrot é enunciado em um exercício apenas. Eu consultei o livro de Ebbinghaus, Flum e Thomas. Ali, o teorema é demonstrado como um teorema de indecidibilidade: "5.4 Trahtenbrot's Theorem. The set of first-order sentences valid in all finite structures is not R-enumerable." p. 171 onde "W is said to be register-enumerable (abbreviated: R-enumerable) , if there is a program which decides W" p. 160 (Definition 2.6) O manuscrito de Stephen Simpson que consta nas referências da entrada na Wikipédia apresenta o teorema de Trakhtenbrot como um reforço do resultado de Church (não mencionei isso na mensagem anterior pois somente agora me dei conta do manuscrito): http://logic.amu.edu.pl/images/2/21/Churchtrakhtenbrot.pdf Saudações, -- Hermógenes Oliveira -- 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/87eg497g1v.fsf_-_%40camelot.oliveira.
Re: [Logica-l] like dirt under the carpet, the incompleteness just won’t go away
ATENÇÃO: O que se segue está escrito num tom incisivo e moralista, além de refletir uma agenda específica do autor com a qual muitos já devem estar aborrecidos. Joao Marcos <botoc...@gmail.com> escreveu: >>> (brevíssimo artigo de divulgação, por Peter Lynch) >>> http://www.irishtimes.com/news/science/the-shaky-foundations-of-mathematics-1.2877075 > > [...] > > Precisamos certamente de mais artigos breves e inúteis como este. > Divulgação científica é importante, [...] Discordo plenamente. O artigo é um desastre. Repleto dos disparates, hipérboles e sensasionalismos comuns em artigos de divulgação dos teoremas de Gödel. É altamente duvidoso que artigos desse tipo contribuam para a divulgação de qualquer conteúdo que se possa chamar adequadamente de "científico". Mas creio que contribua consideravelmente para o tipo de misticismo barato e abuso dos teoremas de Gödel relatados nas obras de Torkel Franzén e Sokal & Bricmont, dentre outros. Porém, *mais importante ainda*, rejeito a premissa que ciência deva ser divulgada (no sentido que o artigo de Peter Lynch pode ser chamado de "divulgação científica"). *** começo da pregação *** Em primeiro lugar, artigos de divulgação que circulam na imprensa comum estão mais preocupados com frases de efeito e deslumbramento pseudocientífico do que com precisão e correção, o que, do ponto de vista científico, causa mais prejuízo do que benefício. As razões para isso são variadas, mas certamente incluem o fato de que é impossível transmitir para o não especialista qualquer conteúdo científico considerável em dez parágrafos de texto. Excessão concedida à colunas de recreação matemática, mas talvez estas não sejam, propriamente falando, artigos de divulgação científica. Em segundo lugar, a *veneração pela ciência* na maior parte das sociedades ocidentais já está acima da linha do ridículo. E isso é prejudicial para a ciência. Portanto, "divilgar ciência" como meio de alavancar o seu status no meio da sociedade, ou aprimorar a sua imagem perante a população em geral, me parece contraproducente. *Ensinar* ciência, contudo, me parede mais proveitoso. Me admira a prepotência da comunidade científica de manter (por conivência ou esmorecimento) uma situação na qual a Mariazinha da Esquina tenha que dispensar considerável esforço e dinheiro para obter conteúdo verdadeiramente científico (na forma de artigos e livros didáticos) enquanto a alimenta com curiosidades pseudointelectuais na roupagem de "divulgação científica": afinal a verdadeira ciência pertence aos cientistas, é produzida por cientistas e só consegue ser compreendida por cientistas; não há demanda por ciência em meio a população em geral, somente demanda por aplicação, ou, melhor ainda, por produtos de consumo; ciência e tecnologia é coisa de gente grande, deixe por conta dos especialistas. Ninguém é obrigado a se interessar por ciência e certamente *não* há nenhum valor em estimular esse interesse artificialmente, mas as pessoas que eu conheci que se interessam sinceramente por algum tema científico mostravam-se frustadas pela ausência de informações relevantes em peças de divulgação científica. Só ficam satisfeitos aqueles que estão menos interessados em ciência do que em parecer espertos. Divulgação científica *não* é importante. Ensino e livre acesso à material didático e produção científica é essencial. *** fim da pregação *** Saudações, -- Hermógenes Oliveira "If you make people think they're thinking, they'll love you; but if you really make them think, they'll hate you." Donald Robert Perry Marquis -- 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/87ziknsyiw.fsf%40camelot.oliveira.
Re: [Logica-l] like dirt under the carpet, the incompleteness just won’t go away
az de desdenhar artigos de divulgação científica completamente bem intencionados, os quais eu mesmo não conseguiria melhorar sequer uma linha sem explodi-lo para as dimensões dos monólogos que escrevo para a lista de lógica. -- Hermógenes Oliveira Este espaço deveria ser preenchido por uma frase inteligente e espirituosa. -- 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/87vavbss2p.fsf%40camelot.oliveira.
Re: [Logica-l] Five stages of accepting constructive mathematics (Andrej Bauer)
Marcelo Finger <marcelo.fin...@gmail.com> escreveu: > Como seria uma prova construtiva do resultado de Turing sobre a > existência de números (reais) não computáveis? > > A prova clássica é fortemente não construtiva e não apresenta um tal > número. E nem poderia apresentar pois se houvesse um algoritmo que o > gerasse, o número seria construtivo. > > Mas uma prova construtiva deveria apresentar um tal número. Mas como? > Fico com a impressão de que este resultado não é provável na lógica > intuicionista. Superficialmente, isto é, no âmbito puramente lógico, a demonstração intuicionista mostraria que nem todos os números reais são computáveis (¬∀x C(x), x ∈ ℝ) o que, intuicionisticamente, *não* é equivalente a mostrar que existem números reais não computáveis (∃x ¬C(x), x ∈ ℝ). No âmbito matemático mais fino, contudo, deve-se atentar ainda para a presença de noções baseadas em definições intuicionisticamente inadimissíveis. Assim, a noção de número real intuicionista não coincide com a noção de número real clássica, na medida em que podem haver definições e especificações clássicas de números reais que não são admissíveis para um intuicionista. De fato, é na análise real que as peculiaridades da matemática intuicionista se revelam com maior vigor. Porém, eu suspeito que a noção *clássica* de número real não seja essencial ao argumento de Turing. Não sei exatamente a qual trabalho de Turing você se refere, mas presumo que esteja se referindo ao artigo clássico de 1936. Ali, se não me falha a memória, Turing mostra que as sequências e números computáveis são enumeráveis. Bem, como os números reais não são enumeráveis, segue que nem todos os números reais são computáveis, isto é, classicamente, existem números reais não computáveis. Do ponto de vista intuicionista, a última parte, incluindo o apelo ao resultado de Cantor sobre a não enumerabilidade dos números reais, *pode* ser problemática. Mas o argumento de Turing que mostra a enumerabilidade dos números computáveis me parece em ordem. Ademais, intuicionistas normalmente não possuem reservas quanto à argumentos diagonais. Porém, como lembrou o João Marcos, sentimentos podem variar dentro da grande família construtivista: finitistas, predicativistas e etc. podem ter lá suas desconfianças. -- Hermógenes Oliveira -- 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/878tttn6oy.fsf%40camelot.oliveira.
Re: [Logica-l] Proof-theoretic proof of NP=PSPACE?
Olá, pessoal. O trabalho de Hermann e Gordeev estava na programação da conferência "General Proof Theory"[1] que aconteceu em Tübingen no ano passado. Contudo, não foi possível aos autores participar da conferência. Gordeev apresentou o trabalho no seminário do nosso grupo algumas semanas depois. Hudelmaier estava presente. As lâminas[2] da apresentação do Gordeev oferecem um bom panorama geral da demonstração, com foco nos pontos principais. Elas foram publicadas nos anais da conferência[3]. Na ocasião, o manuscrito foi disponibilizado com antecedência, o que nos permitiu acompanhar a apresentação sem muita perplexidade. Na minha opinião, os pontos mais críticos da demonstração, isto é, aqueles que mereceriam uma atenção mais detalhada em busca por erros: a) a afirmação dos autores de que o embutimento do fragmento implicativo do cálculo de sequentes de Hudelmaier no fragmento implicativo de dedução natural preserva as estimativas polinomiais de comprimento e fundamento (nº de fórmulas distintas). Gordeev apresentou o embutimento em detalhes e, para mim, ficou claro que esta parte está correta. Mas aqui é necessário atenção aos detalhes. Quem sabe alguém encontra um escorregão... Curiosamente, a reação inicial de Hudelmaier fora que uso do seu cálculo de sequentes seria inessencial, o que me impressionou um pouco, pois as estimativas polinomiais aqui estão apoiadas no fato de que o comprimento da derivação está restrito a O(n log n). b) após o embutimento das demonstrações CSH (cálculo de sequentes Hudelmaier) para DN (dedução natural), as árvores de DN são horizontalmente compactadas para DAGs (directed acyclic graphs) de maneira que colapsa múltiplas ocorrências de uma mesma fórmula. Esse processo, contudo, resulta em complicações com o descarte de hipóteses. A solução dos autores para este problema está baseada no que eles chamam de "correção local". Esta parte merece atenção. A noção intuitiva de descartes para DAGs é o que os autores chamam de "correção global". Esta noção de descarte, contudo, não pode, em geral, ser verificada em tempo polinomial. Daí, a noção de "correção local" é introduzida como substituta suficiente com verificação polinomial. Confesso que não acompanhei esta parte detalhadamente, embora tenha capturado o funcionamento geral. Este pedaço do argumento, eu diria, é o mais engenhoso do trabalho e merece atenção especial. Eu me prometi passar pelas minúcias depois da apresentação do Gordeev, mas nunca cheguei a fazê-lo. +++ Eu li somente o manuscrito distribuido na conferência em Tübingen, mas dei uma passada de olhos pelo artigo depositado no arXiv. Em comparação com o manuscrito, o artigo parece conter mais material, especialmente exemplos e diagramas ilustrando a compactação (descompactação) para (a partir de) DAGs, bem como uma discussão mais detalhada da questão dos descartes, correção global/local[4]. O Hermann vem trabalhando na intersecção entre complexidade computacional e derivabilidade em CS e DN há um bom tempo. Mas creio que não haja muitas pessoas amplamente familiriazidas com a literatura de ambos os campos. Eu recomendo as referencias nº 7, 1 e 2 do artigo, bem como outros trabalhos do Hermann[5], para quem quiser entender mais sobre o método de compactação para DAGs e a relação entre complexidade, CS e ND. As atualizações recentes na página de divulgação indicam como transferir os resultados obtidos para o âmbito mais conhecido do fragmento existencial de QBF, respondendo aos comentários do Marcelo. Acho ótimo que os colegas estejam interessados na demonstração. É um resultado importante e, quanto mais olhos, melhor. Notas: [1] http://ls.informatik.uni-tuebingen.de/GPT/ [2] Me parece que permaneceu uma pequena falha na última lâmina. Onde se lê "[...] proof of α is verifiable in polynomial time by a non-deterministic algorithm [...]" deveria-se ler ""[...] proof of α is *verifiable* in polynomial time by a *deterministic* algorithm [...]". [3] http://dx.doi.org/10.15496/publikation-10394 [4] A definição 5 (correção global) mencionada na § 3.6.1 parece ter sumido do artigo (embora haja uma discussão no corpo do texto em § 3.4). [5] http://www.tecmf.inf.puc-rio.br/EdwardHermann/Public -- Hermógenes Oliveira -- 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/87d1j5nb3o.fsf_-_%40camelot.oliveira.
[Logica-l] Re: [fora do tópico] Algorithmic Bias
Flávio Luis de Mello <flavioluis.me...@gmail.com> escreveu: > Saiu um statement da ACM > (http://www.acm.org/media-center/2017/january/usacm-statement-on-algorithmic-accountability) > tratando da preocupação deles com eventuais resultados tendenciosos de > algoritmos voltados para a tomada de decisão. > > Penso que a IA é uma das áreas contempladas por essa preocupação. Além > disso, ainda que a preocupação seja válida, me pergunto se realmente é > viável auditar o processo neste contexto. Gerar dados ou informações > tendenciosas é uma característica do algoritmo ou o reflexo daqueles > que produzem o algoritmo? Entendo que é o segundo. Eu entendo que é o primeiro. Note que as tendências e preconceitos dos programadores, ou da organização que desenvolve o algorítimo, não se refletem necessariamente no algorítimo (se este fosse o caso, obter um algorítimo não tendencioso seria praticamente um milagre). Como o problema está nos resultados tendenciosos dos *algorítimos*, então são estes que devem passar pelo crivo. Ademais, com o emprego crescente de métodos algorítmicos mais opacos, como redes neurais artificiais em combinação com aprendizado de máquina, resultados tendenciosos podem surgir a despeito das intenções (conscientes ou não) dos desenvolvedores, pois, como observa bem o documento publicado pela ACM, eles podem ser causados pelo dados que alimentam o algorítimo. Por exemplo, se um algorítimo, usado para alguma tomada de decisão, digamos, a ordenação dos resultados de alguma busca, é alimentado com dados coletados dos próprios usuários, pode-se esperar que tendências e preconceitos dos usuários se reflitam nos resultados do algorítimo. Dependendo do contexto, algo assim pode ser bastante problemático. -- Hermógenes Oliveira "There are two ways of constructing a software design: One way is to make it so simple that there are obviously no deficiencies and the other way is to make it so complicated that there are no obvious deficiencies." C. A. R. Hoare -- 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/877f5xb9re.fsf%40camelot.oliveira.
Re: [Logica-l] Women in Logic -- workshop associated to LiCS
Joao Marcos <botoc...@gmail.com> escreveu: >>> Esta é mais uma iniciativa válida, Valeria, com um comitê organizador >>> de primeira (e de Primeiro Mundo anglófono). >> >> Bem, se a razão de ser desse comentário diz respeito ao país de origem e >> à língua materna, posso acrescentar que reconheço apenas três nomes no >> comitê, nenhum deles de "Primeiro Mundo anglófono": Valéria de Paiva >> (brasileira), Alexandra Silva (portuguesa) e Adriana Compagnoni >> (argentina). > > Não entendi bem o aparte... Todas trabalham no Primeiro Mundo > anglófono, como está claro. Coincidência? Ou um ponto a mais a cujo > respeito valeria a pena refletir? E eu continuo sem entender o propósito da observação sobre "Primeiro Mundo anglófono". De primeiro, cogitei que o ponto dizia respeito à questão de diversidade cultural, étnica ou nacional. Agora, o ponto parece dizer respeito ao endereço e/ou vínculo empregatício? >> acrescento o seguinte: >> >> Talvez o estresse mencionado na mensagem de divulgação seja melhor >> compreendido, e talvez mesmo percebido como óbvio, por mulheres que >> atuam na área de lógica (para as quais, enfim, o evento é direcionado). >> Mas, fazendo um exercício de empatia, digo que, se eu entrasse numa sala >> de conferência que estivesse repleto exclusivamente de mulheres, >> certamente me sentiria inicialmente meio fora de lugar e talvez mesmo >> buscasse verificar se não teria entrado numa espécie de lavatório feminino >> por engano. Porém, mulheres que atuam na área de lógica passam por >> situação similar rotineiramente. > > De minha parte, eu certamente não penso que entrei em um lavatório nas > ocasiões em que entro em salas nas quais as mulheres são maioria. Nunca aconteceu comigo de eu entrar numa *sala de conferência*, num evento acadêmico, onde houvessem mais de vinte pessoas e *todas* fossem do sexo feminino. Se pretende dizer que isso já aconteceu contigo, fico sinceramente surpresso. A observação sobre o lavatório foi uma tentativa, aparentemente fracassada, de tratar o assunto com um pouco de bom humor[1] (com uma referência indireta à citação de Hilbert). Para esclarecer, isso nunca aconteceu comigo, mas se eu entrasse numa sala de conferência com, digamos, 200 mulheres e nenhum homem, eu obviamente não pensaria que tivesse realmente entrado num lavatório feminino. Ainda assim, provavelmente me questionaria se alguma variável envolvendo gênero me escapara: talvez o evento é somente para mulheres, etc. O ponto é que a maioria das mulheres que atuam na área de lógica, contudo, certamente já tiveram a experiência de entrar em salas de conferência cheias *sem nenhuma outra mulher presente*. Porém, muitos crêem que, neste caso, está tudo normal e não há nenhuma variável de gênero envolvida, pois não há ninguém *proibindo* as mulheres de participar. >> Se o ambiente não fosse tão dominado por homens e não houvesse tanto >> assédio, creio que tanto homens quanto mulheres se sentiriam mais à >> vontade para discutir ciência. > > Como são estas coisas nas áreas em que as mulheres são maioria? Não faço idéia. Mas não me preocupa tanto o fato de termos um sexo *em maioria*. Já participei de seminário (em filosofia, mas não em lógica) onde as mulheres fossem maioria (algo como 6 mulheres e 4 homens). O problema é quando, com frequência, um sexo está absolutamente ausente ou em *maioria esmagadora*. Em inúmeros ajuntamentos menores (seminários e etc.) da área de lógica que participei, ou bem não havia mulheres (caso mais comum) ou havia apenas uma (raro) ou, no máximo, duas (raríssimo) mulheres presentes. Notas: [1] https://broodsphilosophy.wordpress.com/2007/12/16/how-to-tell-if-you-suck-at-telling-philosophical-jokes/ -- Hermógenes Oliveira -- 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/87zikagrj8.fsf%40camelot.oliveira.
Re: [Logica-l] Women in Logic -- workshop associated to LiCS
Marcelo Finger <mfin...@ime.usp.br> escreveu: > Mesmo em eventos em que há a presença de algumas mulheres, a postura > é, em geral, masculina: um bando de gente batendo a mão no peito e > mostrando os dentes. :-D Essa frase raiou o meu dia, Marcelo! Além do mais, acho que ela aponta para um fator importante. Um estudo[1] publicado recentemente sobre a evasão de estudantes em filosofia nos EUA revela que um dos fatores que afastam estudantes, em particular as do sexo feminino, é o, digamos, "clima masculino" que domina a disciplina, especialmente o *esteriótipo masculino* do filósofo (podemos acrescentar também o lógico) e o *culto ao gênio*. Citando um trecho da mensagem do Morgan Thompson, um dos autores do estudo: "[...] it seems likely that the subtle ways in which philosophy instructors, texts, or stereotypes about philosophers contribute to this brilliance-based belief about success in philosophy partially explains why women leave (or simply don’t enter) the field. It’s likely that both the gendered stereotype of philosophy and brilliance-based beliefs about it are "in the air" such that students are influenced by them even before taking any college philosophy courses." Ademais, creio que o culto ao gênio influencie um pouco o clima de rivalidade, vaidade e egomania que se observa na disciplina. Durante a graduação, algumas colegas comentaram comigo que achavam o ambiente em filosofia um tanto hostil. Claro que falar em "clima masculino" e sugerir que mulheres são naturalmente aversas à confrontação pode reforçar ainda mais os esteriótipos[2]. Mas talvez o esteriótipo do gênio infalível seja prejudicial a todos estudantes, não somente as do sexo feminino. Notas: [1] http://dailynous.com/2016/03/31/why-do-undergraduate-women-stop-studying-philosophy/ [2] http://thecooperreview.com/non-threatening-leadership-strategies-for-women/ -- Hermógenes Oliveira -- 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/8737i1tkex.fsf%40camelot.oliveira.
Re: [Logica-l] Saiu o Qualis 2015 !
Joao Marcos <botoc...@gmail.com> escreveu: > [...] > > EM FILOSOFIA > [...] > Subiram de posição: > - Journal of Philosophical Logic Uma das coisas mais estranhas no Qualis (≤ 2014) da Filosofia era esse periódico estar classificado no extrato C. Journal of Philosophical Logic é pior que a revistinha dos alunos de graduação da minha antiga universidade?! Como pode isso? Fico contente que pelo menos essa anomalia tenha sido corrigida. *** A Revista Brasileira de Pós-Graduação publicou recentemente (ainda no prelo) alguns artigos sobre o Qualis. Dentre eles, me chamou a atenção um artigo da Profª Rita de Cássia Barradas Barata: Dez coisas que você deveria saber sobre o Qualis http://dx.doi.org/10.21713/2358-2332.2016.v13.947 A visão do Qualis apresentada pela Profª Rita de Cássia, em geral, faz sentido, porém temo que não corresponda muito à realidade de como o Qualis é, de fato, aplicado e encarado pela comunidade científica brasileira. Por exemplo, no artigo consta: "[...] o Qualis Periódicos não é uma ferramenta que possa ser utilizada em avaliações do desempenho científico individual de pesquisadores, visto que não foi desenvolvido com essa finalidade. Sua aplicação faz sentido para a análise coletiva da produção de um programa, cumprindo requisitos específicos do processo de avaliação comparativo estabelecido pela Capes. Em avaliações orientadas por princípios essencialistas, os instrumentos usados para comparações relativas nem sempre se mostrarão adequados." (§2, e algo similar na §10) Como justificar então o emprego do Qualis em editais de contratação e, algumas vezes, mesmo em critérios de promoção? Não seria compreensível que um Programa de Pós-Graduação (Faculdade, Departamento, Instituto etc.) queira contratar/promover alguém que aumente as chances do programa de ser melhor avaliado? Não seria ingênuo esperar que o Qualis, como instrumento de avaliação dos programas, não termine enfim afetando a avaliação *individual* de pesquisadores/professores? Afinal, a produção do programa nada mais é do que o conjunto da produção *individual* dos pesquisadores/professores atrelados ao programa. Dada a realidade de como o Qualis é aplicado, o conselho a seguir parece contraproducente: "Tendo em vista que a classificação é sempre feita a posteriori, conforme será detalhado em outro item, não é aconselhável que a lista sirva de referência para ações futuras, tais como a escolha de periódicos para submissão de artigos. A escolha de um periódico para a submissão deveria levar em conta, entre outros aspectos, o público-alvo do próprio artigo, o escopo dos diversos periódicos em um mesmo campo científico, a credibilidade, a rapidez no processo de julgamento e de publicação, a competitividade expressa pela taxa de rejeição, a circulação que os periódicos têm na comunidade de interesse e seu prestígio, o que pode ser indiretamente avaliado por diferentes medidas de impacto." (§2) A Profª Rita de Cássia também menciona (§6, último parágrafo) o chamado "mecanismo de indução" que consiste em inchar o Qualis de periódicos nacionais com o intento de aumentar o fator de impacto, algo que é facultado aos coordenadores de área (desde que aprovado pelo CTC-ES). Contudo, o funcionamento desse suposto mecanismo está baseado no fato de que o Qualis é, de fato, usado como referência na escolha de periódicos para submissão de trabalhos! O forte contraste entre a suposta função do Qualis e a aplicação prática do Qualis (entre o Qualis teoria e o Qualis prática) torna ainda mais evidente seus vários problemas. Saudações, P.S. Talvez o porquê do Journal of Philosophical Logic ter sido classificado como C tenha algo a ver com o que está exposto na §4 do artigo da Profª Rita de Cássia. -- Hermógenes Oliveira -- 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/87inqe74su.fsf%40camelot.oliveira.
[Logica-l] [fora do tópico] Nature's 10
Olá, pessoal. Alexandra Elbakyan, fundadora do SciHub, apareceu na lista da Nature de dez pessoas que fizeram a diferença na ciência este ano: http://www.nature.com/news/nature-s-10-1.21157 Num fórum de discussão sobre IA, alguém notou a ironia por traz disso pois, segundo o autor da mensagem, a Nature havia pressionado Demis Hassabis (outro dentre os dez) a retirar o "preprint" (disponibilizado na página do DeepMind) do artigo sobre o AlphaGO que havia sido publicado na Nature (eu mesmo não teria conseguido ler o artigo na época não fosse pela ajuda do João Marcos). Outro destaque da lista é, certamente, a Profª Celina. Saudações, -- Hermógenes Oliveira -- 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/87eg1273is.fsf%40camelot.oliveira.
Re: [Logica-l] Saiu o Qualis 2015 !
Samuel Gomes escreveu: > Isso de que o Qualis é só pra avaliar programas é só o que está "no > papel" dos documentos da CAPES - todo mundo sabe que ele vem sendo > usado como instrumento de avaliação individual, e isso tanto > extra-oficialmente como oficialmente (por exemplo, no programa de > pós-graduação que eu estou vinculado o professor para pedir para ser > credenciado tem que ter dois artigos de B2 pra cima nos últimos 5 > anos, sendo um nos últimos 3 anos - e isso está escrito no > Regimento!!!). Pois é, Samuel. E o problema maior é que o Qualis teoria, o Qualis no papel, é usado para refutar críticas e tentativas de melhorar a ferramenta. Crítica: Disciplinas menos tradicionais não são adequadamente representadas no Qualis. Refutação Qualis Teoria: O Qualis foi feito para avaliar *programas*. Portanto, o fato de disciplinas tradicionais carregarem mais peso, apenas expressa o desejo de ver essas disciplinas bem representadas nos programas de pós-graduação. Pesquisadores de disciplinas menos tradicionais não são prejudicados, pois o Qualis não deve ser usado para avaliação *individual*. Crítica: O Qualis não é exaustivo. Muitos periódicos, principalmente em áreas de pesquisa emergentes em território nacional não constam na base de dados. Refutação Qualis Teoria: O Qualis foi feito para avaliar *programas*. A maneira mais eficiente de avaliar a produção de programas é a posteriori. Portanto o Qualis não pode, nem deve, ser exaustivo. A ausência de periódicos da base de dados não afeta a pesquisa em áreas emergentes, pois o Qualis não deve ser usado para avaliação *individual*. Crítica: Em áreas que não adotam explicitamente critérios bibliométricos (fatores de impacto etc.), com todas suas maravilhas e misérias, o Qualis parece altamente sensível às convicções e agendas dos membros do comitê de avaliação. Refutação Qualis Teoria: O Qualis foi feito para avaliar *programas*. Nesse âmbito não há mesmo como escapar o julgamento de um comitê avaliador. O Qualis foi feito para auxiliar o comitê na avaliação dos programas e não prejudica ou privilegia pesquisadores específicos, pois o Qualis não deve ser usado para avaliação *individual*. E por aí vai... -- Hermógenes Oliveira -- 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/87d1gl3cht.fsf_-_%40camelot.oliveira.
Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3
Fernando Yamauti <fgyama...@gmail.com> escreveu: > Oi, > > Será que alguém teria acesso ao paper > > 1 Ladyman, J., Presnell, S.: Identity in Homotopy Type Theory, Part I: > The Justification of Path Induction. Philosophia Mathematica (2015) ? Coincidência. Eu li esse artigo recentemente. A versão que eu li está disponível em http://philsci-archive.pitt.edu/11079/1/Identity_in_HTT_public.pdf Sem contar o selinho da Oxford University Press, não sei se há muitas diferenças entre a versão acima e a versão oficial. Além das páginas tradicionais, https://homotopytypetheory.org/links/ https://ncatlab.org/nlab/show/homotopy+type+theory#References mais referências interessantes para quem estiver estudando Teoria Homotópica dos Tipos podem ser encontradas no repositório do grupo de estudos que estamos organizando aqui em Tübingen: https://github.com/BinderDavid/HoTT-StudyGroup -- Hermógenes Oliveira -- 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/87wpb1tpz7.fsf%40camelot.oliveira.
Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3
Eu escrevi: > [...] > > Uma exceção interessante é o caso da "Core Logic" de Tennant, onde a > negação é dada um caráter lógico, mesmo sem ECQ, pela admissão de > modus tollendo ponens (ou silogismo disjuntivo) e uma regra especial > para a implicação que permite obter ¬A,A⊢B. [...] Ops. Obviamente, o correto aqui seria "que permite obter ¬A⊢A→B". Mania de reler/revisar o que escreveu só depois de enviar. Foi mal. :-) -- Hermógenes Oliveira -- 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/87a87tof1w.fsf%40camelot.oliveira.
Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3
to demonstra, em terminologia corrente, a correção da lógica intuicionista (como sistema formal) com respeito a uma fundamentação baseada nas introduções (estilo BHK). Contudo, a contrapartida (a questão se todos os princípios de raciocínio justificáveis são de fato deriváveis intuicionisticamente), isto é, completude, em terminologia corrente, permanece em aberto no artigo, pois Martin-Löf não oferece nenhum argumento em seu favor. Os resultados mencionados anteriormente mostram que, sob certas condições que parecem razoáveis de um ponto de vista construtivo, uma fundamentação estilo BHK, quando formulada precisamente (uma vez que BHK é uma espécia de fundamentação (semântica) informal), justificaria inferências que não são intuicionisticamente deriváveis. Me parece que em ambos os quesitos, a) e b), a posição construtivista de vertente intuicionista, conforme tradicionalmente concebida, deixa muito a desejar. Confesso que, às vezes, me pergunto se o intuicionismo tradicional, como exemplificado pela tradição BHK, seria mesmo uma posição filosoficamente coerente. > [...] > > Ou ainda, outro problema que leva ao regresso infinito e a > identificação de um objeto do conhecimento com o conhecimento desse > objeto (que o Rodrigo havia comentado a um tempo atras de maneira > diferente). Um juízo do tipo 'A true' pode virar uma proposição onde > '(A true) true' se torna um juízo. E, mais. No ponto de vista > epistemico, essas duas coisas são equivalentes (saber que vc sabe é > igual a saber). Acho que o ponto de vista epistemico não bate com a > teoria, já que garantir que o tipo "A é habitado" não é equivalente > a A (em um dado universo), ou será que é? Ou seja, a justificativa > do ML não é adequada e só a teoria funciona. Na minha opinião, o potencial explanatório e de fundamentação da Teoria Intuicionista de Tipos (TIT) se estraçalha a partir do momento que se introduz universos. A partir daí, me parece, a TIT assume um caráter fortemente ad hoc e muitas da intuições iniciais vão para o espaço. Neste ponto, a única vantagem de TIT em comparação à ZF (sua concorrente igualmente ad hoc), principalmente se você é um computeiro ou matemático preocupado com computabilidade, é o fato de TIT ser construtiva. Por outro lado, os argumentos de que ZF seria filosoficamente mais robusta e conceitualmente mais coerente (ver, por exemplo, Harvey Friedman na FOM) não me convencem. Acontece que, dado que ZF é a doutrina ortodoxa, estamos acostumados a fazer vista grossa para as aberrações em ZF e maldizer excessivamente qualquer idiossincrasia de propostas alternativas, como TIT. De qualquer maneira, mesmo num contexto muito elementar, abordar o intuicionismo, ou construtivismo, de um ponto de vista epistemológico, tal como Martin-Löf faz, me parece um equívoco. Concordo ainda que a discussão epistemológica de Martin-Löf em conexão com a fundamentação da sua Teoria de Tipos é muito confusa, para se dizer o mínimo. A epistemologia, contudo, não é a única rota para o intuicionismo, e sequer me parece a melhor. No âmbito puramente lógico, uma rota mais interessante rumo ao intuicionismo passa pela filosofia da linguagem, em particular, por um certo pragmatismo linguístico. Neste sentido, princípios lógicos estariam apoiados em práticas linguísticas regradas (ver trabalho recente do Marcos Silva). Esse tipo de inferencialismo lógico ainda é muito incipiente, é verdade, mas me parece muito promissor. Saudações, Referências: [1] Arend Heyting. G. F. C. Griss and his negationsless intuitionistic mathematics. Synthese 9 (1):91-96, 1955. (ver referências nesse artigo para os escritos de Griss) [2] Ingebrigt Johansson. Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus. Compositio Mathematica 4, 119-136, 1937. [3] Neil Tennant. The Taming of the True. Clarendon Press, 1997. (ver também artigos no RSL sobre "Core Logic") [4] Peter Schroeder-Heister. The Categorical and the Hypothetical: A critique of some fundamental assumptions of standard semantics. Synthese 187 (3), 925-942, 2012. [5] Wagner de Campos Sanz, Thomas Piecha and Peter Schroeder-Heister. Constructive Semantics, Admissibility of Rules and the Validity of Peirce's Law. Logic Journal of the IGPL 22 (2), 297-308, 2014. [6] Thomas Piecha, Wagner de Campos Sanz and Peter Schroeder-Heister. Failure of Completeness in Proof-Theoretic Semantics. Journal of Philosophical Logic 44 (3), 321-335, 2015. [7] Per Martin-L\"of. On the Meanings of the Logical Constants and the Justifications of the Logical Laws. Nordic Journal of Philosophical Logic 1 (1), 11-60, 1996. -- Hermógenes Oliveira -- 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/87shllitep.fsf%40camelot.oliveira.
Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3
Joao Marcos <botoc...@gmail.com> escreveu: >> Eu, pessoalmente, acho ECQ um princípio *muito* suspeito. O >> difícil é que, sem ECQ, um construtivista ficaria basicamente sem >> negação (ao estilo do cálculo mínimo de Johansson), ou a negação >> cessaria de ser um operador *lógico*. > > Por quê, Hermógenes? Bem, o problema é o que colocar no lugar de ECQ que, ao mesmo tempo, (1) seja razoável se chamar de "negação" (ou, melhor, "absurdo", no caso da negação definida pelo absurdo), e (2) seja construtivamente justificável. Se permanecemos com a negação definida como ¬A≡A→⊥ *e não colocamos nada no lugar de ECQ*, então as nossas inferências dedutivas corretas são exatamente aquelas do fragmento mínimo sem negação e, do ponto de vista inferencial, não é possível distinguir o absurdo (⊥) de outra sentença qualquer: nós basicamente não teríamos a negação no âmbito das inferências lógicas. Obviamente, poderiamos ainda introduzir uma noção de incompatibilidade entre sentenças e, mantendo apenas as regras de inferência do fragmento mínimo, tratar a negação no âmbito extra-lógico: a negação deixa de ser um operador lógico (se entendemos por lógica apenas aquilo que está sendo capturado pelas nossas regras de inferência). Espero que agora esteja mais claro. Ou você estaria perguntando o porquê de eu achar ECQ um princípio suspeito? >> Martin-Löf, no artigo de fundamentação filosófica da sua Teoria dos >> Tipos[7], assume que as regras de introdução dão o significado das >> constantes lógicas e, a partir daí, justifica as regras de >> eliminação. > > E o que dizer do conectivo nulário de absurdo, que não possui regra > de introdução? Bem, segundo Martin-Löf, há uma regra de introdução para o absurdo (⊥): sob nenhuma circunstância podemos introduzir o absurdo (⊥). Isto é uma regra de introdução no sentido em que diz algo sobre as circunstâncias em que teríamos uma prova do absurdo (similar à cláusula BHK para o absurdo). Daí, ele justifica ECQ como regra de eliminação usando, inclusive, um exemplo não muito convincente envolvendo um chapéu. :-o Referências: [1] Per Martin-Löf. On the Meanings of the Logical Constants and the Justifications of the Logical Laws. Nordic Journal of Philosophical Logic 1 (1), 11-60, 1996. (disponível em https://github.com/michaelt/martin-lof) -- Hermógenes Oliveira -- 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/87k26wimgm.fsf%40camelot.oliveira.
Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3
ossa para as aberrações em ZF e maldizer excessivamente qualquer > idiossincrasia de propostas alternativas, como TIT. > > O problema que citei ('A true' =' 'A true' true' do ponto de vista > epistêmico) não tem relação com universos (eu não devia ter citado > universo no meu comentário) , apesar de ser mais fácil de internalizar > o juízo 'A true' nas proposições usando universos, i.e., enche o saco > escrever a definição de uma equivalência homotópica para definir 'A é > habitado'. Hum... Não consigo ver uma maneira de fazê-lo sem universos. Poderia me fornecer detalhes? Pode ser em privado, se você preferir. É possível ainda que eu não tenha compreendido muito bem o seu comentário. > Também acho que a definição de universo univalente é bem intuitiva e > consistente com a pratica matemática. O universo é só um objeto a mais > na teoria que mostra a compatibilidade da identidade com a > equivalência homotópica. Eles fazem o mesmo papel dos V_{\kappa}. E > como a TIT deve ser semântica e sintática ao mesmo tempo, acho natural > colocar um universo (ou melhor, uma estratificação em universos) na > teoria. Gostaria, portanto, de entender o que gera essa tal destruição > do potencial explanatório da TIT. O principal problema com os universos é que eles borram a distinção entre os juízos "A é um tipo" e "x tem o tipo A" (i.e. A é habitado). Na presença de universos, o juízo "B é um tipo" se reduz a um juízo da forma "x tem o tipo A" ou "x é um termo do tipo A", onde A é um universo. Tecnicamente, isso pode até ser muito conveniente, mas, filosoficamente, é desastroso. Sem me alongar muito, creio que a gravidade do problema pode ser depreendida de uma leitura atenta e refletiva do artigo de fundamentação do Martin-Löf[1]. Ali, ele discorre sobre a importância em se distinguir entre os juízos "A prop" ("A é um tipo", pois ali o único tipo tratado é o tipo das proposições) e "A true" ("x tem o tipo A", "o tipo proposicional A é habitado", "x é uma prova de A"). Esta distinção me parece importantíssima para o funcionamento da teoria como fundamentação filosófica. Quando se introduz universos, toda as intuições e coerência filosófica que estavam apoiadas nesta distinção vão para o espaço. Qual seria o valor como fundamentação filosófica de uma teoria construtiva se, todas as vezes que efetuo uma construção com base nos princípios básicos da teoria, tenho que verificar, *caso a caso*, se as construções são bem tipadas sob pena de inconsistência? A justificativa para a adição de universos é basicamente ad hoc: por que eles são necessários para se fazer matemática para além da aritméticazinha de primeira ordem. Nesse sentido, TIT+universos não me parece menos ad hoc do que ZF. Eu, particularmente, tenho a impressão de que a introdução irrestrita de universos é a maneira dos construtivistas de jogar a toalha, após o que Martin-Löf chamou de "segundo fracasso do programa de Hilbert"[2]. Agora, pode ser que universos sejam intuitivos e essenciais de um ponto de vista homotópico, mas, até o momento, a aspiração da Teoria Homotópica dos Tipos (THT) como fundamentação alternativa para a matemática está apoiada na Teoria Intuicionista de Tipos adjacente, uma vez que, até o momento, como você mesmo observou, as tentativas de oferecer explicações e justificativas para os elementos básicos da teoria por vias diretamente homotópicas, contornando a teoria de tipos, são insatisfatórias. > De qualquer maneira, mesmo num contexto muito elementar, abordar o > intuicionismo, ou construtivismo, de um ponto de vista > epistemológico, tal como Martin-Löf faz, me parece um > equívoco. Concordo ainda que a discussão epistemológica de Martin-Löf > em conexão com a fundamentação da sua Teoria de Tipos é muito > confusa, para se dizer o mínimo. > > Brouwer não fazia a mesma coisa? Aquela idéia de matemático ideal no > tempo me soa bem similar. Brouwer não fazia a mesma coisa. Fazia muito pior! De qualquer maneira, não considero Brouwer, Heyting, Martin-Löf, ou qualquer outro, como donos do intuicionismo. Creio que há razões para ser um intuicionista ou construtivista que independe da exegese desses autores. Referências: [1] Per Martin-Löf. On the Meanings of the Logical Constants and the Justifications of the Logical Laws. Nordic Journal of Philosophical Logic 1 (1), 11-60, 1996. (disponível em https://github.com/michaelt/martin-lof) [2] Per Martin-Löf. The Hilbert-Brouwer Controversy Resolved? In: One Hundred Years of Intuitionism (1907-2007), 243-256, 2008. (disponível em https://github.com/michaelt/martin-lof) -- Hermógenes Oliveira -- 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/87fuhkilsk.fsf%40camelot.oliveira.
Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3
Bruno Bentzen <b.bent...@hotmail.com> escreveu: > Oi Hermógenes, Olá, Bruno. > [...] > > PS: Posso estar enganado, mas acho um pouco equivocado e confuso usar > a palavra “completude” (um termo de cunho técnico ou meta-matemático) > neste caso quando estamos nos tratando de uma semântica informal ou > justificativa filosófica (até onde sei, o estudo de semânticas formais > para a lógica intuicionista nunca foi uma das preocupações principais > do Martin-Löf). De qualquer forma, não vejo porque as explicações de > significado não seriam “completas”, no sentido informal, para a MLETT, > que, repito, é a única das duas vertentes tradicionais de sua teoria > de tipos que interessa ao intuicionista. Você está correto em observar que as explicações semânticas de Martin-Löf não foram propostas como uma semântica formal e que o estudo de semânticas formais não tem lugar no espectro da obra dele. Porém, a questão da adequação das explicações semânticas pode ser levantada também no âmbito informal, como tentei indicar na minha mensagem original. Nas suas explicações semânticas, Martin-Löf toma as regras de introdução como primitivas (como aquelas que conferem significado às constantes lógicas) e justifica as regras de eliminação com base nelas. Se as regras de eliminação também fossem consideradas primitivas, ele não teria porquê se dar o trabalho de justificá-las com base nas regras de introdução. A questão agora surge: Será que as regras de eliminação justificadas por Martin-Löf são, de fato, as regras mais fortes que podem ser justificadas, tomando como base as regras de introdução? Isto é, seria possível fornecer regras de eliminação mais fortes que também sejam justificadas com base nas regras de introdução? Como se trata de uma semântica (explicação, fundamentação) informal, esta questão não pode ser respondida, no caso de Martin-Löf, com um teorema. Mas isso não significa que a questão é inócua ou desimportante, e, certamente, é uma questão que não pode ser afastada simplesmente sob o pretexto de que a semântica é informal. Martin-Löf fornece uma justificação, informal, obviamente, para as suas regras de eliminação (suas regras de eliminação estão *corretas*). Mas, é perfeitamente razoável se perguntar se haveriam outras regras de eliminação que pudessem ser justificadas e que resultariam numa lógica diferente da lógica intuicionista, que é a lógica alvo da semântica informal em questão. O que, com respeito a Martin-Löf, é um mero questionamento informal, se torna, no caso de Prawitz, uma conjectura[1], pois Prawitz, ainda que num estilo similar ao de Martin-Löf, fornece definições rigorosas que resultam, de fato, numa semântica formal. A conjectura de Prawitz é justamente uma versão formal da questão que estou discutindo: Seriam as regras de eliminação padrões as regras mais fortes que podem ser validadas do ponto de vista das regras de introdução? Os resultados que mencionei anteriormente sugerem que a resposta a essa conjectura possa ser "não". E, como esses resultados negativos incluem mesmo contraexemplos, é fácil traduzir os contraexemplos na forma de justificativas informais nos termos de semânticas informais como BHK e as explicações semânticas de Martin-Löf. De fato, eu já forneci a você, em conversa privada, uma justificativa informal em termos de BHK de uma inferência que não é intuicionisticamente derivável. Eu entendo a objeção que faz ao meu uso do *termo* "completude" no contexto de Martin-Löf, mas espero que tenha conseguido deixar claro que o uso que fiz de "completude" e "correção" naquele contexto se referia à *adequação* das explicações semânticas de Martin-Löf ao sistema de regras de inferência dedutivas que conhecemos como lógica intuicionista. Esta questão da adequação é legítima, não importa o quão informal seja a sua fundamentação (explicação, semântica). Gostaria ainda de deixar claro que estas minhas observações não afetam em nada a *utilidade* da TIT como teoria matemática e o fato de que suas propriedades construtivas, concordo com a Valéria nesse ponto, podem ser razões mais do que suficientes para favorecê-la em detrimento de ZF. Referências: [1] Dag Prawitz. An Approach to General Proof Theory and a Conjecture of a Kind of Completeness of Intuitionistic Logic Revisited. In: Advances in Natural Deduction, 269-279, 2014. -- Hermógenes Oliveira -- 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/874ly0e5sz.fsf%40camelot.oliveira.
Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3
Joao Marcos <botoc...@gmail.com> escreveu: >> Bem, o problema é o que colocar no lugar de ECQ que, ao mesmo tempo, >> (1) seja razoável se chamar de "negação" (ou, melhor, "absurdo", no >> caso da negação definida pelo absurdo), e (2) seja construtivamente >> justificável. >> >> Se permanecemos com a negação definida como ¬A≡A→⊥ *e não colocamos >> nada no lugar de ECQ*, então as nossas inferências dedutivas corretas >> são exatamente aquelas do fragmento mínimo sem negação e, do ponto de >> vista inferencial, não é possível distinguir o absurdo (⊥) de outra >> sentença qualquer: nós basicamente não teríamos a negação no âmbito >> das inferências lógicas. > > Por um lado, vale notar que há sim uma maneira neste caso de > distinguir a negação, vista como um conectivo com interpretação > parcialmente não-determinística aplicada a uma outra sentença qualquer > (note-se que a negação de uma sentença falsa é perfeitamente > determinística, usando a definição acima; o "problema" está apenas na > negação de sentenças verdadeiras), de uma sentença atômica arbitrária Uma maneira de resumir o meu comentário nesse contexto seria: Até que ponto seria razoável chamar isso de *operador lógico*? Isto é, eu hesitaria em chamar o conectivo que você descreve acima de operador lógico (assumindo que o entendi corretamente). No fim das contas, me parece, a questão é ideológica: uns vêem lógica em tudo, outros a procuram de dia com uma lâmpada na mão. :-) > note com efeito que a regra de substituição uniforme não se aplica ao > símbolo de absurdo, como um *conectivo* nulário, tal como se aplica a > sentenças atômicas. Bem, a regra de substituição uniforme não se aplica, de qualquer maneira, a conectivos (o quão marivolhoso seria se pudéssemos substituir conectivos à vontade, não é mesmo? :-D). Mas, considerando a *sentença* formada usando o conectivo nulário, não consigo ver porquê a regra de substituição seria problemática, assumindo, é claro, que esse conectivo não seja governado por ECQ ou qualquer outra regra de inferência, que era o caso que eu tinha em mente. Afinal, neste caso, o absurdo seria apenas uma sentença, embora pudéssemos conferí-la, extra-logicamente, um significado especial. > Por outro lado, não vejo porque deveríamos pensar sempre na negação > como conectivo *derivado*. Aliás, isto parece até uma ideia bem > ruinzinha, do ponto de vista de lógicas não-clássicas em que a > interdefinibilidade entre conectivos clássicos usualmente se perde > pelo caminho. De acordo. >> Bem, segundo Martin-Löf, há uma regra de introdução para o absurdo >> (⊥): sob nenhuma circunstância podemos introduzir o absurdo (⊥). >> Isto é uma regra de introdução no sentido em que diz algo sobre as >> circunstâncias em que teríamos uma prova do absurdo (similar à >> cláusula BHK para o absurdo). >> >> Daí, ele justifica ECQ como regra de eliminação usando, inclusive, um >> exemplo não muito convincente envolvendo um chapéu. :-o > > Hummm... Dualmente, qual seria a regra de eliminação do top? A regra > de que "sob nenhuma circunstância podemos eliminar o top"? Parece-me > um simples forçação de barra. Eu diria que não é apenas aparência... -- Hermógenes Oliveira -- 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/87zifscpcm.fsf%40camelot.oliveira.
Re: [Logica-l] A respeito de um Teorema de Tarski e uma historinha interessante
Walter Carnielli <walter.carnie...@gmail.com> escreveu: > > [...] > > Para os estudantes iniciantes compreenderem [...] o Axioma da Escolha > não é [...] falso [...] Me parece que "estudantes iniciantes", dependendo do seu grau de doutrinação em Lógica (especialmente lógica clássica ensinada como "teoria do bom raciocínio"), tenderiam a entender a afirmação acima como equivalente a "o Axioma da Escolha é verdadeiro" e estariam assim autorizados a solicitar-lhe, como justificativa dessa alegação, uma demonstração do *Axioma* da Escolha, visto que "axioma" aqui não pode ser tomado como verdade óbvia/evidente (conforme você mesmo escreveu). -- Hermógenes Oliveira -- 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/87pogvnbav.fsf%40camelot.oliveira.
Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3
Joao Marcos <botoc...@gmail.com> escreveu: > Assim que tivermos um critério de logicidade em mãos, portanto, > poderemos discutir melhor. :-) Eu diria que o problema não é a ausência de critérios de logicidade, mas a abundância deles. > Uma maneira de resumir o meu comentário seria: antes de dizer que algo > não é "razoável", convém deixar claras as nossas expectativas e as > regras do jogo. Perdão, eu pensei que estivesse claro. Se é que eu entendi bem o "conectivo" que você apresentou, minha hesitação inicial diz respeito exatamente ao fato dele ser apenas *parcialmente* determinado, isto é, sua semântica (valor semântico) estaria fixada apenas com relação a uma parte das sentenças da linguagem. Isso parece ir de encontro a algumas propriedades que são comumente atribuídas à logica e que, portando, deveríamos exigir de conectivos lógicos: neutralidade e universalidade. Esta posição, obviamente, não é sacrossanta. Por isso mesmo, eu não *afirmei* que o conectivo não era razoável, mas *questionei* até que ponto ele seria razoável. Também compartilhei a minha (pessoal) *hesitação* em aceitar o conectivo como conectivo lógico. Minha esperança era que isso fosse interpretado como um *convite* a uma defesa da logicidade do conectivo. Por fim, concedi que o núcleo da questão pudesse ser ideológica (ou, terminológica): alguns são mais liberais com uso do termo "lógica", ou "negação", outros são mais conservadores. Não vejo nenhum problema nisso. > (Tenho a impressão de que falhar repetidamente nesta tarefa converte > muito do que se faz em Teoria das Demonstrações em pregação com > caráter puramente ideológico.) Não entendi muito bem o que você quis dizer com isso, ou sua relevância para o tópico em questão, mas fico com a impressão de que talvez eu tenha, inadvertidamente, tocado em alguma ferida... Não sei muito bem o que você entende por "muito do que se faz em Teoria das Demonstrações", mas, no que diz respeito a "deixar claras as expectativas e regras do jogo" com relação a critérios de logicidade e constantes lógicas, eu diria justamente o contrário[1][2]. Obviamente, ninguém é obrigado a concordar, mas não há pobreza de argumentos. Além disso, só para deixar registrado, eu, pessoalmente, não vejo nenhum problema com "pregações com caráter puramente ideológico". > [...] > > Moral: um conectivo não é uma proposição atômica --- nem quando ambos > se parecem. Você poderia elaborar mais? Em particular, no caso de IL⁺ e hJ, dado que você admite[3] que este é extensão conservativa daquele, qual seria a diferença entre ⊥ e uma sentença atômica qualquer? O fato de que um deles eu escrevo assim "⊥" e o outro eu escrevo assim "p", ou assim "q"? (AKA don't you see? the signature is different!) Referências: [1] https://plato.stanford.edu/entries/logical-constants/#InfCha [2] Michael Dummett. The Logical Basis of Metaphysics. 1991. (capítulo 9, em especial a subseção "Conservative Extensions") [3] João Marcos. What is a Non-truth-functional Logic? Studia Logica 92:215-240, 2009. (página 230) -- Hermógenes Oliveira "The reasonable man adapts himself to the world; the unreasonable one persists in trying to adapt the world to himself. Therefore all progress depends on the unreasonable man." George Bernard Shaw -- 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/87pognl0xp.fsf%40camelot.oliveira.
Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3
Fernando Yamauti <fgyama...@gmail.com> escreveu: > Não. A minha sugestão é diferente. \neg A deve ser definido como A > \cong empty := \sum_{f: A --> empty} isequ (f) . Já iseq (f) é um > pouco mais complicado de escrever via email, portanto vou pedir que > olhe a pagina 78 do HoTT book Isso não faz muito sentido para mim. Em primeiro lugar, o termo sendo definido, ¬A, não aparece na definição (estou usando "0" para o seu "empty"): A≅0 := ∑(f: A→0) isequiv(f). A não ser que você já esteja tomando A→0 como definição de ¬A, mas aí a coisa fica ainda mais confusa. Em segundo lugar, não me parece muito conveniente, para se dizer o mínimo, uma abordagem que defina a negação em termos de tipos mais complexos como a soma ∑ (também conhecido como quantificador existencial) e tipos de igualdades (uma vez que isequiv(f) é definido de acordo com os tipos idA e idB para f: A→B). > Mas isso é considerado quando se usa tipos dependentes. De uma prova > hipotética \Gamma \vdash A e outra \Delta \vdash \Gamma se > concatenarmos tudo temos \Delta \vdash \Gamma \vdash A, ou seja, outra > prova hipotética, não? Sim. Mas esse não era o ponto. > [...] > > A introdução de 'A prop' como proposição até onde eu entenda serve > para evitar em falar de um domínio (onde as expressões variam) > contendo objetos de caráter semânticos e não puramente formais. Em > contrapartida em Analytic and Synthetic Judgements in Type Theory, ML, > inspirado por Church, introduz um tipo 'prop' (que é igual a 'set') e > usa 'A : prop' ao invés de 'A prop' . Além disso, ele introduz um tipo > 'type' e termos 'i (A) : prop' para cada tipo A. > > Portanto, de acordo com a sua afirmação, ML não estaria sendo > consistente? Não, não foi isso que eu quis dizer (eu acho). Você está trazendo mais e mais elementos para a discussão, e eu não estou conseguindo ver a relação deles com os meus comentários iniciais (isto não significa que não haja relação, somente que *eu* não estou conseguindo vê-la). Isso não é ruim, *em si*, mas eu já estou ficando meio velho e não tenho mais fôlego intelectual para discussões assim. Você poderia, por gentileza, tentar se focar naquilo que eu escrevi e responder ponto-a-ponto para que eu possa identificar exatamente aquilo que não ficou claro. > Desculpe-me, mas ainda estou falhando em entender o que vai para o > espaço. Creio eu que você esteja pensando em um problema diferente do > que eu mencionei acima : criar uma estratégia para A variar em > expressões completas ao invés de proposições, que tem um caráter > semântico. Espero que você tenha compreendido, pelo menos, que, com a introdução *irrestrita* de universos (i.e. com a introdução completa da hierarquia infinita de universos), nós perdemos a distinção entre os juízos "A é um tipo" e "x tem o tipo A" (i.e. "x é um termo do tipo A" ou "A é habitado"). Você poderia dizer: "Tá bem. E daí?" Bem, para compreender o tamanho da perda, é preciso apreciar o valor da distinção. Para isso, eu sugeri uma leitura atenta e *reflexiva* dos escritos mais *filosóficos* do Martin-Löf, com uma mente voltada para fundamentação. Não fornecerei uma explicação detalhada disso aqui na lista para não encher ainda mais o saco do pessoal que, a este ponto, já deve estar lotado de doutrina martin-löfiana. :-) -- Hermógenes Oliveira -- 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/87lgrbkxd6.fsf%40camelot.oliveira.
Re: [Logica-l] Lógica construtiva
Diogo Dias <diogo.bispo.d...@gmail.com> escreveu: Gostaria de pedir ajuda com duas perguntas. 1. É possível definir, na lógica clássica proposicional, uma noção de "construtível" de tal forma que se possa dizer que tal prova é construtível e, portanto, aceita intuicionisticamente? Dito de outro modo, é possível determinar uma restrição no conceito clássico de prova para limitá-lo a provas construtivas? Não sei se corresponde ao que você tem em mente, mas Gödel parece ter tratado essa questão[1][2]. *Grosso modo*, a lógica modal S4 corresponde ao cálculo proposicional intuicionista de Heyting se interpretarmos o operador modal como demonstrabilidade intuicionista. Nesse caso, portanto, teríamos uma teoria clássica, isto é, uma extensão da lógica clássica, que é capaz de expressar validade proposicional intuicionista. Num outro registro, reconhecer se uma demonstração clássica é aceita intuicionisticamente é algo relativamente simples em dedução natural. Basta colocar a derivação em forma normal. A demonstração é construtiva se, e somente se, não há aplicações da regra de redução ao absurdo clássica (ou, dependendo da formulação, outro princípio clásssico, como a Regra de Peirce). Referências: [1] Kurt Gödel. Eine interpretation des intuitionistischen aussagenkalküls. Ergebnisse eines mathematischen Kolloquiums, 4: 39-40, 1933. (ver excelente nota introdutória de Troelstra no "Collected Works", primeiro volume) [2] Sergei Artemov. Explicit provability and constructive semantics. Bulletin of Symbolic Logic 7 (1):1-36, 2001. (ver para exemplos de desenvolvimentos recentes da idéia Gödeliana) -- Hermógenes Oliveira -- 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/20170718110154.Horde.Mq_3njgpocjc-317SkaMBI8%40webmail.uni-tuebingen.de.
Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?
Anderson Nakano <andersonnak...@gmail.com> escreveu: > Boa tarde, pessoal. Olá, Anderson. > > [...] > > 1. Como o primeiro teorema da incompletude poderia ser construído em > sistemas formais da aritmética sem negação? Refiro-me, em particular, > ao sistema introduzido por Krivtsov em "A Negationless Interpretation > of Intuitionistic Axiomatic Theories". Não conheço o sistema de Krivtsov, mas gostaria de observar o seguinte. A demonstração de Gödel não depende de nenhuma noção semântica, seja a noção *semântica* de "negação" ou "verdade". Dado que a lógica clássica pode ser interpretada na lógica mínima[#], via lógica intuicionista, imagino que não seria difícil ajustar a noção Gödeliana de representabilidade à um sistema "sem negação", por exemplo, à um sistema no qual ¬A ≡ A → (1=0), com a noção de igualdade e desigualdade (diferença) determinada por axiomas construtivos adicionais. Desde que o sistema formal em questão seja poderoso o suficiente para representar sua própria sintaxe, é possivel diagonalizar e obtair daí uma sentença indecidível. Algo similar acontece com o teorema de Church: a tradução da lógica clássica na lógica intuicionista é comumente usada para transferir o resultado de indecidibilidade da lógica clássica de primeira ordem para o caso intuicionista. > > [...] > > 3. Além disso, a prova do primeiro teorema demonstra a > indecidibilidade da sentença G levando a hipótese da decidibilidade > (seja de G ou de ¬G) a uma contradição. Para um intuicionista que não > aceita que a refutação (P → ⊥) seja de fato o sentido da negação na > matemática (penso na linha de Freudenthal, Griss, ...) e que vão > trabalhar com axiomas para a relação de diferença (no lugar da > negação), não me é claro qual seria a interpretação correta do teorema > neste caso. A interpretação sintática do teorema permanece inalterada. Na minha hulmide opinião, interpretações semâmticas do teorema, que apelam a noções semânticas como "verdade" ou alguma noção semântica de "negação", *não fazem o menor sentido*. Mesmo no caso clássico. Nota: [#] Interpretações da lógica clássica na lógica intuicionista e mínima foram exploradas por Kolmogorov, Bernays, Gentzen e Gödel, dentre outros. Um apanhado geral dos resultados e traduções pode ser encontrado em: D. Prawitz and P. E. Malmnäs. A survey of some connections between classical, intuitionistic and minimal logic. In H. Arnold Schmidt, K. Schütte, and H. J. Thiele, editors, Contributions to Mathematical Logic, Proceedings of the Logic Colloquium, Hannover 1966, pages 215-229. North-Holland Publishing Company, 1968. -- Hermógenes Oliveira -- 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/878tk7te6a.fsf_-_%40camelot.oliveira.
Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?
Rodrigo Freire <freires...@gmail.com> escreveu: Olá Hermógenes, Olá, Rodrigo. Imagino que a "interpretação sintática do teorema" para um sistema S (digamos, para a aritmética de Peano) seja: há (construtivamente) uma sentença G tal que se S é (omega-)consistente, então G não é teorema e ~G não é teorema. É isso? Sim. Em linhas gerais, foi isso o que Gödel demonstrou em 1931, não? O problema é que só com essa "interpretação sintática do teorema" é impossível distinguir o teorema de Godel de uma trivialidade irrelevante como, por exemplo: Há uma sentença G da teoria de grupos (suposta consistente) tal que G não é teorema e ~G também não. De fato, sintaticamente, como sistemas formais sem algum tipo de "interpretação semântica", a aritmética de Peano e a teoria de grupos são o mesmo tipo de coisa. Onde estaria a diferença? De onde viria a pretensão de completude da aritmética de Peano, e por que isso estaria ausente na teoria de grupos, por exemplo? O estado medíocre do meu atual conhecimento de álgebra não me permite comentar com precisão o exemplo que você citou. Mas eu me interessei pelo exemplo e também planejo remediar a minha ignorância de álgebra, portanto referências pontuais são bem-vindas (pode enviar em privado). O que posso comentar no momento, assumindo aqui que o exemplo algébrico não é essencial à questão, é que, no caso de sistemas como AP (aritmética de Peano), no qual o vocabulário é exclusivamente matemático e os axiomas são tomados como determinantes exaustivos das noções matemáticas envolvidas, haveria sim a pretensão de que o sistema formal possa decidir qualquer sentença matemática A por meio de uma derivação de A ou de uma refutação de A. -- Hermógenes Oliveira -- 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/20170703111937.Horde.kV8xZb9MxZVutIIoGf1WlHp%40webmail.uni-tuebingen.de.
Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?
Anderson Nakano <andersonnak...@gmail.com> escreveu: Olá, Hermógenes. Muito obrigado pela resposta! Por nada. Uma pequena observação: nestes sistemas sem negação, não se trata apenas de tratar a negação como conectivo derivado (def., p. ex., ¬A ≡ A → (1=0)), mas de banir toda e qualquer "suposição não realizável" e, com isso, até mesmo o raciocínio hipotético (o "p → q") da matemática. Isso porque, vai alegar, digamos, o Freudenthal, uma suposição não realizada não é um "material construtivo" a partir do qual se poderia partir. Isso me parece exatamente a situação que temos no caso da lógica mínima onde não temos o princípio ECQ (ex contradictione quodilibet) que nos permitiria extrair conseqüências de "suposições não realizáveis". Em resumo, o enredo da minha sugestão seria o seguinte. A negação clássica pode ser interpretada na lógica intuicionista por meio da conhecida tradução de Gentzen-Gödel. Porém, ainda resta o princípio ECQ, característico da negação nos sistemais intuicionistas usuais, mas que não é aceito por construtivistas como Freudenthal e Griss. Contudo, ECQ pode ser interpretado numa lógica mínima por meio da disjunção. Aqui, em termos gerais, traduzimos uma sentença A por A∨⊥. Grosso modo, isto significa que, tendo em vista a regra de introdução da disjunção, A pode ser obtido pelas vias mínimas normais *ou por meio de ⊥*, simulando assim os raciocínios por ECQ. Note que "⊥" não precisa ser considerada uma constante lógica, mas pode ser uma sentença refutável qualquer (de acordo com os axiomas aritméticos subjacentes) como, por exemplo, 1=0. É claro, resta saber ainda se os sistemas sem negação aos quais você se refere permitem alguma noção de refutação, ou se há apenas a noção de demonstração. Isto é, resta saber se uma demostração de 1≠0 significa o mesmo que uma refutação de 1=0, ou se as noções de igualdade e desigualdade (diferença) são *completamente independentes* (i.e. não há nenhum axioma aritimético subjacente conectando, ou contrastando, as duas noções, o que seria bastante estranho). Enfim, ao que me parece, a aplicação dos resultados de Gödel a esses sistemas sem negação dependeria mais da teoria aritmética subjacente do que dos conectivos lógicos disponíveis. Não estou certo se a minha sugestão estaria correta, mas, independente disso, a questão que você levanta é bastante interessante. -- Hermógenes Oliveira -- 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/20170703103849.Horde.z-lGP8nnk-5NA2nGOLAke_Q%40webmail.uni-tuebingen.de.
Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?
Rodrigo Freire <freires...@gmail.com> escreveu: [...] O vocabulário da teoria de grupos é exclusivamente matemático, e os axiomas são tomados como determinantes exaustivos das noções matemáticas envolvidas (operação de grupo), muito mais que no caso da aritmética. Não sei se compreendi muito bem a analogia. Normalmente, a noção de grupo é definida como *uma* operação sob um conjunto de elementos que satisfazem determinados axiomas. Porém, diversas operações *distintas* satisfazem os axiomas de grupo. Em que sentido poderíamos dizer que os axiomas determinam exaustivamente a operação? Em contraste, você conseguiria ver como os axiomas de AP determinariam exaustivamente (ou pelo menos, possuem a pretensão de determinar exaustivamente) a noção de número natural? -- Hermógenes Oliveira -- 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/20170703143740.Horde.9xe98xEwRy44Xs6N4kGOSVa%40webmail.uni-tuebingen.de.
Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?
Rodrigo Freire <freires...@gmail.com> escreveu: Não. Não há um predicado para "número natural" que ocorre nos axiomas da aritmética [...] Então eu não sei o que você entende por axiomas de Peano. No meu livro, o primeiro axioma já reza: 1. O zero é um número natural. :-) [...] Alem disso, apelar para uma "noção de número natural" que aritmética pretende capturar já é introduzir um elemento semântico que vai além da sintaxe [...] Eu concordo com isso (talvez trocando "introduzir" por "reconhecer" ou "aceitar"). [...] justamente para avaliar a "limitação do formalismo". Mas *não* concordo com isso, ao menos da forma como está expresso. O fato de que reconhecemos noções pré-teóricas (supostamente de caráter semântico, embora não exatamente num sentido técnico do termo "semântico", e.g. Teoria dos Modelos) que nos guiam na formulação de sistemas formais não implica, *por si só*, limitações inerentes do formalismo. Não há diferença puramente formal entre o caso aritmético e o caso da teoria de grupos, o que trivializaria sim a relevância fundacional do teorema na ausência de algum elemento semântico (pois o caso da incompletude dos grupos é irrelevante). Bem, o teorema, conforme demonstrado em 1931, é puramente sintático e responde a uma importante questão de *decidibilidade formal* que havia sido formulada e estudada no contexto da Escola Hilbertiana desde o início do século passado. Portanto, acho que podemos concordar que o teorema, mesmo na sua formulação original sintática, *não* é trivial. Quanto à uma suposta "relevância fundacional" que só poderia ser reconhecida numa interpretação semântica do teorema, eu não saberia dizer. Como observei anteriormente, as interpretações semânticas do teorema, assim como tentativas de formular e demonstrar o teorema em termos semânticos não fazem o menor sentido para mim. Claro, esta observação pode ser tomada como nada além de evidência da minha própria ignorância e/ou incapacidade. Para mim, contudo, ela constitui evidência de que a interpretação semântica do teorema, juntamente com seus usos e abusos em alegações sobre os "limites da matemática" (ou formalismo) e "existência de sentenças verdadeiras indemonstráveis", não passam de histórias pra boi dormir. Porém, eu continuo sinceramente buscando evidências contrárias, e, em vista das informações do JYB, estou curioso para saber o que Kripke tem a dizer sobre o assunto. Até agora, contudo, apresentações "semânticas" do teorema de Gödel tem me decepcionado, inclusive aquelas presentes no excelente livro de Smullyan sobre o assunto. -- Hermógenes Oliveira -- 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/20170703164531.Horde.8p6u9YWznSErZ9myGml-znU%40webmail.uni-tuebingen.de.
Re: [Logica-l] lógica, pra quê?
Joao Marcos <botoc...@gmail.com> escreveu: [...] A propósito, há um outro paper do Sesardic (com Rafael De Clercq) [2] que comenta sobre a *disparidade de gênero* na área de Filosofia e coloca em questão as alegadas evidências da hipótese segundo a qual haveria algum tipo de *discriminação* contra as mulheres na área de Filosofia. [...] [2] Women in Philosophy: Problems with the Discrimination Hypothesis https://www.nas.org/articles/women_in_philosophy_problems_with_the_discrimination_hypothesis Obrigado pela referência João Marcos. Esse artigo é um ótimo exercício em sofismas! Ele não sobrevive aos próprios padrões que pretende aplicar aos trabalhos que critica e emprega os clássicos _falácia do espantalho_, _apelo à ignorância_, _falsa dicotomia_ e _petição de princípio_. Isto se revela a qualquer um que esteja familiarizado com a literatura citada pelo próprio artigo, mas vou fazer um breve apanhado como aperitivo. a) Alguns pontos do artigo argumentam contra espantalhos de Haslanger, Saul e Beebee. Por exemplo, Haslanger realmente escreve que "the data mostly speak for themselves". Essa citação é tirada fora de contexto para sugerir que Haslanger faz um salto ilegítimo da "disparidade de gênero" para "discriminação". Quando se lê o texto de Haslanger, porém: 1. Está claro que ela toma os dados como evidência da *disparidade de gênero*, o que, de fato, *pode* ser concluído dos dados a despeito da afirmação de Sesardic de que "the data don’t speak for themselves at all. Without additional information, it is impossible to draw *any* conclusion". 2. Haslanger então prossegue a *problematizar os dados* e sugere explicações para a disparidade, *uma* das quais é a discriminação ("outright discrimination"). Outras explicações incluem "Gender Bias" e "Stereotype Threat", coisas que Sesardic, aparentemente, joga tudo no mesmo saco. Mas, mesmo aqui, Haslanger concede que "Based on the limited data I’ve gathered (for example, I don’t have data on submission), I cannot argue that evaluation bias *is* playing a role in publication in philosophy." (ênfase dela) 3. Diferente do que sugere Sesardic, Haslanger está discutindo a disparidade de gênero em *publicações* e não em comitês de contratação. A tabela citada por Sesardic relacionando o número de mulheres nos programas de pós-graduação americanos é usado por Haslanger somente para constrastar o número de mulheres ativas em áreas da filosofia com o números de publicações por mulheres nas mesmas áreas. 4. Em nehum dos trabalhos citados no artigo de Sedardic, Haslanger sugere "a prima facie case for anti-woman hiring bias" ou recomenda cotas ou quaisquer outras medidas de reparação do mesmo. b) Sesardic oferece duas possíveis alternativas que explicariam a disparidade de gênero, mas que seriam livres da hipótese de discriminação: "gender differences in abilities" e "gender differences in interests". A segunda delas *não* está livre da hipótese de discriminação, pois, como o próprio Sesardic explica mais adiante, um ambiente de discriminação pode levar mulheres a desenvolver menos interesse por filosofia. A primeira delas, além de ser completamente ridícula, possui muito menos evidência em seu favor do que a hipótese criticada por Sesardic. c) Ao mesmo tempo que exige alta robustez estatística de estudos que apontem a presença de discriminação, Sesardic cita trabalhos baseados em "estimativas", como o de Andrew Irvine. d) Os estudos canadenses mencionados como evidência de que mulheres não seriam discriminadas ou seriam até mesmo favorecidas em contratações foram realizados num período em que universidades canadenses implantaram fortes medidas, incluside envolvendo cotas, favorecendo a contratação de mulheres. A despeito da paridade relativa em contratações recentes, em termos absolutos, a disparidade é enorme (veja relatório sobre a Universidade de Western Ontario citado por Sesardic). e) Quando se trata de discutir "Bias" em pesquisa, Sesardic cita estudos da área de medicina, onde a disparidade de gênero é bem menor. f) Mesmo aqui, Sesardic cita o estudo de Sandström & Hällsten como contraposto ao estudo anterior de Wennerås & Wold quando, na verdade, o estudo de Sandström & Hällsten pertende mostrar como medidas adotadas pelo governo Sueco ajudaram a amenizar os problemas relatados por Wennerås & Wold (tanto na questão de gênero quanto na questão do nepostismo). Enfim, as falácias e deturpações são numerosas. Quando terminei de ler o artigo, fiquei me perguntando se não se tratava de uma piada... -- Hermógenes Oliveira -- 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
Re: [Logica-l] Gaisi Takeuti (1926-2017)
Recollections of Prof. Takeuti by Norbert Preining: https://www.preining.info/blog/2017/05/gaisi-takeuti-1926-2017/ -- Hermógenes Oliveira -- 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/87k25mpdrk.fsf_-_%40camelot.oliveira.
Re: [Logica-l] the most influential living philosophers
Marcos Silva <marcossilv...@gmail.com> escreveu: > https://thebestschools.org/features/most-influential-living-philosophers/ > > e aí? concordam com a (controversa) lista? Lembrando que a lista contém apenas filósofos *vivos* e que o critério de seleção é a *influência* ou prestígio, me parece que ela abre pouco espaço para controvérsia. Eu reconheço por volta de 80% dos nomes na lista, o que indica que esses nomes são mesmo influentes, pois minha familiaridade com o vasto corpo de discussão filosófica contemporânea é bastante limitado. A maioria dos nomes não me causaram nenhuma surpresa: Cornel West, Charles Taylor, Slavoj Žižek, Martha Nussbaum, John Searle, Graham Priest, Noam Chomsky, David Chalmers, Peter Singer, Alain Badiou, Robert Brandom, Saul Kripke, Jürgen Habermas, Daniel Dennett. Esses são certamente filósofos *muito* influentes. Outros nomes causaram uma surpresa inicial: Jaegwon Kim, Christine Korsgaard, Nancy Cartwright, Tyler Burge e Susan Haack. Mas, pensando bem, esses filósofos são realmente influentes em suas respectivas áreas de especialização. William Lane Craig também me surpreendeu, mas deve-se reconhecer que o sujeito conquistou muita influência devido ao deplorável debate teísmo vs. ateísmo, religião vs. ciência. -- Hermógenes Oliveira -- 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/87h8vzqg0y.fsf%40camelot.oliveira.
Re: [Logica-l] um probleminha com logica intuicionista...
Valeria de Paiva <valeria.depa...@gmail.com> escreveu: [... ] (¬φ → ¬χ) → (χ → φ) (Law of contraposition) mas essa ultima assercao nao 'e o que eu chamaria de contraposicao. Contraposicao usual 'e valida em logical intuicionista. o que acontece e' que essa assercao combina contraposicao com eliminacao da negacao dupla, ou seja: contraposicao devia ser (A → B) → (¬B → ¬A) mas quem escreveu o artigo em vez de dizer (¬A → ¬B) → (¬¬B → ¬¬A), removeu a dupla negacao, ficando com (¬A → ¬B) → (B → A) dai que isso 'e mesmo nao-derivavel em IL, pois inclui double negation elimination, junto com a contraposicao. voces concordam? ou eu estou "esquecendo" alguma coisa importante? Eu concordo contigo, Valéria. Tradicionalmente, "contraposição" é o nome dado à (A → B) → (¬B → ¬A). Curiosamente, a primeira vez que eu vi a "contraposição" apresentada como divisora de águas entre lógica clássica e intuicionista foi no vídeo da palestra da Elaine Pimentel, "A semantical view of proof systems", no Filomena 2017 (divulgado recentemente nesta lista). Na ocasião, pensei "Peraí...", pausei o vídeo e raciocinei basicamente o que você apresentou acima. A Elaine apresentou o negócio como uma regra de inferência que permitiria estabelecer A → B por meio de derivação de ¬A a partir de ¬B. Devo admitir, contudo, que apresentado assim, como regra de inferência, o nome "contraposição" não me parece *tão* estranho. Eu não sei porque (¬A → ¬B) → (B → A), com o nome "contraposição", tem sido usado como diferenciador entre lógica clássica e intuicionista, mas isso parece ser um desenvolvimento recente (a palestra da Elaine e o artigo da Wikipédia sendo os únicos casos que me lembro até agora). Talvez tenha aparecido em algum livro ou artigo e as pessoas passaram a adotar essa caracterização. Eu não gosto muito, pois tem grande potencial para causar confusão. tem mais alguma coisa errada no artigo? eu estou querendo me lembrar da relacao entre implicacao e disjuncao. essas estao certas? Disjunction versus implication: (φ ∨ ψ) → (¬φ → ψ) Esta está correta. Basta aplicar ∨E com premissa menor ψ, obtida, respectivamente, (1, [φ]) por ECQ a partir de φ (descartado) e ¬φ, e (2, [ψ]) ψ (descartado). Daí é só introdizir as implicações. (¬φ ∨ ψ) → (φ → ψ) Esta tambeḿ está correta. Basta substituir φ por ¬φ na justificativa acima. Mas talvez a relação mais interessante entre disjunção e implicação seja dada por φ ∨ ψ ⇔ ∀χ (φ → χ) → ((ψ → χ) → χ)) que é, basicamente, uma tradução da regra de eliminação em segunda ordem (com quantificação sobre sentenças), também chamado de sistema Fₐₜ na literatura recente. Essa relacão é inclusive usada no artigo da Wikipédia que você mencionou para oferecer um *esquema* axiomático alternativo para a lei do terceiro excluído (φ ∨ ¬φ): (φ → χ) → ((¬φ →χ) → χ). -- Hermógenes Oliveira -- 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/20171024103907.Horde.StcBDM_NGGFij6cUvk478_N%40webmail.uni-tuebingen.de.
Re: [Logica-l] sobre a "melhor forma" de apresentar a negação em lógicas construtivas
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.
Re: [Logica-l] Dúvidas sobre Dummett
Diogo Dias <diogo.bispo.d...@gmail.com> escreveu: Olá! Olá, Diogo. Eu estou estudando Dummett e sua teoria do significado. Em diversas ocasiões, ele defende a necessidade de distinguir entre prova e prova canônica, sendo que a última seria responsável por determinado o significado dos conectivos lógicos. Não obstante, não há uma definição precisa de prova canônica, e ele próprio reconhece isso. Gostaria de saber se alguém tem indicações de textos em que essa noção é definida com precisão. Dummett oferece uma definição precisa de argumento canônico em _The Logical Basis of Metaphysics_, em particular os capítulos 11 ao 13 (infelizmente, desconheço traduções deste livro para o português ou espanhol). Definições alternativas podem ser encontradas em diversos artigos de Prawitz, Martin-Löf, Schroeder-Heister, Göran Sundholm, Tor Sandqvist e outros. Contudo, dependendo do caso, essas definições podem se distanciar bastante da perspectiva de Dummett. Em particular, estou investigando se, e como, é possível gerar lógicas diferentes a partir de formalizações diferentes da noção de prova canônica. Dummett oferece duas definições distintas de validade lógica: uma com base nas regras de introdução, e outra com base nas regras de eliminação. As definições não pressupõe nenhuma lógica específica de antemão e poderiam, *em princípio*, ser aplicadas a qualquer lógica bem-comportada (normalização, propriedade da subfórmula). Por exemplo, as definições com base nas regras de eliminação podem ser levemente adaptadas de modo a obter lógicas subestruturais, como a lógica relevante. Eu estou trabalhando com isso no momento e, se você quiser, podemos discutir os detalhes em privado (para não incomodar a lista). -- Hermógenes Oliveira -- 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/2018005547.Horde.u3Xq_olxYd4hCleCkbl45C8%40webmail.uni-tuebingen.de.
Re: [Logica-l] Dúvidas sobre Dummett
Diogo Dias <diogo.bispo.d...@gmail.com> escreveu: > Quando disse que Dummett não apresenta uma definição precisa de prova > canônica, estava pensando nas seguintes citações: > > "What exaclty the notion of a canonical proof amounts to is obscure" > (The Philosophical Basis of Intuitionistic Logic, p. 241), e "no one > can at present give a detailed account of canonical proofs even of > statements of first order arithmetic." (Elements of Intuitionism, > p. 400) Ao que me parece, Dummett tinha em mente nessas citações um contexto mais amplo do que o da lógica pura: o contexto da aritmética ou mesmo da matemática em geral (análise e etc.). Isso está inclusive explícito no caso da segunda citação. Enquanto a tese da canonicidade parece bastante natural e plausível no âmbito da lógica pura, a coisa complica quando passamos para a aritimética de primeira ordem ou teorias matemáticas mais complexas. Problemas similares aparecem quando tentamos aplicar a tese da canonicidade à teorias empíricas. O próprio Dummett chega a discutir vários problemas com a tese da canonicidade (ali tratada como "hipótese fundamental") em contextos extra-lógicos, tanto empíricos quanto matemáticos, no capítulo 12 do "The Logical Basis of Metaphysics". > Obrigado pela indicação do Logical Basis of Metaphysics. Acabei de ler > os capítulos que você mencionou e, de fato, ali ele apresenta uma > definição precisa dessa noção. Li, também, o texto Meaning approached > via proofs, do Prawitz, em que ele apresenta outro possível tratamento > de prova canônica, e compara com o do Dummett. > > Meu interesse no tema é o seguinte: Eu estou atualmente estudando > pluralismo lógico, e estou investigando se alguns argumentos que, a > princípio, foram propostos como uma defesa de um tipo de monismo > lógico, podem ser interpretados como dando margem à legitimidade de > lógicas distintas. No caso do Dummett, me parece que, variando o > tratamento da noção de prova canônica, mas respeitando as restrições > gerais da sua proposta (normalização, harmonia, molecularidade da > linguagem etc), é possível gerar lógicas distintas. > > Você poderia me indicar alguns artigos desses autores que você > mencionou que fazem isso? Em particular, fiquei interessado na > possibilidade de obter uma lógica relevante mantendo o framework do > Dummett. Quanto à semântica Dummettiana para lógica relevante e outras lógicas subestruturais, me referia a um trabalho preliminar meu e de dois co-autores, Mattia Petrolo e Eugenio Orlandelli. Nosso impulso é, em linhas gerais, exatamente a que você descreveu acima: trazer uma perspectiva pluralista para o monismo característico do inferencialismo semântico da tradição Prawitz-Dummett. Nós apresentamos nosso trabalho em alguns congressos, mas ainda não temos nada publicado. Infelizmente, não conheço nenhuma pesquisa nessa linha além da nossa, portanto não tenho muito o que indicar. No que concerne o nosso trabalho, a ideia é bastante simples. Grosso modo, basta observar que a noção de argumento canônico de Dummett trabalha com argumentos hipotéticos (com hipóteses abertas), em vez de provas fechadas. Uma vez que as hipóteses são incorporadas de modo essencial na abordagem, podemos refinar o tratamento das hipóteses de modo a obter lógicas subestruturais. Por exemplo, nas defininições baseadas nas regras de eliminação, argumentos válidos são predicados, grosso modo, na possibilidade de transformar certos argumentos canônicos em outros argumentos canônicos que dependem, *no máximo*, das mesmas hipóteses. Se, em vez disso, exigirmos que os argumentos canônicos resultantes dependam *exatamente do mesmo conjunto de hipóteses*, temos uma lógica relevante (sem a lei de distribuição) similar àquela de Prawitz (1965, Cap. VII). Se, além disso, coletamos as hipóteses em multiconjuntos, em vez de conjuntos, temos um fragmento da lógica linear intuicionista (sem exponenciais). E por aí vai. -- Hermógenes Oliveira -- 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/87wp0of8tn.fsf%40camelot.oliveira.
Re: [Logica-l] Arquivo digital do Die Grundlagen der Arithmetik: Centenarausgabe mit ergänzenden Texten (1986 - Christian Thiel)
João Paulo Carneiro <jpcb...@gmail.com> escreveu: > > [...] > > Estou buscando o texto que citei no título deste tópico (Die > Grundlagen der Arithmetik: Centenarausgabe mit ergänzenden Texten - > 1986 - Christian Thiel). Trata-se de uma edição comemorativa do > centenário do famoso Die Grundlagen der Arithmetik de Frege. O que me > interessa no livro, interesse oriundo das minhas investigação no > doutorado, são os "ergänzenden Texten" (textos suplementares) que o > editor apresenta nessa versão. Já fiz buscas do formato digital (a > versão impressa custa por volta de R$ 600,00) em vários domínios na > internet, mas sem sucesso até o momento. Gostaria de solicitar que, > caso alguém tenha o formato digital dessa obra (ou consiga a partir do > material físico), o compartilhasse comigo (e outros possíveis > interessados aqui no grupo). Os textos suplementares dessa edição consistem meramente de resenhas e reações ao livro de Frege que apareceram em outros lugares. A maioria desses textos, talvez mesmo todos eles, estão disponíveis na rede (domínio público). Veja o índice da edição: http://digitool.hbz-nrw.de:1801/webclient/DeliveryManager?pid=1804014%5Fatt%5F2=simple%5Fviewer Os textos suplementares estão listados na seção "Das Echo der Grundlagen". Por exemplo, o primeiro texto listado ali, a resenha de Hoppe, publicado no Archiv der Mathematik und Physik, está disponível pelo archive.org (p. 486 nesta digitalização): https://archive.org/details/archivdermathem14unkngoog Para os outros textos, aconselho procurar também no DigiZeitschriften: http://www.digizeitschriften.de Os artigos na Wikipedia alemã também costumam indicar versões digitalizadas de revistas e livros antigos disponíveis na rede. Por exemplo, a resenha de Cantor foi publicada no Deutsche Literaturzeitung: https://de.wikipedia.org/wiki/Deutsche_Literaturzeitung Digitalizações estão listadas ali no Wikisource. P.S. Estranho que você tenha encontrado a edição impressa por R$ 600,00... Na livraria regional aqui, ela sai por € 19,00! -- Hermógenes Oliveira -- 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/87y3j05lvn.fsf%40camelot.oliveira.
Re: [Logica-l] #OFF A Vida de Ada Lovelace
Adolfo Neto escreveu: Aproveito e pergunto: que outra mulher na lógica poderia ser tema de um livro infantil? Rózsa Péter, sem dúvida. [1] https://en.wikipedia.org/wiki/R%C3%B3zsa_P%C3%A9ter [2] http://www-groups.dcs.st-and.ac.uk/~history/Biographies/Peter.html Uma bela história de perseverança. Ela sobreviveu o gueto em Budapeste durante a Segunda Guerra (ainda que tenha perdido amigos e um irmão), perdeu manuscritos por conta dos bombardeios (mas os recriou e publicou posteriormente). Buscou consolo na poesia após descobrir que os resultados de seu trabalho em teoria dos números já haviam sido publicados por outros. Retornou à matemática no âmbito da lógica, especializando em funções recursivas. Na literatura sobre funções recursivas em língua alemã, de Felscher a Hermes, a influência do trabalho dela é praticamente onipresente. As anedotas sobre como um colega a convenceu a se dedicar à matemática ("it is not that I am worthy to occupy myself with mathematics, but rather that mathematics is worthy for one to occupy oneself with") e sobre o ensino do algorítimo de Euclides no ensino fundamental são absolutamente encantadoras[2]. -- Hermógenes Oliveira -- 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/20181018095342.Horde.rfp2BXMbp7URXqSw4GSwREm%40webmail.uni-tuebingen.de.
[Logica-l] Georg Cantor e seus rivais
Olá, pessoal. Como o João Marcos já esclareceu, nossa discussão revela uma certa confusão entre a demonstração de que os números naturais podem ser relacionados bijetivamente com os números (im)pares (ou outros supostos subconjuntos próprios dos naturais), ideia cuja origem precede Cantor (Galileu, Dedekind e outros), e o argumento diagonal de Cantor que mostra que os números reais tem cardinalidade diferente daquela dos números naturais. O primeiro argumento de fato não assumi nada sobre a natureza do infinito, mas o segundo, ao menos em sua formulação mais comum, aparentemente pressupõe totalidades infinitas completadas, ainda que seja um argumento por redução ao absurdo (posso elaborar esse ponto, se alguém sentir que é necessário). O primeiro argumento é relativamente incontroverso, mas o argumento diagonal tem sido ocasionalmente contestado, algumas vezes por gente aparentemente competente. Wilfrid Hodges escreveu um artigo muito interessante à respeito: An editor recalls some hopeless papers. The Bulletin of Symbolic Logic. Volume 4, Issue 1, March 1998. Postscript file available at: http://www.math.ucla.edu/~asl/bsl/0401-toc.htm Aqui na Alemanha, Wolfgang Mückenheim[1] causa bastante polêmica sobre o assunto. Ele tem participado de discussões, muitas delas pouco produtivas, em fóruns virtuais como o sci.math (assinando sempre com suas iniciais "WM"), embora, algumas vezes, essas discussões revelem informações históricas interessantes[2]. Algumas pessoas tem exigido que, por conta de suas ideias controversas no que concerne o infinito e a teoria de conjuntos, Mückenheim seja removido e proibido de lecionar, uma sugestão certamente inapropriada. É curioso que a teoria Cantoriana dos conjuntos atraia tanta confusão e tantos rivais. Ao que me parece, um dos motivos pode ser sua difusão descuidada por meio de alegações aparentemente fantásticas, como a de que existem infinitos maiores que o infinito (sem esclarecer o conceito de cardinalidade e o que "maior" significa nesse contexto). Algo similar ocorre com os teoremas de Gödel e alegações sobre verdades matemáticas indemonstráveis ou incognoscíveis, ou sobre o poder relativo entre mentes e máquinas de Turing. Para piorar, tanto Cantor quanto Gödel foram tentados pelo misticismo fantástico (por exemplo, tentando relacionar seus resultados com teologia) e, no ambiente altamente personalista que vigora na ciência atualmente, eles são ocasionalmente tomados, sem muita reflexão, como autoridades. Por falar na exaltação de cientistas, um documentário recente sobre o Cantor (em alemão, legenda em alemão disponível): https://www.ardmediathek.de/tv/MDR-Dok/Georg-Cantor-Der-Entdecker-der-Unendli/MDR-Fernsehen/Video?bcastId=17603862=50543922 https://www.ardmediathek.de/tv/MDR/Georg-Cantor-Der-Entdecker-der-Unendli/mdr-de/Video?bcastId=15123138=50613182 (mesa redonda sobre o documentário) Notas: [1] https://de.wikipedia.org/wiki/Wolfgang_M%C3%BCckenheim [2] https://de.sci.mathematik.narkive.com/LWMTIIfp/kronecker-und-cantor -- Hermógenes Oliveira -- 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/20181105113306.Horde._XjrupCF0TF0CcOc62JvsM6%40webmail.uni-tuebingen.de.
Re: [Logica-l] "All I am saying is to give Ps (and Qs) a chance."
ue se revelaram inconsistentes). Independente de serem perfeitos, os métodos estatísticos da corrente conexionista recentemente obtiveram grandes sucessos enquanto os almejos simbolistas das décadas de 60 e 70 permanecem, em grande medida, como promessas. Impressiona que o financiamento[10], a empolgação e a especulação pseudocientífica esteja favorecendo os conexionistas e seus métodos de aprendizado de máquina? Notas: [1] https://twitter.com/JeffDean/status/1065342676143243265 [2] https://medium.com/backchannel/has-deepmind-really-passed-go-adc85e256bec [3] https://en.wikipedia.org/wiki/AlphaGo_Zero [4] https://en.wikipedia.org/wiki/AlphaGo_versus_Lee_Sedol#Game_4 [5] https://youtu.be/yCALyQRN3hw?t=11406 [6] https://youtu.be/yCALyQRN3hw?t=12152 [7] https://www.youtube.com/watch?v=HT-UZkiOLv8 [8] https://youtu.be/yCALyQRN3hw?t=21327 [9] http://users.ox.ac.uk/%7Ejrlucas/Godel/mmg.html [10] http://cyber-valley.de/en -- Hermógenes Oliveira "If you give someone Fortran, he has Fortran. If you give someone Lisp, he has any language he pleases." Guy L. Steele -- 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/87tvjmkcnw.fsf%40camelot.oliveira.
[Logica-l] [META] Sobre uma questão técnica de configuração da lista
Mario Benevides escreveu: Peço desculpas por ter enviado uma mensagem pessoal para o Jean na lista. Ana Paula observou: Agora todo mundo da lista sabe seu número de telefone. Pessoal, A nossa lista pratica o famigerado "Reply-To Munging"[1]. Isto significa que, ainda que você escolha a opção "Responder" em vez de "Responder a todos" (responder para a lista), a sua mensagem será *automaticamente* endereçada para a lista. Algumas listas aderem a esta prática numa tentativa de direcionar para a lista discussões que eventualmente aconteceriam em privado (não sei se esta é a motivação no nosso caso). Assim que notei esta configuração, quando comecei a participar ativamente há alguns anos atrás, conversei com os então administradores a respeito. Apesar dos incidentes[2] que, volta e meia, acontecem na nossa lista, a coisa acabou ficando do jeito que estava. Isto não me afeta pessoalmente, pois o meu gerenciador de mensagens possui um antídoto[3]. Mas, para a maioria das pessoas, responder a uma mensagem da lista em privado provavelmente requer que se altere *manualmente* os campos de endereçamento do E-mail. Ademais, a prática de "Reply-To Munging" parece estar em conflito com o tipo de convívio que esperamos da nossa lista[4], pois incentiva, indiretamente, o clima de sala de bate-papo e rede social. O propósito desta mensagem *não* é, de forma alguma, reclamar da administração da lista (passada ou atual). A intenção é apenas levar ao conhecimento dos membros uma questão técnica que, provavelmente, tenha passado despercebida, e sugerir que, talvez, convenha repensar o atual estado de coisas. Notas: [1] http://marc.merlins.org/netrants/reply-to-still-harmful.html [2] Apenas um aperitivo, uma lista completa seria muito longa para incluir aqui: https://groups.google.com/a/dimap.ufrn.br/d/msg/logica-l/I6kFjUAerj8/x-PZ3A-H83gJ https://groups.google.com/a/dimap.ufrn.br/d/msg/logica-l/4OXfJaRRzuk/pZwAYt5TFgAJ https://groups.google.com/a/dimap.ufrn.br/d/msg/logica-l/dAbP6w2kx8w/Lf4cFjCsBwAJ [3] https://www.gnu.org/software/emacs/manual/html_node/gnus/Group-Parameters.html#index-broken_002dreply_002dto-253 [4] https://groups.google.com/a/dimap.ufrn.br/d/msg/logica-l/C4CCsLSKywA/CVtVnxGgZTIJ -- Hermógenes Oliveira -- 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/20181127092750.Horde.1SjRO8xdN0BgRXBXooStTvS%40webmail.uni-tuebingen.de.
Re: [Logica-l] [META] Sobre uma questão técnica de configuração da lista
Para os colegas usuários do Gmail que porventura sofram de fadiga cognitiva e prefiram que suas pérolas de sabedoria tenham, por padrão, o maior alcance possível, seguem instruções do Gmail para alterar a sua configuração: https://support.google.com/mail/answer/6585?hl=pt-BR_topic=3395756 (Seção "Definir 'Responder a todos' como sua configuração padrão") Notem, contudo, que essa configuração afeta *todas* as mensagens, não somente as da Lógica-L. Eu, pessoalmente, prefiro a fadiga ao arrependimento. E me esforço bastante para que minhas bobagens não caiam no domínio público, embora nem sempre com sucesso (afinal, aqui estamos). Na minha opinião, eventualmente ter que reenviar para a lista uma mensagem erroneamente endereçada somente ao remetente é preferível do que eventualmente colocar no domínio público mensagens de conteúdo privado. -- Hermógenes Oliveira -- 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/20181127143152.Horde.czhrhDkdsBi43yOncBba_A0%40webmail.uni-tuebingen.de.
Re: [Logica-l] [fora do tópico] Europeus aumentam a pressão por OA
Creio que *ninguém* tenha entendido mal, mas para que não reste sombra de dúvida, talvez convenha deixar explícito que não há intenção de apontar o dedo para quem quer que seja. Eu mesmo, há alguns anos atrás, decidi que a melhor estratégia era dançar à toada do Qualis (e demais monstrengos classificatórios) na hora de considerar os veículos para minhas publicações, ao menos temporariamente, enquanto não consigo meu lugarzinho ao sol (presumindo a fortuna sorrirá para mim algum dia), ou enquanto o bom senso não contagia as políticas acadêmicas de avaliação. Nesse sentido, penso sim que cientistas estabelecidos carregam uma responsabilidade maior, se quisermos mesmo mudar o status quo. Dito isso, há diversas razões legítimas para um que um cientista, ainda que empenhado em melhorar a situação da acessibilidade, publique em (ou revise para) veículos de acesso restrito: área de especialização ou enquadramento da obra ainda não tem periódicos de qualidade publicados com acesso livre, coautoria (não é cortês empurrar sua agenda nos seus coautores), compromisso com coletâneas (também não é muito cortês empurrar sua agenda nos editores) etc. Enfim, em cada caso, diversos fatores estão potencialmente em jogo. Contudo, gosto de levantar o assunto sempre que tenho oportunidade, pois certamente há muita insatisfação, mas às vezes não agimos por receio de ficarmos isolados, ou de prejudicar nossas carreiras acadêmicas por uma causa perdida. Divulgar as pequenas conquistas e o grande apoio da comunidade acadêmica ajuda a manter o assunto vivo e a ganhar o impulso necessário para que possamos pender essa balança de vez. Ademais, não me parece que qualquer apoio que temos visto a essa causa, seja com pequenas medidas *voluntárias* (individuais ou coletivamente organizadas), seja com regras de agencias de fomento (no livre desempenho de suas funções), possam ser classificadas como "radicais". Radical é manter a própria comunidade científica refém em mesas de negociação por meses com demandas abusivas, e quando suas demandas finalmente não são atendidas, cancelar o acesso de cientistas aos frutos do seu próprio trabalho voluntário, em grande parte financiado por agências de fomento com dinheiro público (Elsevier vs Projeto DEAL na Alemanha). Surpreende que agências de fomento queiram dar um basta a isso? -- Hermógenes Oliveira "Tão certo é que a paisagem depende do ponto de vista, e que o melhor modo de apreciar o chicote é ter-lhe o cabo na mão." Machado de Assis -- 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/87k1np5d8b.fsf_-_%40camelot.oliveira.
[Logica-l] [fora do tópico] Europeus aumentam a pressão por OA
Olá, pessoal. Aqui estou, discutindo novamente meu assunto predileto fora do tópico da lista. Na Europa, aumenta cada vez mais a pressão de agências de fomento e centros de pesquisa por maior acessibilidade e menores custos para publicações científicas. https://www.sciencemag.org/news/2018/09/european-science-funders-ban-grantees-publishing-paywalled-journals Os argumentos das grandes editoras acadêmicas se tornam cada vez mais difíceis de sustentar em face da atual multitude de periódicos de livre acesso, alta qualidade e baixo custo de manutenção. As lamúrias sobre "inevitáveis e gigantescos custos de manutenção" e alegações sobre os "inestimáveis serviços" supostamente prestados por editoras comerciais estão mais do que desbancados. O único trunfo restante à editoras como Springer e Elsevier é o nome e suposto prestígio dos seus periódicos. A preocupação com acessibilidade, contudo, tem levado muitos cientistas a evitar periódicos de acesso pago. Perfeitamente cientes de que suas faturas não são pagas por indivíduos em busca de artigos avulsos, mas sim por agencias governamentais de fomento e bibliotecas públicas pelo mundo, essas editoras estão empenhadas em manter o fluxo de artigos e revisores para os seus periódicos. Estão mesmo dispostas a liberar o acesso, desde que *sob o seu controle*. https://www.springernature.com/gp/researchers/sharedit Artigos "compartilhados" por tais vias não podem ser redistribuídos e o compartilhamento e arquivamento fica sob controle absoluto da editora. O acesso ao artigo em si não está restrito, mas a distribuição sim. A diferença é que, nesse cenário, nossas agências de fomento permanecem compelidas a entregar somas milionárias para os que controlam o acesso. Imaginem esses milhões de dólares revertidos em bolsas de estudo e laboratórios de pesquisa em vez de pagamentos de lucros e dividendos aos acionistas... Se você publicou um artigo num periódico da Springer cujo período de embargo já espirou, não compartilhe SharedIt links, mas sim PDFs arquivados em repositórios institucionais. Para suas próximas publicações, considere periódicos de livre acesso (Philosopher's Imprint, Ergo, Logical Methods in Computer Science etc.). Seu chato de plantão, -- Hermógenes Oliveira »Wer sich nicht bewegt, spürt seine Fesseln nicht« Rosa Luxemburg -- 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/87worrrs57.fsf%40camelot.oliveira.
Re: [Logica-l] Kurt Gödel and the mechanization of mathematics
é a indecidibilidade de A. Consultando as definições relevantes em TMR, em particular a definição de "definível", constatamos que a nossa missão seria demonstrar um resultado existencial. E eis aqui, finalmente, a minha alegação: - Uma *demonstração* de que a função D de diagonalização é definível em A não pode dispensar de aritmetização. Em especial, essa alegação *não* pretende ser interpretada das seguintes formas: - Para se compreender o enunciado abstrato de TMR e sua dicotomia subjacente é necessário apelar à aritmetização. - A noção de "aritmetização", ou "representabilidade da matemática" é uma panaceia que remonta, pelo menos, aos tempos de Pitágoras. No próprio livro TMR, as demonstrações de indecidibilidade de teorias particulares, especialmente no teorema 9, §II, assumem explicitamente (nota de rodapé 7, §II) a recursividade da função D, e aqui se aplicam as minhas observações anteriores sobre as propostas alternativas nos moldes de Kleene. Em resumo, o enunciado abstrato de TMR nos fornece a dicotomia: ¬ D (diagonalização) ∨ ¬ T (teoremicidade) o que, para quem está familiarizado com a lógica proposicional clássica, é equivalente a D → ¬T Se o resultado pretendido é, para além da dicotomia abstrata de TMR, a indecidibilidade, isto é ¬T, de uma teoria particular A para a aritmética, então, temos ainda que demonstrar D. Ora, pelas definições em TMR, D é um enunciado existencial. Por isso eu falava de uma hipótese existencial embutida. > No que me concerne, foi me perguntado se eu poderia, porventura, > representar a diagonalização *na aritmética* sem usar > aritmetizacao. Pois bem, posso resolver o problema sem usar a > divisão em primos e compostos. Se eu usasse só a divisão entre pares > e ímpares estaria bom? Ou a dicotomia pares e ímpares ainda conta > como aritmetizacao? Está concedido que existem codificações distintas e, porventura, melhores do que aquelas utilizadas por Gödel e que, por sua vez, podem apelar para as mais variadas propriedades numéricas. Isso significa que qualquer codificação funciona para se aritmetizar a teoria, desde a noção de fórmula até a noção de derivação formal, e que basta mencionar números para que se tenha aritmetização? Não me parece razoável. Agora, nós poderíamos, eventualmente, fornecer critérios gerais (por exemplo, por meio de definições) que uma codificação precisa obedecer para desempenhar o papel pretendido na aritmetização. Isso não significa, porém, prescindir da aritmetização. Seria apenas o mesmo que dizer, em termos coloquiais: "Não enche o saco! Gödel já mostrou que dá pra fazer! Ninguém tem tempo ou interesse nessas continhas. Com exceção, talvez, dos hackers. Vá amolar um construtivista!" Referências: [1] https://groups.google.com/a/dimap.ufrn.br/d/msg/logica-l/3r3JuY79Ojc/r-G5sBKzBgAJ [2] https://groups.google.com/a/dimap.ufrn.br/d/msg/logica-l/dAbP6w2kx8w/VawkJgKnBwAJ -- Hermógenes Oliveira »Die Mathematiker sind eine Art Franzosen: Redet man zu ihnen, so übersetzen sie es in ihre Sprache, und dann ist es alsobald ganz etwas anderes.« Johann Wolfgang von Goethe -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/AM6P192MB0488AA9294E57CC3466CD1F7E9220%40AM6P192MB0488.EURP192.PROD.OUTLOOK.COM.
Re: [Logica-l] Kurt Gödel and the mechanization of mathematics
Olá, Chico. Eu não li a tese de doutorado do Smullyan ou o artigo de 1959, mas conheço o livro de 1992, Gödel's Incompleteness Theorems. De acordo com o prefácio, ideias daquelas obras anteriores estão incorporadas ali. Dentre a literatura secundária sobre os teoremas de Gödel, esse livro do Smullyan é o meu predileto. Me lembro de nós termos usado ele, juntamente com o artigo original do Gödel, num curso do mestrado na UFG em meados de 2011. Um dos cursos mais divertidos dos quais eu já participei! O livro apresenta codificações bem perspicazes que, na minha opinião, são melhores que as do artigo original. Contudo, ele não abre mão da aritmetização em momento algum, ainda que em alguns momentos a pressuponha *explicitamente* quando apresenta formulações abstratas do resultado gödeliano. -- Hermógenes Oliveira From: Francisco Miraglia Neto Sent: Sunday, 29 December 2019 12:47 Cc: Lista brasileira Subject: Re: [Logica-l] Kurt Gödel and the mechanization of mathematics > Car@s, > > Me indago porque ninguém parece se lembrar da tese de doutorado do Smulian em > Princeton, publicada naquela coleção de Princeton que tinha capa vermelha. > Para quem não conhece , recomendo: > A theory of formal systems > Princeton Univ Press, 1961. > > Há um artigo anterior de 1959, seu primeiro artigo, anterior à tese, em que > os argumentos de Godel são analisados e simplificados consideravelmente. > > De todo modo, o que chamamos de aritmetizacão , um caso particular de > internalização de uma Teoria no sentido que fala o Rodrigo, possui muitas > outras aplicações, como todo mundo sabe. O mesmo se aplica à ideia de > diagonalização, que trata-se, na minha opinião, de um método , uma ideia e > não apenas uma técnica particular. > > Um grande abraço a todas e todos e Feliz Ano Novo !! > > Chico Miraglia -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CE2D8CD8-A246-42D6-8622-47C714C61337%40ime.usp.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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/AM6P192MB04885FBB7208427DFED25A43E9240%40AM6P192MB0488.EURP192.PROD.OUTLOOK.COM.
Re: [Logica-l] Kurt Gödel and the mechanization of mathematics
Rodrigo Freire escreveu: > A hipótese que T tem nomes para suas fórmulas significa apenas que > as fórmulas de T e os termos fechados de T estão em correspondência > 1-1: a cada fórmula F corresponde um termo fechado ‘F’. Nem precisa > mencionar aritmética. Qualquer teoria em que o numero de fórmulas é > igual ao número de termos fechados satisfaz isso por definição. > Que T não representa simultaneamente sua diagonalização de fórmulas > (a operação que associa F(‘F’) à fórmula F) e sua teoremicidade é a > conclusão (em TMR), e também dispensa qualquer menção à > aritmética. Não é preciso qualquer menção, por exemplo, às funções > recursivas nesse teorema. Onde está a aritmetização como hipótese? Bem, Rodrigo, acho que podemos concordar que a questão em pauta não é a simples *menção* do termo "aritmetização", ou outro termo que o valha, mas se a técnica em si não é, de alguma maneira, pressuposta nas demonstrações alternativas que estamos discutindo. No caso da sua proposta específica, você pergunta: > Onde está a aritmetização como hipótese? Eu necessitaria de mais detalhes para fornecer uma resposta mais enfática, mas faço algumas indicações a seguir. Você propõe: > Se o numero de fórmulas de T é igual ao número de termos fechados de > T, e T é consistente, então T não representa simultaneamente a > operação de diagonalização nas suas fórmulas e a dedutibilidade em > T. Ora, consideremos uma teoria matemática fundamental, numa formulação qualquer, digamos, nos moldes do Principia Mathematica, como Gödel fez. Vamos avaliar a sua (in)decidibilidade com base no enunciado acima. Suponhamos que essa teoria é consistente. O critério de que o número de fórmulas seja igual ao número de termos fechados, claramente, não pode ser suficiente para a indecidibilidade (ex. Aritmética de Presburger). O outro critério seria que T "*representa* a operação de diagonalização nas suas fórmulas". O que significa isso? Seria possível avaliar esse critério para a nossa teoria sem apelar para a aritmetização? A minha aposta é que não. Imagino que você tenha em mente algo similar ao que consta no TMR, §II, Theorem 1. Ali, o resultado está enunciado em termos da noção de definibilidade (§II.2), onde, assim eu mantenho, estaria embutido o apelo à aritmetização. Inclusive, esse termo "definível" ("definierbar") é o mesmo usado por Gödel no artigo original. Porém, enquanto Gödel meticulosamente constrói as classes definitórias dos predicados e relações metamatemáticas por meio da aritmetização, TMR simplesmente substituem uma definição existencial, inserem como hipótese do enunciado e pronto! Típico matemático clássico! Sempre que há uma bela e elegante construção, substitui uma definição existencial e alega um resultado mais geral e abstrato. ;-) A questão é: Como seria possível demonstrar o existencial ali com respeito a função D de diagonalização para uma teoria particular, como o Principia Mathematica (e, assim, obter o resultado original de Gödel), sem usar aritmetização? -- Hermógenes Oliveira -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/AM6P192MB04885CB48E338A7815D3D03EE9240%40AM6P192MB0488.EURP192.PROD.OUTLOOK.COM.
Re: [Logica-l] Kurt Gödel and the mechanization of mathematics
> Hermógenes e lista, Olá, Carlos. > Eu , (pura teimosia?) continuo insistindo que a raiz do problema > está na definição recursiva que usam as linguagens formais, que > passam a ser, como Kleene disse, aritméticas. Bem, eu, particularmente, não vejo nenhum problema com isso. Você havia observado: > Se demonstrar que o conjunto das fórmulas que não são teoremas não é > recursivamente enumerável, então o conjunto dos teoremas não é > recursivo, E isso pode ser provado de maneira finitária. Certo? O problema em se abordar o resultado obtido por Gödel em termos da teoria das funções recursivas é que se perde de vista, ou simplesmente se pressupõe, a relação entre esses conceitos da teoria da recursividade e as teorias formais com aspirações fundacionistas. Hoje isso faz parte do repertório do lógico, e alguns poderiam mesmo tomar como óbvio ou evidente, porém, foi algo que Gödel precisou demonstrar! E, se parece tão natural agora, é porque ele o fez! Após o teorema demonstrado, fica fácil olhar para trás e formular enunciados equivalentes ao resultado original de Gödel os quais, ao menos superficialmente, não fazem uso dos conceitos e métodos encontrados no original. Observações semelhantes se aplicam à sua sugestão envolvendo modelos não-standard. Imagine que você voltasse no tempo, para 1928, e se encontrasse com Hilbert, ou Ackermann ou Bernays e dissesse a eles que o programa do Hilbert não pode triunfar porque "nem toda função recursiva parcial é potencialmente recursiva" (ou qualquer outro enunciado da teoria da recursão que o valha) e prosseguisse com as definições dos conceitos que ocorrem no enunciado e uma demonstração dele. Qual seria a reação deles? Ou, se viagem no tempo for ficção científica demais, imagine que você está *demonstrando* para seus alunos o resultado de Gödel e explicando seus efeitos sobre o programa de Hilbert. Você usaria modelos não-standard? Teoria da recursividade? Uma boa parte desses conceitos, como o de modelos não-standard, só fazem sentido hoje *por causa* do resultado de Gödel e, portanto, não podem prescindir dele ou substituí-lo. Por isso, me parece que algumas alternativas propostas nesta discussão pressupõe, ainda que implicitamente, o resultado original (ou uma parte importante dele). Nós podemos, eventualmente, nos contorcer com considerações informais baseadas no nosso já solidificado conhecimento de lógica, dizendo que é evidente a relação entre sistemas formais e recursividade, ou que é óbvio que qualquer teoria adequada da matemática permite diagonalização, ou coisas do gênero. Mas quando se trata de *demonstrar* essas alegações, fazer as continhas mesmo e mostrar o recibo, acho que é difícil escapar de algo semelhante ao trabalho meticuloso do original. Não lembro onde li isso, mas dizem que Gödel considerou o seu teorema a partir de algumas ideias bastante informais, de ordem semântica, envolvendo autorreferência. Mas ele sabia que esse tipo de argumento não convenceria os vovozinhos de Göttingen e sentou para elaborar uma demonstração completamente sintática. O esforço teria o custado uma temporada no sanatório. Mas, em troca, recebemos uma bela demonstração. -- Hermógenes Oliveira -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/AM6P192MB0488563805565FD4241C1922E9240%40AM6P192MB0488.EURP192.PROD.OUTLOOK.COM.
Re: [Logica-l] Kurt Gödel and the mechanization of mathematics
Rodrigo Freire escreveu: > Legal, vamos ver como o teorema de Godel na versão que mencionei > (TMR) *se aplica* nesse caso sem aritmetização no sentido usual > (sequer há um predicado para os números naturais). Ora, se a teoria é decidível, ninguém disputa que a aritmetização pode ser dispensada! Trata-se, porém, de dispensá-la em demonstrações de *indecidibilidade*! > [...] > > Agora a aritmetização: Entendo que esse termo está sendo usado para > um tipo de implementação da “representação formal da matemática” em > T. Há outros modos de fazer isso que não apelam para números. Acho > que essa é a “eliminação” da aritmetização que está em questão. É > claro que não se está propondo a eliminação da “representação formal > da matemática em T”. Se você identifica essas duas coisas, tudo > bem. Mas não acho razoável. “Representação” é muito mais geral que > “aritmetização”. Me parece claro que “aritmetização” é um tipo muito > particular e restrito de “representação” que remete ao uso de > operações aritméticas básicas com números apenas. Mas essa é uma > discussão sobre a identificação de dois termos indefinidos. Bem, então me parece que há uma maneira bastante direta de se resolver a questão. Considere o mencionado teorema 1 na seção II.2 do TMR. Tome uma formalização qualquer T, em primeira ordem, da aritmética. Você poderia, porventura, *demonstrar*, sem uso da aritmetização, que a função D é definível em T (sob a hipótese de que T é consistente)? Sinta-se a vontade para usar qualquer outro tipo de "representação formal da matemática" que não seja aritmética (que não apele a números), ou para, alternativamente, apenas indicar uma referência na literatura onde isto tenha sido realizado. -- Hermógenes Oliveira -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/AM6P192MB04882B62787FEBE43CCD1364E9270%40AM6P192MB0488.EURP192.PROD.OUTLOOK.COM.
Re: [Logica-l] Kurt Gödel and the mechanization of mathematics
Olá, pessoal. João Marcos escreveu: > Rodrigo, a sua resposta ajuda a corroborar a minha afirmação que a > demonstração do teorema de incompletabilidade gödeliano NÃO depende > da "aritmetização da sintaxe" (como defendeu a autora do artigo > citado no começo da presente discussão). Permitam-me assumir o ultrajante papel de advogado do diabo. :-) Rodrigo Freire escreveu (ênfase minha): > TMR apresenta a seguinte versão do teorema de Godel (citando de > memória, pode haver alguma variação inessencial) > *Se T tem nomes para suas fórmulas* (item 1 da codificação na minha > mensagem anterior) e é consistente, então T não representa > simultaneamente a operação de diagonalização nas suas fórmulas e a > dedutibilidade em T. Ora, é fácil se livrar da aritmetização se simplesmente a assumirmos como hipótese! O resultado de Kleene também foi aludido nesta discussão como evidência em favor da tese de João Marcos. Esse resultado, de fato, implica uma *versão* do resultado de Gödel que trata de teorias recursivamente axiomatizáveis nas quais *as funções recursivas primitivas são representáveis*[1]. Ora, para se chegar ao enunciado original de Gödel, é necessário ainda estabelecer que as funções recursivas primitivas são representáveis nas teorias fundacionais tipo Principia Mathematica. É precisamente isso que é alcançado por meio da aritmetização. Ainda que seja repertório básico para os lógicos de carreira contemporâneos, isso não é evidente. Inclusive, pode-se dizer que Gödel inaugurou com seu artigo os estudos do que hoje chamamos de funções recursivas primitivas. Se estamos pensando em demonstrações do enunciado original de Gödel, com todo seu impacto e consequências, então não creio que seja possível evitar a tal aritmetização (bem como diagonalização). Supostas demonstrações livres dela estão fadadas a pressupô-la de alguma maneira, seja explicitamente, ou embutida em definições. Certamente, como já foi observado nesta discussão, há uma certa vagueza em "demonstrações do resultado de incompletabilidade de Gödel". Não está perfeitamente claro quando um resultado deve contar como uma demonstração do enunciado gödeliano. Ademais, quando estamos discutindo o que é ou não necessário para se demonstrar um resultado, há que se considerar ainda uma certa ambiguidade na noção de demonstração. Afinal, há boas e más demonstrações. Qual o valor de se evitar esta ou aquela técnica se o preço é terminarmos com uma má demonstração? Assim como qualquer resultado, as demonstrações do teorema da indecidibilidade do Gödel podem ser inseridas num espectro com relação a sua perspicácia e poder elucidatório. Num dos extremos está algo como a demostração do próprio Gödel (talvez com algumas melhorias inessenciais na codificação) e no outro extremo está aquela em que simplesmente se assume o enunciado do teorema como hipótese. Afinal, o resultado é conhecido como teorema de Gödel e não teorema de Finsler[2]. E, a julgar pela escassa correspondência entre os dois[3], os detalhes técnicos, inclusive aritmetização, são uma importante razão para essa nomenclatura. Portanto, não diria que seja matéria apenas para hackers[3]. Notas: [1] Em conversa privada, João Marcos indicou a excelente nota de Peter Smith sobre o assunto: https://www.logicmatters.net/resources/pdfs/KleeneProof.pdf [2] Paul Finsler. Formale Beweise und die Entsheidbarkeit. Mathematische Zeitschrift, Band 25, 1926, S. 676-682. [3] Kurt Gödel. Collected Works, Volume IV, p. 405-415. [3] A codificação particular escolhida por Gödel é, de fato, inessencial, como observou o próprio Gödel, e pode ser substituída, eventualmente por versões melhores, sem qualquer prejuízo. Porém, a aritmetização em si me parece desempenhar um papel central. -- Hermógenes Oliveira "The competent programmer is fully aware of the strictly limited size of his own skull; therefore he approaches the programming task in full humility, and among other things he avoids clever tricks like the plague." Edsger W. Dijkstra -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/AM6P192MB0488F538837579BDB703E438E9250%40AM6P192MB0488.EURP192.PROD.OUTLOOK.COM.
Re: [Logica-l] [discussão sobre Lógica e inclusão] uma rosa com um novo nome?
ra aspirantes a comediantes. Sinceramente. Algém quer fazer piada, mas não tem qualquer talento humorístico e está desesperado(a) por piadas de graça? Pois que se vire! Trata-se de algo frívolo demais para ser objeto de consideração, dada a pauta em discussão. > E - Vários membros e ex-alunos do grupo afirmam ter muito orgulho do nome > do grupo, e chegam a se autodenominar "loliteiros" ou "loliteiras" ("para > sempre", ou "até a morte"). > > F - Continuando o ponto anterior, temos ex-alunos que tatuaram "LoLITA" no > corpo, que afirmam que "não há nenhum tipo de malícia no nome" ou > "intenções escusas ao criá-lo", que defenderam a tese usando sapatos que > faziam referência ao logotipo do grupo (ver abaixo), etc. Ainda, a maior > parte das ex-alunAs e das colaboradorAs do grupo que se manifestaram no > nosso fórum interno de discussões afirmaram estar plenamente confortáveis > com o nome do grupo. OK. Não tenho experiência com o grupo, mas gostaria de levantar a hipótese de que o orgulho não advém tanto do *nome* do grupo, mas do *próprio grupo* (das atividades que desenvolve, daquilo que o grupo representa). Sim, imagino que possa haver quem ache o nome legal, mas suspeito que não se sentiriam tão diferentes caso o grupo tivesse um outro nome, digamos tão astuto quanto e com duplo significado, mas que não estivesse associado com a exploração e/ou erotização de meninas púberes? Interessante saber que a maior parte das alunas e colaboradoras se sentem confortáveis com o nome do grupo. E a menor parte? A maior parte também se sentiria confortável com um outros nomes, suponho? Talvez alguns com os quais a menor parte também esteja confortável? Convém notar que a suposição considerada em pauta é de que o nome teria o *potencial* de afastar. Difícil sondar a opinião das pessoas que, caso o suposto potencial tenha se efetivado no passado, escolheram se afastar. Também é difícil auferir em que proporção esse potencial se efetivou, se é que isso ocorreu. Contudo, qualquer resquício de chance nesse sentido me parece bastante pesado em comparação com piadas, estampas de sapatos, ou defasagem de tatuagens, ainda que combinados. > G - Qualquer nome pode dar lugar a "interpretações distorcidas". Correto. Mas inócuo. > H - A *referência* última do nome "LoLITA", por nexo de batismo, é > simplesmente o grupo de pesquisa correspondente, do DIMAp/UFRN, e não o > romance do Nabokov, nem o apelido carinhoso de uma mulher chamada Dolores, > nem nenhum dos outros itens extra-linguísticos apontados nos outros itens > acima (ou abaixo). Correto. Mas irrelevante. Um pouco mais detalhadamente sobre os pontos G e H (e talvez partes do ponto F). Creio que ninguém esteja sob a hipótese de que o fato de que a sigla do grupo soletra "Lolita" é um infeliz acidente. Isto é, a sigla LoLITA é proposital. Bem, mas trata-se de um grupo de lógica. Não de literatura. Nem de fãs do Nabokov. Ou de pedófilos na internet. A pergunta natural é: Bem, por que logo "LoLITA"? Ao que tudo indica, a resposta, no contexto do batismo do grupo, é completamente inocente: a sigla se encaixa bem com uma boa descrição, é o nome de uma obra literária famosa, é bem astuta e etc. Agora, se pessoas começam a levantar preocupações com possíveis efeitos negativos do nome (que supostamente passaram despercebidos), a posição "o nome permanece" já não é tão inocente. Não se trata aqui de atribuir malícia, ou qualquer outra motivação nefasta ao contexto de batismo. Quem defende que o nome deve permanecer me parece estar comprometido(a) com alguma combinação das seguintes teses: - Nenhuma pessoa razoável associa conotações negativas ou impróprias à expressão "lolita" (embora seja banida em várias ferramentas de busca por aí) a ponto de afetar o seu envolvimento com o grupo de pesquisa em qualquer capacidade (uma tese temerária, eu diria) - os possíveis efeitos negativos são desfavoravelmente contrabalanceados pelos benefícios em termos de piadas, sapatos, tatuagens e evitar o considerável trabalho envolvido em mudar o nome do grupo - o legado do grupo de pesquisa está de alguma forma atrelado à *permanência* do nome. proteger esse legado, de alguma maneira, tem mais valor do que garantir o conforto e/ou acolhimento de futuros membros e/ou colaboradores Meus centavinhos, -- Hermógenes Oliveira -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/4392895.f77xMH5Q12%40avalon.
Re: [Logica-l] [discussão sobre Lógica e inclusão] uma rosa com um novo nome?
Na segunda-feira, 21 de junho de 2021, às 12:40:15 -03, Marcelo Finger escreveu: > No centro de IA (C4AI) da USP-IBM-Fapesp, estamos construindo 3 Córpus: > - Córpus Carolina (em homenagem à Carolina Michaelis de Vasconcelos) > - Córpus Portinari (em homenagem a Cândido Portinari) > - Córpus Coraa (em homenagem à Cora Coralina) Confesso que, a despeito de muito esforço, não consegui capturar o motivo desse informe no contexto desta discussão. > Pessoalmente, não acho que as objeções ao nome do seu grupo tenham > fundamento, não vejo como admitir a crítica "não adequado para um grupo de > pesquisa vinculado a uma universidade; é anti-profissional; é de mau > gosto". > > O estilo Tango era considerado vulgar e de mau gosto. Idem para o samba. > Idem para o Jazz. Já foi o tempo, sei lá por quê, que mulheres grávidas > não podiam aparecer na TV. O futebol feminino já foi ilegal no Brail. E > por aí vai. A analogia aqui seria que a exploração e/ou erotização de meninas é censurável hoje, mas eventualmente poderá ser considerada totalmente normal no futuro?! > Eu acho Lolita simpático e consagrado. Não me parece que esta seja a pauta da discussão. Não se trata de uma enquete: quem gosta do nome, quem não gosta do nome. Me parece perfeitamente concebível que alguém goste do nome (digamos, porque é um(a) fã de Nabokov), mas que discorde que seja apropriado usá-lo para um grupo de lógica. Recapitulando, a pauta, juntamente com uma possível argumentação para mudança do nome, pelo que eu entendi, seria: - Existem conotações negativas associadas ao termo "lolita". - Isso pode gerar constrangimentos (mesmo para pessoas que não associam, elas mesmas, nada de negativo com o termo, por exempĺo, ao lidar com outras pessoas) e, consequentemente, afugentar e/ou intimidar pessoas de se associar com o grupo em alguma capacidade - Ora, mas as razões para a escolha do nome "lolita" são completamente ortogonais à missão e à área de trabalho do grupo: lógica. - Deveríamos mudar o nome, pois assim evitamos possíveis associações negativas. A mudança do nome não traz nenhum empecilho ou efeito negativo ao propósito e aos trabalhos do grupo de pesquisa, que, repito, é a *lógica* Em resumo, não se trata de uma questão de pudor ou gosto. Nesse sentido, concordo que o ponto citado por JM que menciona "mau gosto" não é muito convincente, pelo menos da forma como está formulado, embora eu consiga vislumbrar um ponto subjacente que possa ser pertinente. Enfim, não vejo a mudança do nome como uma pauta moral. Ninguém estaria sendo proibido de ler Nabokov, gostar de Nabokov, dançar o tango, o Jazz e o ChaCha, fazer piada usando o termo "lolita" na mesa de buteco com os amigos, e seja lá mais o que as pessoas acham que essa discussão seja a respeito). -- Hermógenes Oliveira -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/5077691.WgdXaEvCEn%40avalon.
Re: [Logica-l] Para Todxs: Natal - Procuram-se coautoras e coautores
Olá, Daniel. Muito legal o projeto! Há algum tempo atrás, eu escrevi para sondar sobre o projeto e, na ocasião, você me enviou as fontes LaTeX da tradução feita pelo grupo de Natal. Eu e Diego estamos usando o texto como livro didático das disciplinas de lógica aqui em João Pessoa. Para coordenar as nossas revisões do texto, Diego incluiu as fontes no GitHub sob a licença que acompanhava as fontes que você me forneceu, isto é CC-BY-4.0 (a mesma do projeto original): https://github.com/diegofernandess/paratodxs-rn-pb Nós fizemos algumas alterações e correções que estão espalhadas em quatro bifurcações ("branches"). Tentamos, na medida do possível, granularizar ao máximo nossas alterações em remendos ("commits") separados, adicionando comentários explicativos ou motivadores, sempre que possível (alguns, inclusive, contém discussões e divergências entre eu e Diego). A ideia é encorajar colaborações e permitir pinçar ("cherry pick") mudanças localizadas, facilitando a incorporação em versões paralelas (por quem quer que seja). Provavelmente, algumas de nossas correções não são mais aplicáveis, pois estão baseadas numa versão mais antiga do texto. Porém, talvez algumas delas ainda sejam de interesse. Noto que a versão atual contém capítulos sobre lógica modal e metateoria. Eu havia começado a trabalhar no capítulo sobre lógica modal, mas infelizmente não pude avançar muito. Talvez convenha centralizarmos os esforços. Daí nós manteriamos um tronco separado do repositório de vocês. Isso facilitaria a troca de remendos entre as diversas versões. Cordialmente, -- Hermógenes Oliveira -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/1664059.lhQJIO16El%40avalon.
Re: [Logica-l] [off] Licença maternidade no lattes
Na sexta-feira, 9 de abril de 2021, às 18:02:50 -03, Jaison Schinaider escreveu: > Acredito que essa informação seja de interesse de alguns membros do grupo: > > https://linkdigital.ifsc.edu.br/2021/04/08/cnpq-anuncia-inclusao-do-campo-li > cenca-maternidade-no-curriculo-lattes/ Bem, antes tarde do que nunca, eu suponho. O próximo passo agora é adaptar todas as resoluções, regimentos, pareces técnicos e demais normas que regem seleções, promoções, progreções, e demais processos relevantes no âmbito acadêmico, para que levem em conta esse novo campo. Uma longa jornada. Ideias sobre os detalhes de como isso poderia funcionar na prática podem ser talvez obtidos junto à organizações acadêmicas que já incorporam algo assim há algum tempo. A DFG, para citar apenas um exemplo, possui diretrizes[1] nesse sentido para pareceristas em processos seletivos: "There is no room for non-scientific criteria in the review process. However, appropriate consideration can and should be given to personal factors affecting an applicant. For example, appropriate allowance should be made for longer qualification phases, publication gaps or reduced periods abroad, which are often due to childcare or caring for a family member." [1] https://www.dfg.de/en/research_funding/principles_dfg_funding/ equal_opportunities/reviewers/index.html -- Hermógenes Oliveira -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/2307838.OfsEH2KBJ2%40avalon.
Re: [Logica-l] Vácuo
No domingo, 11 de abril de 2021, às 17:45:16 -03, Joao Marcos escreveu: > [...] > > Meu raciocínio: > Se houvesse uma "Aritmética Relevante", estendendo [A4], que tivesse > algo relevante (perdão) a dizer sobre [A1], sem ao mesmo tempo se > comprometer com [A2] (como Daniel parece desejar), talvez ela > consistisse em uma resolução satisfatória para o mistério de [A3]? Core Logic? https://sci-hub.se/10.1007/bf00763511 > Claro, esta seria a solução _mais simples_. Outra explanação para o > funcionamento da semântica "folk", que vai contra o bom senso _dos > lógicos_, também poderia ser satisfatória. Uma Aritmética sempre será > necessária, de uma maneira ou de outra, para dar conta de [A1]. Quais lógicos são esses, cujo bom senso está sendo invocado aqui? Lógicos clássicos, eu suponho? Não me parece que a relevância seja um problema para a aritmética em si. Ao menos, não me recordo de inferências patentemente irrelevantes em teoria dos números, com a qual tenho certa familiaridade, mas, reconhecidamente, não sou um especialista. Ficaria agradavelmente surpreso se alguém fornecesse um exemplo. A irrelevância do condicional clássico oferece alguns ganhos técnicos no âmbito dos programas de fundamentação que pairavam por volta do início do século XX, mas não parece ser um elemento essencial da argumentação matemática informal. Porém, ainda que o fosse, não me parece correto impor um artefato da tradição matemática, especialmente como conteúdo obrigatório em cursos de filosofia, nos quais, inclusive, é comumente apresentado como regra do raciocinar correto, dentre outras baboseiras. -- Hermógenes Oliveira -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/3581293.RALIiNX56z%40avalon.
Re: [Logica-l] Vácuo
Em segunda-feira, 12 de abril de 2021, às 11:53:36 -03, Joao Marcos escreveu: > > > > Quais lógicos são esses, cujo bom senso está sendo invocado aqui? Lógicos > > clássicos, eu suponho? > > Os lemas que eu invoquei eram intuicionisticamente válidos, certo? OK. O bom senso dos lógicos clássicos e intuicionistas, então. Ambos endossam lógicas não relevantes. E os lógicos relevantes? Não são lógicos? São anátemas? Blásfemos? > > Porém, ainda que o fosse, não me parece correto impor um artefato da > > tradição matemática, especialmente como conteúdo obrigatório em cursos de > > filosofia, nos quais, inclusive, é comumente apresentado como regra do > > raciocinar correto, dentre outras baboseiras. > > Ainda gostaria de ver uma interpretação formal (de qualquer tipo) que > justificasse a alegada inequivalência entre (A) e (B). Assumindo que se trata de um desejo sincero da sua parte, trata-se de uma simples aplicação da lógica intuicionista *relevante*, cujos detalhes formais estão disponíveis no artigo que mencionei antes. Na verdade, a apresentação aqui está mais robusta, ainda que o título não seja tão chamativo quanto: https://sci-hub.se/10.1017/s1755020311000360 Divirta-se! -- Hermógenes Oliveira -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/2426189.3kHWx39YlV%40avalon.
Re: [Logica-l] Concurso Público (FIL-UnB) - Área: Lógica
João Marcos escreveu: > De resto, considero válido, sim, discutir OUTROS argumentos > importantes apresentados aqui, envolvendo a formação pedagógica, a > escolha cuidadosa dos temas a serem cobrados no concurso, a escolha > cuidadosa da banca e a implementação de políticas públicas > afirmativas, dentre outros. Proponho focar a questão por uma perspectiva prática. Poderíamos discutir qual seria o formato ideal para contratações no magistério superior federal, mas, na realidade, já existem regras gerais sobre o formato dos concursos a nível nacional e, eventualmente, regras mais específicas também a nível da instituição. Sobre esta perspectiva prática, a primeira coisa a se observar é que a preocupação primordial em contratações para o magistério superior é o interesse público, conforme emanado da finalidade e missão da autarquia. Não se trata de uma questão de distribuição equitativa de cabides de emprego de acordo com o mérito de indivíduos, não importa qual métrica seja adotada para o mérito (na minha humilde opinião, "meritocracia" é um conceito que já nasceu falido, mas, enfim, tentarei me manter no tópico[1]). O perfil mais alinhado com a missão pública atrelada ao departamento pode variar de acordo com a situação do mesmo, não obstante o mérito percebido em favor deste ou daquele candidato, ainda que a ideia de mérito empregada aqui esteja diretamente relacionada com a área de conhecimento do concurso. Por exemplo, numa certa IES, os programas de pós-graduação na área podem ser mais ou menos desenvolvidos. Portanto, a expectativa de atuação do(a) contratado(a) na graduação em filosofia pode ser maior ou menor. Em certas IESs, a lógica está presente na grade de vários cursos de graduação. Em outras, a lógica, como componente curricular ministrada pelo departamento de filosofia, está presente apenas no curso de filosofia. De acordo com a situação, o contratado terá a expectativa de lecionar exclusivamente lógica ou, eventualmente, outras temáticas afins para o curso de filosofia, ainda que predominantemente focado na lógica. Enfim, existem diversos fatores inerentes ao contexto específico da IES e/ou departamento que justifiquem a preferência pela contratação de professor especialista em lógica, porém com formação razoavelmente ampla e sólida em filosofia. Isto do ponto de vista do interesse público. Agora, dados os parâmetros legais para contratação, qual seria a maneira de tentar aumentar a probabilidade de contratação de um profissional com o perfil mais alinhado? Garantias cabais não podem ser obtidas, e creio que isto seja pacífico. Uma sugestão apresentada foi incluir pontos filosóficos nas temáticas do concurso. Os pontos são sorteados, contudo. O que significa que a averiguação de competência em temas filosóficos ficaria ao sabor da sorte. Por outro lado, se todos temas são filosóficos, não se averigua competência em tópicos avançados de lógica. Existem várias outras opções de incluir a averiguação de ampla competência filosófica dentro das etapas do concurso. Por exemplo, seria concebível incluir na prova de títulos uma pontuação generosa para quem já tem experiência docente em filosofia (embora suponho que isto não agradaria nem a gregos nem a troianos, e também esbarra no fato deste tipo de pontuação normalmente já estar determinada a nível da IES). Poderia também ser o caso de calibrar o sorteio dos pontos, introduzir algumas novidades na prova didática, e por aí vai. Contudo, quem já participou de bancas de concurso sabe que estas medidas são convites irresistíveis a recursos e toda sorte de imbróglios jurídicos. Exigir graduação em filosofia, por outro lado, é uma maneira mais segura, ainda que falível, de aumentar a probabilidade de contratação de uma pessoa com ampla formação em filosofia e, concomitantemente, competente em temas avançados de lógica. É uma garantia? Não, obviamente. É razoável exigir alguma garantia neste processo? Não creio. É um processo justo, do ponto de vista de quem supostamente "merece" uma posição no serviço público pela sua dedicação e conquistas acadêmicas na área? Também não creio. Pode ser razoavelmente justificada do ponto de vista do interesse público? Possivelmente sim. Agora, quanto ao edital do concurso em tela, não consigo sequer especular quais motivações levaram à exigência de diploma de graduação em filosofia. Se tivesse que adivinhar, diria que sequer refletiram tanto sobre a questão quanto nós aqui na lista e simplesmente fizeram o conhecido copia-cola-e-ajusta do último edital lançado. Cordialmente, [1] Para quem se interessa pelo tópico, recomendo a coletânea "Meritocracy and Economic Inequality" editada por Kenneth Arrow etal. como aperitivo inicial. -- Hermógenes Oliveira -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica --- Você está recebendo esta mensagem porque se inscreveu no grupo &q
Re: [Logica-l] Fwd: [CAROL / UFRN] Fwd: [CHAMADA] - Edição Especial revista Axioms
Em segunda-feira, 27 de março de 2023 às 21:59:20 UTC-3, Walter Carnielli escreveu: Então Hermógenes, considerando os elevados custos da compra de assinaturas pelo cofres públicos, e considerando a tendência de pagar para publicar que está pressionando aqueles que produzem ciência, o que devemos fazer? Pagar dos dois lados? Pois é, Walter. Acho que um primeiro passo importante é levantar a pauta, como você fez, e trocar ideias e argumentos entre os colegas para que o assunto ganhe mais visibilidade e, quem sabe, suscite ações mais coordenadas (é um problema difícil de solucionar no âmbito meramente individual). Como escrevi, não tenho uma solução universal a sugerir. Mas vou compartilhar algumas considerações, as quais, contudo, são bastante peculiares à minha situação e certamente não se aplicam a vários outros contextos. Primeiro, algumas observações, que me parecem incontestáveis: 1. O serviço de editoração de casas de publicação científica é ruim, e parece estar piorando com o passar do tempo (escrevi sobre isto na lista antes <https://groups.google.com/a/dimap.ufrn.br/g/logica-l/c/D5hMtl4KedY/m/Jug-fvxaBQAJ>). Uma boa parte do serviço é terceirizado a trabalhadores sobrecarregados em países em desenvolvimento. 2. Publicação científica tem custos, sim. Hospedagem, indexação, arquivo permanente, DOI, software de gerenciamento do fluxo de submissão etc. Nada disto é gratuito. Contudo, como Valéria tem apontado, existem diversos exemplos que demonstram que este custo é bem menor do que muitas casas de publicação alegam, especialmente quando não é necessário bancar o lucro de proprietários. No âmbito da filosofia, se destacam Philosopher's Imprint <https://journals.publishing.umich.edu/phimp/> e Ergo <https://journals.publishing.umich.edu/ergo/> (ambas gerenciadas pela Michigan Publishing). A qualidade do serviço (tanto para leitores quanto autores) deixa grande parte das grandes casas editoriais no chinelo. Em comparação, o custo é irrisório. Então, com base nisto e outras observações já aludidas na discussão, uma estratégia bastante natural seria apoiar veículos com modelo de acesso livre genuíno e, em caso de insuficiência destes em alguma especialidade, buscar fundar novos. As condições para desempenhar estas ações variam bastante de indivíduo para indivíduo, de área de especialidade para área de especialidade, de contexto para contexto. Portanto, vou focar agora no meu caso. Eu atuo como parecerista para periódicos de grandes editoras. Minha racionalização/desculpa esfarrapada: a minha área de especialização é relativamente pequena e praticamente todos os textos são submetidos e/ou publicados num certo punhado de periódicos de grandes editoras, pelo simples fato de especialistas fazerem parte do corpo editorial destes periódicos. Novos pesquisadores na área comumente reclamam de submissões apodrecendo no "journal hell", em boa parte por dificuldade de arranjar pareceristas ou, ao menos, de conseguir pareceres em tempo hábil. Isto afugenta a moçada, a qual, sob pressão para publicar, eventualmente decide dedicar-se a outra especialidade, contribuindo assim para o arrefecimento ainda maior da minha área. Portanto, no balanço das coisas, me parece menos danoso tolerar o status quo, ao menos enquanto não conseguimos pouco a pouco diversificar para outros veículos. Quanto à publicação, a minha intenção é submeter meus melhores artigos daqui em diante em periódicos mais decentes, ainda que menos prestigiosos. Sim, o Qualis provavelmente irá me penalizar por isto, pode ser difícil encontrar pareceristas e etc. Mas acho que, sem um pouco de sacrifício, é difícil conseguir impulso para sairmos desta encruzilhada. Contudo, não me parece correto impor esta minha decisão a coautores em caso de artigos conjuntos. Nestes casos, vou com a sugestão dos meus colaboradores e o que seria melhor para suas respectivas carreiras. *Se eu fosse influente na minha área*, e capaz de aglutinar pesquisadores, eu fundaria um novo veículo de livre acesso com um bom corpo editorial, ou convenceria meus pares a abandonar suas funções nos corpos editoriais das grandes casas e se juntar a mim no corpo editorial de outros periódicos mais decentes. Tenho certeza que as submissões e, consequentemente, os artigos publicados iriam nos acompanhar. Até eu chegar lá, vou vivendo entre frustrações, planos e racionalizações. Cordialmente, -- Hermógenes Oliveira -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica --- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/e0f1b6d6-b4d0-4f73-8d2e-c6c7ac36b1a5n%40dimap.ufrn.br.
Re: [Logica-l] Fwd: [CAROL / UFRN] Fwd: [CHAMADA] - Edição Especial revista Axioms
Prezad@s, João Marcos traz um ponto importante, sobre o qual já discorri antes na lista <https://groups.google.com/a/dimap.ufrn.br/g/logica-l/c/hdgs_PeUEyo/m/cbY8DMUeBAAJ>. Não convém ignorar que contribuir com periódicos de propriedade das grandes editoras científicas também prejudica a causa da ciência e pesquisa livre. Sim, sob a condição de ceder os direitos autorais, *autores* comumente não pagam para *publicar*. Mas, neste caso, os *cofres públicos* normalmente pagam pelo *acesso*, e as respectivas editoras também embolsam lucros obscenos. Eis um experimento para quem curte ficar deprimido ou indignado. Abra a página do Diário Oficial da União e faça uma busca na Seção 3 pelo termo "Elsevier", "Springer", "Clarivate Analytics" etc. Faça uma breve soma dos contratos dos três últimos anos e relembre a magreza dos recursos para pesquisa no mesmo período. Eles também assinam contratos diretamente com as IES, claro. A minha instituição, a UFPB, por exemplo, pagou algumas centenas de milhares de reais <https://sipac.ufpb.br/public/jsp/processos/processo_detalhado.jsf?id=1849298> para obter acesso aos dados bibliométricos da Clarivate e Scival. O contrato tem sido renovado periodicamente. A justificativa supostamente seria a "necessidade de uma ferramenta para avaliação da produção da universidade com base em dados e evidência". Os demais detalhes da justificativa é copiado e colado da própria brochura do fornecedor. É possível argumentar <https://www.scidev.net/global/features/open-access-excludes-developing-world-scientists/> que *pagar para publicar* afeta mais negativamente a pesquisa em países emergentes do que *pagar para ler* (não quero entrar nas instrumentalizações destes argumentos pelas grandes editoras para se pintarem como defensoras dos fracos e oprimidos). Contudo, somos leitores de ciência também. Não é improvável que uma boa parte de nós vá direto ao Sci-Hub e sequer se importe com o portal de periódicos da CAPES. Ainda que não façamos tanto uso atualmente, os cofres públicos continuam pagando. E não é factível que o Governo Brasileiro simplesmente deixe de pagar sob a alegação que quase 100% de nós já usamos Sci-Hub mesmo. Me parece que os custos aos cofres públicos devem ser devidamente considerados, ainda que seu efeito em pesquisadores individuais seja mais diluto. Não tenho soluções a sugerir. Trata-se de um problema melindroso. Mas acho importante evitar que a perspectiva do pesquisador individual domine, e que os custos para a sociedade sejam devidamente considerados. Cordialmente, -- Hermógenes Oliveira -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica --- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/07cb74bc-9854-4779-9f7c-aadadaf824ebn%40dimap.ufrn.br.
Re: [Logica-l] Trends in Logic conference- Torun, 2023
Salve, Valéria, e demais. Bem, a memória do ser humano é falha, como sabemos, mas talvez convenha compartilhar mais algumas recordações da conversa, pois foi muito instrutiva para mim à época. O grupo vinha organizando "MANELS" mais por omissão ou acidente do que por convicção. Com as reclamações em 2015, ficou meio que acordado que este fator seria considerado de modo mais contundente na organização de eventos posteriores. Entretanto, **não** foi colocado um embargo em "MANELS", embora evitar "MANELS" tenha sido promovido para um dos fatores de maior peso. Minha única contribuição para a conversa, pelo que me recordo, foi compartilhar o relato de uma jovem pesquisadora de destaque, com a qual esbarrei num evento de lógica, quem lamentava estar sendo inundada por convites. Como ela considerava a causa justa, sentia-se pressionada a aceitar os convites, porém já estava ficando "farta de eventos e conferências" e sentia-se meio que usada como espécie de trunfo anti-MANEL. É costumeiro julgar um evento, principalmente na fase inicial de organização, por meio da notoriedade do painel de palestrantes convidados. Junte-se a escassez de mulheres na área com outros fatores como conflitos de agenda, falta de entusiasmo por viagens transoceânicas e etc, e a tarefa de se evitar um "MANEL" pode se tornar bastante melindrosa. De fato, foi mencionado que alguns dos "MANELS" organizados anteriormente foram acidentais, isto é, mulheres foram inicialmente convidadas (não como medida consciente de evitar um "MANEL"), mas recusaram por razões diversas. Por estas e outras razões, fixou-se o entendimento de que se evitar "MANELS" a todo e qualquer custo, não seria proveitoso. Por exemplo, numa suposta situação logística desesperadora, esgotadas as opções razoáveis, não seria propício (e talvez fosse mesmo ofensivo) estender convites a pessoas apenas longinquamente relacionadas com a temática do evento, de modo que ficasse patente que a pessoa estava sendo convidada *única e exclusivamente* por causa do seu gênero. Felizmente, parece que este tipo de situação hipotética se mostrou bem menos factível do que se antecipava. Enfim, as reclamações em 2015, além de não gerarem qualquer desconforto (pelo que me recordo), suscitaram mudanças positivas. Portanto, creio que ainda pode valer a pena reclamar, sim. Também acho razoável, contudo, adotar cautela ao atrelar malícia, ou um posicionamento consciente sobre o desequilíbrio de gênero na área, com base **apenas** na organização de um evento com "MANEL". Claro, independente das razões por traz do "MANEL", seja por fatores incontornáveis de logística organizativa ou simples obtusidade, reclamar é sempre legítimo e, eu diria, necessário. Cordialmente, -- Hermógenes Oliveira -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica --- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/695ab370-406b-4b2f-b2c1-5e74712dd401n%40dimap.ufrn.br.
Re: [Logica-l] Trends in Logic conference- Torun,2023
Olá, pessoal. Eu simpatizo com a frustração e o cansaço, mas concordo com Elaine que convém continuar reclamando. Me lembro que, há não muito tempo atrás, após reclamações <https://feministphilosophers.wordpress.com/gendered-conference-campaign/#comment-139251>, houve uma conversa interna e o grupo em Tübingen passou a considerar a questão nos eventos que organizou dali em diante. Cordialmente, -- Hermógenes Oliveira -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica --- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/35fc81c8-3a12-4252-af6b-227117d79c3dn%40dimap.ufrn.br.
[Logica-l] Peter Schroeder-Heister on Proof-Theoretic Semantics
Acesso livre: https://link.springer.com/book/10.1007/978-3-031-50981-0 -- Hermógenes Oliveira -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica --- 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 acessar esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/f3034b17-197f-49f3-abb8-e1400472aaf1n%40dimap.ufrn.br.
Re: [Logica-l] Códigos de ética e conduta em sociedades científicas
Prezadas(os), Sobre esta temática, acho que sanções são absolutamente indispensáveis. Denunciantes precisam ter total transparência sobre os procedimentos para tratamentos das denúncias, a expectativa de serem levadas(os) à sério e protegidas(os) de eventuais retaliações, e que suas denúncias, caso contundentes, conduzam a reais consequências. Caso contrário, ninguém se prestará a denunciar qualquer coisa. -- Hermógenes Oliveira -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica --- 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 acessar esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/2049fcd3-c2dc-44d4-8be9-e89af90f45b6n%40dimap.ufrn.br.
Re: [Logica-l] Caso de vira-latismo e misoginia no CNPq- será o primeiro????
Olá, pessoal. Em sábado, 6 de janeiro de 2024 às 21:12:12 UTC-3, Joao Marcos escreveu: Está de parabéns o CNPq pela justa e expedita reação! (mesmo que ainda não tenha ficado inteiramente claro, do que está escrito na nota do CNPq, quem seriam os beneficiados pelo "parto ou adoção", e como isto seria computado na prática) Diferente de alguns países onde o próprio arcabouço legal, especialmente o trabalhista, permitem uma participação mais equitativa no cuidado da prole (na Alemanha, a duração da licença pode mesmo aumentar caso haja participação do pai), no Brasil as coisas infelizmente ainda funcionam sob o pressuposto de que o cuidado das crianças é responsabilidade da mãe. No caso da Alemanha, que conheço mais de perto, as semanas de licença para cuidado da criança retiradas pelo pai possuem o mesmo peso daquelas retiradas pela mãe frente a agências de fomento, como a DFG. Dado o contexto brasileiro, as medidas anunciadas pelo CNPq provavelmente afetarão apenas as mães (ou talvez também pais com guarda exclusiva). Acho que parte da tarefa de tornar o ambiente trabalhista brasileiro (não só o acadêmico) um pouco mais adequado para pessoas com filhos passa por uma reorientação das políticas públicas ao contexto familiar atual, onde pais participam ou desejam participar de maneira equitativa no cuidado dos filhos e famílias nas quais o cuidado das crianças é exercido por casais homossexuais, para citar apenas alguns exemplos. No caso da DFG, a agência pode contar com o contexto alemão para averiguar, digamos, que o pai está efetivamente com o cuidado da criança, uma vez que este está de licença enquanto a mãe trabalha, digamos. O contexto brasileiro é bem distinto. Afinal, a situação de um novo pai com uma rede de suporte local, uma esposa, uma babá e um escritório com isolamento acústico dentro de casa é muitíssimo diferente daquela de uma mãe solteira sem família num raio de mil quilômetros e que more num cafofo de 50 m². Sabemos que temos colegas na universidade em ambos estes extremos, bem como em diversos outros pontos no espectro. -- Hermógenes Oliveira -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica --- 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 acessar esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/d0ecd389-907f-4705-aa47-38bf78f7b630n%40dimap.ufrn.br.
Re: [Logica-l] Caso de vira-latismo e misoginia no CNPq será o primeiro????
incomodado com os ruídos envolvidos nos cuidados da minha filha durante minhas aulas remotas (Cafofo sem escritório aqui. Também levando em conta este episódio desagradável, não liguei o microfone para fazer minha pergunta no encontro recente em Bristol, pois a pequena estava cantando amavelmente em alto e bom som, e ninguém conseguiria escutar minha pergunta mesmo). Acho que os colegas conhecem os episódios lamentáveis durante a pandemia de mães sendo hostilizadas por patrões, juízes e/ou colegas de trabalho por estarem amamentando ou cuidando da prole durante videochamadas. Eu pude usar efetivamente do machismo arraigado para convencer minha esposa a vagar pelas ruas desertas com a criança no colo nos dias de aula com o tal cidadão. O mesmo não está disponível a uma mulher que amamenta. Dado o contexto brasileiro, as medidas anunciadas pelo CNPq provavelmente afetarão apenas as mães (ou talvez também pais com guarda exclusiva). É um começo! Importante, porque atinge a maioria dos casos. Sim, eu diria que não apenas é um começo, como o correto, dado o cenário nacional atual. Uma situação mais ideal, como a que observamos com a DFG, apenas faz sentido quando em consonância com as demais políticas públicas em geral, como ocorre na Alemanha, mas não no Brasil. Acho que parte da tarefa de tornar o ambiente trabalhista brasileiro (não só o acadêmico) um pouco mais adequado para pessoas com filhos passa por uma reorientação das políticas públicas ao contexto familiar atual, onde pais participam ou desejam participar de maneira equitativa no cuidado dos filhos e famílias nas quais o cuidado das crianças é exercido por casais homossexuais, para citar apenas alguns exemplos. Concordo. Isso vai levar uma vida. Como a gente tem que começar de algum lugar, que tal do mais óbvio? :) O contexto brasileiro é bem distinto. Afinal, a situação de um novo pai com uma rede de suporte local, uma esposa, uma babá e um escritório com isolamento acústico dentro de casa é muitíssimo diferente daquela de uma mãe solteira sem família num raio de mil quilômetros e que more num cafofo de 50 m². Sabemos que temos colegas na universidade em ambos estes extremos, bem como em diversos outros pontos no espectro. Pra qual lado você acha que a balança pende mais? Eu diria que raramente pra babá e escritório com isolamento acústico, ao menos no nosso ambiente brasileiro. Eu diria que o papai hipotético no seu escritório, na verdade, está em condições invejáveis para *alavancar* a sua carreira, nos moldes do seu colega italiano. -- Hermógenes Oliveira -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica --- 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 acessar esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/a2736198-009a-42a7-b492-a5399205d19dn%40dimap.ufrn.br.
[Logica-l] Intuicionismo e racismo? (Clickbait)
Esbarrei numa curiosidade que *talvez* adicione a uma discussão histórica iniciada por João Marcos há algum tempo atrás: https://groups.google.com/a/dimap.ufrn.br/g/logica-l/c/AvSKkMvN-gs/m/ghsLFIngCwAJ Nos anos 50, na época do apartheid <https://en.wikipedia.org/wiki/Population_Registration_Act,_1950>, Brouwer publicou a seguinte peça no South African Journal of Science: https://hdl.handle.net/10520/AJA00382353_3009 OK, nada particularmente surpreendente até aqui. Acontece que, ao buscar pelo artigo no sumário do respectivo volume, notei que o artigo de Brouwer sucede o seguinte artigo cujo título, "The Nation's Intelligence and its Measurement" me chamou a atenção: https://hdl.handle.net/10520/AJA00382353_3008 Dado o título do artigo e o contexto, choca, mas não surpreende, que logo no resumo lê-se coisas do tipo: "There is a shortage in South Africa of people with professional, administrative and technical ability, because a small European population is trying to meet virtually all requirements in these top employment classes for a nation of 12,600,000 people. Potential ability for these functions should therefore be detected at an early age, and developed to its maximum capacity. At the same time, the basic abilities of Africans should be studied to determine what contributions they could eventually make." Asqueroso, não é mesmo? Não li muita coisa de Brouwer (e não gostei muito do pouco que li). Da sua biografia, então, não conheço basicamente nada. Portanto, não sei até que ponto a publicação do artigo dele neste contexto sugere algo sobre sua pessoa. -- Hermógenes Oliveira -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica --- 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 acessar esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/3fc55952-26b1-46a2-a1ca-dcb7a58674edn%40dimap.ufrn.br.