Resumen
A common misconception among logicians is to think that intuitionism is necessarily tied-up with single conclusion (sequent or Natural Deduction) calculi. Single conclusion calculi can be used to model intuitionism and they are convenient, but by no means are they necessary. This has been shown by such influential textbook authors as Kleene, Takeuti and Dummett, to cite only three. If single conclusions are not necessary, how do we guarantee that only intuitionistic derivations are allowed? Traditionally one insists on restrictions on particular rules: implication right, negation right and universal quantification right are required to be single conclusion rules. In this note we show that instead of a cardinality restriction such as oneconclusion-only, we can use a notion of dependency between formulae to enforce the constructive character of derivations. The system we obtain, called FIL for full intuitionistic logic, satisfies basic properties such as soundness, completeness and cut elimination. We present two motivating applications of FIL and discuss some future work.Citas
BELLIN, G. “Subnets of Proof-nets in multiplicative linear logic with MIX”. Mathematical Structures in Computer Science, 7, pp. 663-699, 1997.
BIERMAN, G. “A note on full intuitionistic linear logic”. Annals of Pure and
Applied Logic, 79(3), pp. 281-287, 1996.
BRÄUNER, T. “A cut-free Gentzen formulation of the modal logic S5”. Journal of the IGPL, 8, 2000.
BRAÜNER, T. and DE PAIVA, V. “Cut-elimination for Full Intuitionistic Linear Logic”. BRICS Report Series, RS-96-10, 1996.
DE MEDEIROS, M. da P. N. “Investigações acerca de uma versão modal
para a lógica intermediária dos domínios constantes”. Princípios, 8(10),
pp. 121-137, 2001.
DE PAIVA, V., PEREIRA, L.C. “A new proof system for intuitionistic logic”. The Bulletin of Symbolic Logic, 1(1), p. 101, 1995 (abstract).
FRANKLIN, L. DE S. “Sistemas com múltiplas conclusões para a lógica
proposicional intuicionista”. MSc. Dissertation, PUC-Rio, 2000.
HYLAND, J.M.E. and DE PAIVA, V. “Full lntuitionistic linear logic”. Annals of Pure and Applied Logic, 64, pp. 273-291, 1993.
KASHIMA, R. “Cut-elimination for the intermediate logic CD”. Research
Report on Information Sciences C-100, Tokyo Institute of Technology, 1991.
KASHIMA, R. and SHIMURA, T. “Cut-elimination theorem for the Logic of Constant Domains”. Mathematical Logic Quarterly, 40, pp. 153-172,
KLENNE, S.C. Introduction to Metamathematics. Amsterdam: North-Holland, 1952.
LÓPEZ-ESCOBAR, E.G.K. “A second paper ‘on the interpolation theorem for the logic of constant domains’ ”. The Journal of Symbolic Logic, 48, pp. 595-599, 1983.
MAEHARA, S. “Eine Darstellung der intuitionistischen Logik in der klassischen”. Nagoya Mathematical Journal, 7, pp. 45 -64, 1954.
SCHELLINX, H. “Some syntactical observations in linear logic”. Journal of
Logic and Computation, 1(4), pp. 537-559, 1991.
TAKEUTI, G. Proof Theory. Amsterdam: North-Holland, 1975.