Seminário - Lógica Intuicionista,
com a professora Elaine Pimentel do Departamento de Matemática da UFMG
Dias 12 e 19 de maio às 15h na sala 4094
Abstract: A lógica clássica trata de "verdade absoluta", no sentido
que uma sentença bem formada é sempre falsa ou verdadeira, onde o
contrário de falso é verdadeiro e vice-versa. Este fato e' descrito
pelo Princípio do Terceiro Excluído (|- forall A. A \/ neg A). Desta
forma, a lógica clássica possui um não-determinismo intrínseco que é
utilizado na matemática em algumas técnicas de prova, como a redução
ao absurdo, por exemplo.
A lógica intuicionista, por sua vez, trata de "provabilidade": um
predicado é válido se e somente se podemos construir uma prova para o
mesmo. Desta forma, o princípio do terceiro excluído deixa de ser um
teorema. As aplicações dentro da matemática não são muito
interessantes. Por exemplo, não podemos "construir" o conjunto dos
números reais, portanto toda a teoria de anáilse intuicionista é sem
sentido. Mas os modelos matemáticos que descrevem a semântica da
lógica intuicionista (Modelos de Kripke, Semi-álgebras de Boole, etc)
são bem interessantes, bem como o estudo da "computabilidade"de
funções. De fato, o "isomorfismo de Curry-Howard" estabelece uma
relação biunívoca entre a lógica intuicionista e uma teoria de funções
chamada lambda-calculus simplesmente tipado. A primeira vive no mundo
lógico enquanto a segunda no mundo computacional.
O objetivo desses dois seminários é apresentar uma introdução à lógica
intuicionista utilizando "cálculo de sequentes", que é um sistema de
provas. Para tal falaremos também um pouquinho de dedução natural.
que uma sentença bem formada é sempre falsa ou verdadeira, onde o
contrário de falso é verdadeiro e vice-versa. Este fato e' descrito
pelo Princípio do Terceiro Excluído (|- forall A. A \/ neg A). Desta
forma, a lógica clássica possui um não-determinismo intrínseco que é
utilizado na matemática em algumas técnicas de prova, como a redução
ao absurdo, por exemplo.
A lógica intuicionista, por sua vez, trata de "provabilidade": um
predicado é válido se e somente se podemos construir uma prova para o
mesmo. Desta forma, o princípio do terceiro excluído deixa de ser um
teorema. As aplicações dentro da matemática não são muito
interessantes. Por exemplo, não podemos "construir" o conjunto dos
números reais, portanto toda a teoria de anáilse intuicionista é sem
sentido. Mas os modelos matemáticos que descrevem a semântica da
lógica intuicionista (Modelos de Kripke, Semi-álgebras de Boole, etc)
são bem interessantes, bem como o estudo da "computabilidade"de
funções. De fato, o "isomorfismo de Curry-Howard" estabelece uma
relação biunívoca entre a lógica intuicionista e uma teoria de funções
chamada lambda-calculus simplesmente tipado. A primeira vive no mundo
lógico enquanto a segunda no mundo computacional.
O objetivo desses dois seminários é apresentar uma introdução à lógica
intuicionista utilizando "cálculo de sequentes", que é um sistema de
provas. Para tal falaremos também um pouquinho de dedução natural.
Nenhum comentário:
Postar um comentário