(Universidade de Lisboa)
Uma nova noção de realizabilidade
Data: 7/3/05 (segunda feira)
Local: Sala 5.5
Hora: 14h
Resumo
O método da realizabilidade (Kleene, 1945) providencia uma forma de
tornar explícito o conteúdo construtivo das frases aritméticas. O
método está intimamente ligado à lógica intuicionista e lembra a
interpretação de Brouwer-Heyting-Kolmogorov dos conectivos lógicos. Em
particular, o método decide disjunções e fornece testemunhas de
asserções existenciais. Apresentamos uma nova noção de realizabilidade
que apenas dá majorantes de testemunhas existenciais e que não decide
disjunções. A nova noção suporta uma versão muito geral do Teorema FAN
de Brouwer e entrosa muito bem com certos princípios não
intuicionistas, como o lema fraco de König ou o princípio fraco da
omnisciência limitada. No entanto, não joga bem com o princípio de
Markov, o que a torna de pouca utilidade para a obtenção de informação
computacional de demonstrações clássicas da análise através da
tradução de Gödel-Gentzen. No final da conferência apresentaremos
brevemente uma nova interpretação funcional (depois de Gödel 1958) que
não sofre desta falha.
Reinhard Kahle, 3.03.05