TRADUÇÕES VIA TEORIA DA PROVA: APLICAÇÕES À LÓGICA LINEAR

O objetivo do nosso trabalho é explorar interessantes conexões entre diferentes procedimentos de normalização e traduções entre sistemas lógicos, dando especial ênfase ao caso da Lógica Linear. Mais especificamente, usando recursos da teoria da prova, definiremos uma nova tradução da lógica clássica na lógica intuicionista e estenderemos o Teorema de Glivenko para a lógica de primeira ordem. Além disso, construiremos um sistema proposicional clássico em dedução natural, com conclusão única, para o fragmento multiplicativo da Lógica Linear e mostraremos que tal sistema satisfaz o teorema de normalização. Por fim, mostraremos como transformar provas clássicas do fragmento Linear em questão em provas construtivamente aceitas