Formato: Presencial

Local: IMECC - Auditório

Horário: 16h

Charles Sanders Peirce introduziu o método de tabelas de verdade em 1885, no seu artigo “Sobre a álgebra da lógica: uma contribuição à filosofia da notação”, décadas antes de Russell e Wittgenstein.

Em um manuscrito em seu conhecido “Logic Notebook” (1865-1909), datado de 23 de Fevereiro, 1909, e não publicado até 1966, Peirce apresentou em forma matricial as bases lógicas para um sistema proposicional trivalorado, antecipando em mais de dez anos os sistemas multivalorados introduzidos em 1920 por Ján Łukasiewicz, e Emil Post em 1921.

Nesta apresentação, analisaremos esse manuscrito no contexto da produção intelectual de Peirce, fazendo alegações sobre o seu pioneirismo no uso de conceitos da lógica contemporânea e no uso de tabelas de verdade, e o pondo entre os precursores de lógicas não clássicas em geral, em particular multivaloradas, intuicionistas e lógicas paraconsistentes,introduzidas no século 20.

Formato: Online

Local: IMECC - Sala 226 (para acompanhar juntes)

Horário: 16h30min

Link de inscrição para acessar online.

Nesta palestra,  apresentaremos alguns desenvolvimentos recentes associados sobretudo a trabalhos de alunos e ex-alunos do IME-USP sobre feixes sobre quantales e conjuntos a valores em quantais, retomando um tema de estudos envolvendo lógica e categorias realizados no IME-USP  na metade final dos anos 1990,  mas agora  sob uma nova perspectiva: considerando quantais semicartesianos e comutativos, como generalizações não idempotentes de  locales (= álgebras de Heyting completas). 

Listaremos algumas propriedades das categorias (monoidais) obtidas, indicando algumas semelhanças e diferenças com os topos de Grothendieck. 

O objetivo de fundo destes esforços é desenvolver uma generalização monoidal mas não cartesiana da noção de topos elementar,  de modo a cobrir algumas situações matemáticas (incluindo  generalizações dos espaços métricos) e  possibilitar um estudo axiomático destas categorias e uma definição geral  de sua lógica interna, que apresenta indícios de ser alguma forma de logica linear.

Formato: Online

Local: IMECC - Sala 126 (para acompanhar juntes)

Link de inscrição para acessar online.

Os recentes avanços da computação são, sem dúvida, impressionantes. Mas não se deixe enganar, nem tudo está resolvido. Muito pelo contrário, boa parte dos problemas práticos possui certa dificuldade inerente que muitos acreditam tornar impossível a existência de algoritmos exatos, eficientes e completos para eles. Ou seja, mesmo quando conseguimos, em teoria, resolver problemas com computadores, na prática pode levar uma eternidade para obter a resposta. Mas então está tudo perdido? Como lidamos com tais problemas na prática?

Kurt Gödel inicia  seu famoso artigo de 1931 sobre os Teoremas da Incompletude   afirmando que "todos os métodos de prova usados hoje em matemática são formalizados, isto é, reduzidos a alguns poucos axiomas e regras de inferência".

Essa formalização é a abstrata, desenvolvida no século XIX, mas as novas  tecnologias formais para matemática mudam o cenário, e  já começa a aparecer uma nova  matemática formal com base em assistentes de prova, em especial  COQ,  LEAN e  ISABELLE.

Na Inteligência Artificial  há uma distinção  entre métodos simbólicos, que dependem de representações explícitas  do conhecimento  (Lógica), e métodos subsimbólicos, onde  a informação é representada por padrões de dados em  redes neurais  (probabilidades). Métodos formais  são eminentemente simbólicos.  Mas os LLM (Grandes Modelos de Linguagem), com lógica  limitada, já chegaram a  descobertas  matemáticas  surpreendentes.

Como esclarece J. Avigad em "Mathematics and the Formal Turn" de 2024, o  maior desafio  para a IA é encontrar abordagens que combinem as  características de aprendizado de máquina e raciocínio simbólico, e a  matemática é um lugar ideal para começar.Contudo, há riscos de que estes  métodos formais interfiram  na agenda da ciência, e tirem o foco da matemática   como ajuda à  compreensão humana dos  fenômenos  abstratos.  

Vamos discutir estas ideias emocionantes!

Referências:

Jeremy Avigad.Mathematics and the formal turn.

Bull. Amer. Math. Soc.    Published electronically: February 15, 2024

DOI: https://doi.org/10.1090/bull/1832

 Kevin Buzzard. Proving Theorems with Computers. Notices Amer. Math. Soc. 67 (2020),   1791–1799, DOI 10.1090/noti. MR420192

Walter Carnielli. How AI can be surprisingly dangerous for the philosophy of mathematics— and of science.

Circumscribere Vol. 27 (2021) online

https://revistas.pucsp.br/index.php/circumhc/article/view/55033

Walter Carnielli. Sobre a prova matemática mais ousada da existência de Deus.

Unus Mundus, Belo Horizonte, n. 2, jul-dez, 2023.

Online, https://unusmundus.academiaabc2.org.br/sobre-a-prova-matematica-mais-ousada-da-existencia-de-deus/