O Intucionismo no Contexto da Computação Científica

O paradigma """"fórmulas como tipos"""" de curry, estabelecendo a correspondência combinatória (teoria da funcionalidade) e lógica intuicionista (fragmento proposicional e implicacional), é considerado tradicionalmente como o ponto de partida do encontro entre lógica e ciência da computação, cuja expressão é o isomorfismo de Curry-Howard. O intuicionismo foi assim o primeiro sistema lógico a fundamentar seu caráter construtivo na ciência da computação. A noção de construção/construtividade acompanha toda a tradição intuicionista desde Brouwer. No domínio da lógica, especialmente, a semântica de Heyting baseada em condições de prova (construção) é considerada um paradigma, opondo-se à visão clássica tarskiana baseada em condições de verdade. Os trabalhos de Heyting serviram de referência teórica para desenvolvimentos futuros, sobretudo em teoria da prova. A intenção aqui é estudar alguns sistemas de prova utilizados para apresentar a lógica intuicionista de acordo com sua adequação à semântica procedural de Heyting bem como o """"grau""""de algoritmicidade (construtividade), critério qualitativo que indica o """"quanto""""um aparato dedutivo se aproxima de um algoritmo.