... vou supor que qualquer fundação de matemática adequada tanto para a raciocínio humano quanto para a verificação por computador deva ter as seguintes três componentes. A primeira é um sistema de dedução formal: uma linguagem e regras de manipulação de sentenças puramente formais, de modo que o registro destas manipulações possa ser verificado por um programa de computador. A segunda componente é uma estrutura que atribui um significado às sentenças desta linguagem em termos de objetos mentais intuitivamente compreensíveis por seres humanos. A terceira componente é uma estrutura que permite aos seres humanos codificar as ideias matemáticas em termos dos objetos diretamente associados à linguagem.

Objetivo: neste curso vamos aprender essas três componentes para melhor se basear em matemática.

Ementa básica: Lógica proposicional. Variáveis e quantificadores. Equivalência lógica. Tautologias. Conjuntos e operações com eles. Funções, injetoras e sobrejetoras. Axiomas de Peano, indução. Conjuntos finitos. Cardinalidade e cardinais. Matemática construtiva X não; lei do terceiro excluído, axioma da escolha. Programas assistentes de provas (Lean, Coq, Agda, HOL/Isabelle, ...). Prática em Lean.

Os possíveis bônus: método diagonal de Cantor e a sua reiteração por Russel, Gödel, Brouwer, Lawvere; conjuntos X tipos, Dedução natural, cálculo λ, lógica: clássica X intuicionista, interpretação de Brouwer-Heyting-Kolmogorov, isomorfismo de Curry-Howard.

Bibliografia:

Maioria da bibliopgrafia acima é copiada de https://leanprover-community.github.io/learn.html [0] é um jogo, uma gamificação do trabalhos de Grassmann e Peano. Ela serve como uma pre-introdução ao Lean e às provas. [1,2] são livros introdutórios às provas, e [2] ao mesmo tempo é o introdutório ao Lean. [3,4] são alternativas um doutro. [6] é o livro texto sobre Provando os Teoremas em Lean, escrito pelo autor dele, Leonardo de Moura (Microsoft Research, doutor da PUC-Rio (2000)). [7,6,8] servem como a introdução a teoria atrás de assistentes de provas: a Teoria dos Tipos e o Cálculo das Construções Indutivas. Toda bibliografia é livremente disponível online, maioria licenciada por Creative Commons com códigos fontes abertos: [0] no https://github.com/ImperialCollegeLondon/natural_number_game, [1] no https://gitlab.com/cnewstead/infdesc, [2,6] no https://leanprover.github.io, [3,4,5,7] no https://leanprover-community.github.io, [8] no https://github.com/HoTT/book.