Portal de Periódicos da CAPES

Proof and infinity: response to André Porto

2008; UNIVERSIDADE ESTADUAL DE CAMPINAS; Volume: 31; Issue: 1 Linguagem: Inglês

2317-630X

Oswaldo Chateaubriand,

Logic, programming, and type systems

The main issue Andre Porto raises in his paper concerns the use of dot notation to indicate an infinite set of hypotheses. Whereas I agree that one cannot extract a unique infinite expansion from a finite initial segment, in my response I argue that this holds for finite expansions as well. I further explain how my remarks on infinite proof structures are neither motivated by the impact of Godel’s incompleteness theorems on Hilbert’s program, nor by a negative view of strict finitism. Resumo: O problema central que Andre Porto discute em seu artigo diz respeito ao uso da notacao de pontos para indicar um conjunto infinito de hipoteses. Mesmo estando de acordo nao ser possivel extrair uma expansao infinita a partir de um segmento inicial finito, em minha replica argumento que isto vale igualmente para expansoes finitas. Explico tambem que minhas observacoes sobre estruturas de prova infinitas nao sao motivadas pelo impacto dos teoremas de incompletude de Godel no programa de Hilbert, e tampouco por uma visao negativa do finitismo estrito. Palavras chave: Expansoes infinitas. Formalizacao. Finitismo estrito.