Logica matematica

Projeto de pesquisa: L´gica Matem´tica, teoria o a da prova e teoria de fun¸˜es co
Coordenadora: Elaine Gouvˆa Pimentel e Pesquisadores: Dale Miller Simona Ronchi della Rocca Luca Paolini Luca Roversi Alessio Guglielmi Paola Bruscoli Alunos: M´rio S´rgio Ferreira Alvim J´ nior a e u Vivek Nigam Fabiana Lopes Fernandes Carlos Salvador Murray Giselle Machado Nogueira Reis Henrique Antunes Almeida Frederico Augusto Menezes Ribeiro Joyce Figueir´ o 19 de novembro de 2008

1

Sum´rio a
1 Identifica¸˜o da proposta ca 2 Qualifica¸˜o dos problemas a serem abordados ca 3 Objetivos 4 Organiza¸˜o do projeto ca 5 Metodologia 6 Revis˜o da literatura a 6.1 PARTE I . . . . . . . . . . . . . . . . . . . . . . . . . 6.1.1 L´gica (cl´ssica) de primeira ordem . . . . . . o a 6.1.2 L´gica intuicionista . . . . . . . . . . . . . . . . o 6.1.3 L´gica Linear . . . . . . . . . . . . . . . . . . . o 6.1.4 L´gica e Matem´tica . . . . . . . . . . . . . . . o a 6.1.5 L´gica e Ciˆncia da Computa¸ao . . . . . . . . o e c˜ 6.1.6 Dedu¸ao natural versus c´lculo de seq¨ entes . . c˜ a u 6.1.7 Cut elimination . . . . . . . . . . . . . . . . . . 6.1.8 Logical frameworks . . . . . . . . . . . . . . . . 6.1.9 L´gica Linear como framework para especificar o de seq¨ entes . . . . . . . . . . . . . . . . . . . u 6.2 PARTE II . . . . . . . . . . . . . . . . . . . . . . . . . 6.2.1 λ-calculus e computabilidade . . . . . . . . . . 6.2.2 λ-calculus tipado simples . . . . . . . . . . . . 6.2.3 Sistema de tipos interse¸ao . . . . . . . . . . . c˜ 6.2.4 Isomorfismo de Curry-Howard . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . sistemas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 4 4 5 6 6 6 6 8 10 11 12 13 15 15 16 17 17 20 22 23

7 Principais contribui¸oes cient´ c˜ ıficas 24 7.1 PARTE I . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 7.2 PARTE II . . . . . . . . . . . . . . . . .