Cálculos de múltipla conclusão para a lógica intuicionista sob uma perspectiva geométrica

• Ano de defesa: 2017
• Autor(a) principal: CARVALHO, Ruan Vasconcelos Bezerra
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal de Pernambuco; UFPE; Brasil; Programa de Pos Graduacao em Ciencia da Computacao
• Palavras-chave em Português: Teoria da computação; Teoria da prova; Lógica intuicionista
• Link de acesso: https://repositorio.ufpe.br/handle/123456789/28009

Como verificar se uma prova clássica também é intuicionista? Em dedução natural basta não haver ocorrência da lei do terceiro excluído ou da eliminação da dupla negação, conforme proposto por Gentzen. No seu cálculo de sequentes o mesmo resultado é alcançado restringindo o número de fórmulas no lado direito a no máximo um. Assim não há múltiplaconclusão, embora esta seja importante para a simetria. Hoje já existem abordagens que levam isso em conta e propõem cálculos de sequentes para lógica intuicionista com várias fórmulas no consequente. Mas ainda que elas nos forneçam compreensões do que diferencia a lógica intuicionista da clássica, há o problema da burocracia inerente ao formalismo de Gentzen. Aqui separamos a lógica intuicionista da clássica em derivações não-sequenciais adotando uma abordagem geométrica. Propomos uma versão intuicionista para dois sistemas de múltipla conclusão inicialmente definidos apenas para a lógica clássica proposicional: os N-Grafos, apresentados por de Oliveira (2001) e baseado em dedução natural; e as proof-nets de Robinson (2003), inspiradas no cálculo de sequentes.