Luiz Carlos Pereira
Departamento de Filosofia, PUC-Rio/UERJ
Abstract: In the late twenties and early thirties of last century several results were obtained connecting different logics and theories. These results assumed the form of translations/interpretations of one logic/theory into another logic/theory. In 1925 Kolmogorov defined a translation from classical logic into minimal logic aiming to show that “classical mathematics” can be translated into “intuitionistic mathematics”. In 1929 Glivenko proved two fundamental results connecting provability in classical propositional logic to provability in intuitionistic propositional logic. In 1933, Gödel and Gentzen independently defined an interpretation of Classical/Peano Arithmetic (PA) into Heyting’s arithmetic (HA). A preparatory step in Gödel’s interpretation establishes that classical propositional logic cannot be distinguished from intuitionistic propositional logic with respect to theorems in the fragment {~, &}. In 1933 Gödel also defined an interpretation of intuitionistic propositional logic into the classical modal logic S4. A minimum requirement for all these translations is that they preserve deducibility: Given two logics L1 and L2 and a translation T of L2 into L1, then S |-L2 A if and only if T[S] |-L1 T[A]. The aim of the present paper is to examine the following ideas and results concerning translations between logics and theories:
[1] The first result establishes that given two logics L1 and L2 and a translation of L2 into L1, then, given any intermediate logic L3 between L1 and L2, the same translation can be used to translate L2 into L3. It is also shown that this translation cannot be used to translate L3 into L1.
[2] The second group of results and ideas discusses the constructive behavior of different fragments of classical logic.
[3] In 1979, R. Statman showed a translation from intuitionistic propositional logic into its implicational fragment. This reduction is polynomial and proves that the implicational fragment of minimal Logic is PSPACE-complete. The methods that Statman used are based on proof-theory and Natural Deduction in Prawitz Style. The sub-formula principle for a propositional Natural Deduction system NL for a logic L states that whenever α is provable from Γ in L, there is a derivation of α from a set of assumptions {δ1, . . . , δk} ⊆ Γ built up only with sub-formulas of α and/or {δ1, . . . , δk}. We show that any propositional logic L, with a Natural Deduction system that satisfies the sub-formula principle has a translation to purely minimal implicational logic.
[4] The fourth group of results and ideas aims to discuss a view proposed by Dag Prawitz on the relation between intuitionistic and classical logic.
Work in collaboration with Edward Hermann Haeusler (Departamento de Ciência da Computação, PUC-Rio).
This seminar is supported by National Funding from FCT - Fundação para a Ciência e a Tecnologia, under the project: UID/MAT/04561/2013.
