Hostname: page-component-78c5997874-g7gxr Total loading time: 0 Render date: 2024-11-05T16:41:36.826Z Has data issue: false hasContentIssue false

Deductive Completeness

Published online by Cambridge University Press:  15 January 2014

Kosta Došen*
Affiliation:
University of Toulouse III, Institut de Recherche en Informatique de Toulouse 118 Route de Narbonne, 31062 Toulouse Cedex, France Mathematical Institute, Knez Mihailova 35, P.O. Box 367, 11001 Belgrade, Yugoslavia

Abstract

This is an exposition of Lambek's strengthening and generalization of the deduction theorem in categories related to intuitionistic propositional logic. Essential notions of category theory are introduced so as to yield a simple reformulation of Lambek's Functional Completeness Theorem, from which its main consequences can be readily drawn. The connections of the theorem with combinatory logic, and with modal and substructural logics, are briefly considered at the end.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1996

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1994] Cubrié, D., Embedding of a free cartesian closed category into the category of sets, Journal of Pure and Applied Algebra, to appear.Google Scholar
[1993] Došen, K. and Petrić, Z., Modal functional completeness, Proof theory of modal logic (Wansing, H., editor), Kluwer, Dordrecht, to appear.Google Scholar
[1994] Došen, K. and Petrić, Z., Cartesian isomorphisms are symmetric monoidal: A justification of linear logic, manuscript.Google Scholar
[1966] Eilenberg, S. and Kelly, G. M., Closed categories, Proceedings of the conference on categorical algebra, La Jolla 1965 (Eilenberg, S. et al., editors), Springer-Verlag, Berlin, pp. 421562.Google Scholar
[1935] Gentzen, G., Untersuchungen über das logische Schließen, Mathematische Zeitschrift, vol. 39, pp. 176–210, 405431, English translation in The collected papers of Gerhard Gentzen (M.E. Szabo, editor), North-Holland, Amsterdam, 1969.CrossRefGoogle Scholar
[1994] Ja§kowski, S., On the rules of suppositions in formal logic, Studia Logica, vol. 1, pp. 532, reprinted in Polish logic 1920-1939 (S. McCall, editor), Oxford University Press, Oxford, 1967.Google Scholar
[1969] Lambek, J., Deductive systems and categories II: Standard constructions and closed categories, Category theory, homology theory and their applications I, Lecture Notes in Mathematics, no. 86, Springer-Verlag, Berlin, pp. 76122.CrossRefGoogle Scholar
[1972] Lambek, J., Deductive systems and categories III: Cartesian closed categories, intuitionist propositional calculus and combinatory logic, Toposes, algebraic geometry and logic (Lawvere, F. W., editor), Lecture Notes in Mathematics, no. 274, Springer-Verlag, Berlin, pp. 5782.CrossRefGoogle Scholar
[1974] Lambek, J., Functional completeness of cartesian categories, Annals of Mathematical Logic, vol. 6, pp. 259292.CrossRefGoogle Scholar
[1989] Lambek, J., Multicategories revisited, Categories in computer science and logic (Gray, J. W. and Scedrov, A., editors), Contemporary Mathematics, vol. 92, American Mathematical Society, Providence, pp. 217239.CrossRefGoogle Scholar
[1993] Lambek, J., Logic without structural rules (Another look at cut elimination), Substructural logics (Dosen, K. and Schroeder-Heister, P., editors), Oxford University Press, Oxford, pp. 179206.CrossRefGoogle Scholar
[1986] Lambek, J. and Scott, P. J., Introduction to higher-order categorical logic, Cambridge University Press, Cambridge.Google Scholar
[1971] Lane, S. Mac, Categories for the working mathematician, Springer-Verlag, Berlin.CrossRefGoogle Scholar
[1993] Makkai, M., The fibrational formulation of intuitionistic predicate logic I: Completeness according to Gödel, Kripke and Läuchli, Part 1, Notre Dame Journal of Formal Logic, vol. 34, pp. 334377.Google Scholar
[1965] Prawitz, D., Natural deduction: A proof-theoretical study, Almqvist & Wiksell, Stockholm.Google Scholar
[1971] Prawitz, D., Ideas and results in proof theory, Proceedings of the second Scandinavian logic symposium (Fenstad, J. E., editor), North-Holland, Amsterdam, pp. 235307.CrossRefGoogle Scholar
[1950] Rosenbloom, P.C., The elements of mathematical logic, Dover, New York.Google Scholar
[1956] Tarski, A., Logic, semantics, metamathematics: Papers from 1923 to 1938 (Woodger, J. H., editor), Oxford University Press, Oxford.Google Scholar