Hostname: page-component-78c5997874-t5tsf Total loading time: 0 Render date: 2024-11-13T09:22:27.219Z Has data issue: false hasContentIssue false
  • English
  • Français

Lambek's categorical proof theory and Läuchli's abstract realizability

Published online by Cambridge University Press:  12 March 2014

Victor Harnik  and
Michael Makkai
Victor Harnik
Affiliation:
Department of Mathematics, McGill University, Montréal, Québec H3A 2K6, Canada, E-mail: [email protected].
Michael Makkai
Affiliation:
Department of Mathematics, University of Haifa, 31999 Haifa, Israel, E-mail: [email protected], [email protected]
Get access Rights & Permissions [Opens in a new window]

Extract

In this paper we give an introduction to categorical proof theory, and reinterpret, with improvements, Läuchli's work on abstract realizability restricted to propositional logic (but see [M1] for predicate logic). Partly to make some points of a foundational nature, we have included a substantial amount of background material. As a result, the paper is (we hope) readable with a knowledge of just the rudiments of category theory, the notions of category, functor, natural transformation, and the like. We start with an extended introduction giving the background, and stating what we do with a minimum of technicalities.

In three publications [L1, 2, 3] published in the years 1968, 1969 and 1972, J. Lambek gave a categorical formulation of the notion of formal proof in deductive systems in certain propositional calculi. The theory is also described in the recent book [LS]. See also [Sz].

The basic motivation behind Lambek's theory was to place proof theory in the framework of modern abstract mathematics. The spirit of the latter, at least for the purposes of the present discussion, is to organize mathematical objects into mathematical structures. The specific kind of structure we will be concerned with is category.

In Lambek's theory, one starts with an arbitrary theory in any one of several propositional calculi. One has the (formal) proofs (deductions) in the given theory of entailments A ⇒ B, with A and B arbitrary formulas. One introduces an equivalence relation on proofs under which, in particular, equivalent proofs are proofs of the same entailment; equivalence of proofs is intended to capture the idea of the proofs being only inessentially different. One forms a category whose objects are the formulas of the underlying language of the theory, and whose arrows from A to B, with the latter arbitrary formulas, are the equivalence classes of formal proofs of A ⇒ B.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 57 , Issue 1 , March 1992 , pp. 200 - 230
Copyright
Copyright © Association for Symbolic Logic 1992

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

[BD]Barr, M. and Diaconescu, R., Atomic toposes, Journal of Pure and Applied Algebra, vol. 17 (1980), pp. 1–24.CrossRefGoogle Scholar
[BKP]Blackwell, R., Kelly, G. M. and Power, A. J., Two-dimensional monad theory, Journal of Pure and Applied Algebra, vol. 59 (1989), pp. 1–41.CrossRefGoogle Scholar
[BW]Barr, M. and Wells, C., Toposes, triples and theories, Springer-Verlag, Berlin, 1985.CrossRefGoogle Scholar
[CWM]Lane, S. Mac, Categories for the working mathematician, Springer-Verlag, Berlin, 1971.CrossRefGoogle Scholar
[He]Heyting, A., Intuitionism, North-Holland, Amsterdam, 1956.Google Scholar
[Ho]Howard, W. A., The formulae-as-types notion of construction, To H. B. Curry: essays on combinatory logic, lambda calculus and formalism (Seldin, J. R. and Hindley, J. R., editors), Academic Press, New York, 1980, pp. 479–490.Google Scholar
[IM]Kleene, S. C., Introduction to metamathematics, Van Nostrand, Princeton, New Jersey, 1952.Google Scholar
[J]Johnstone, P. T., Topos theory, Academic Press, New York, 1977.Google Scholar
[L1]Lambek, J., Deductive systems and categories. I, Mathematical Systems Theory, vol. 2 (1968), pp. 287–318.CrossRefGoogle Scholar
[L2]Lambek, J., Deductive systems and categories. II, Category theory, homology theory and their applications, I (Hilton, P., editor), Lecture Notes in Mathematics, vol. 86, Springer-Verlag, Berlin, 1969, pp. 76–122.CrossRefGoogle Scholar
[L3]Lambek, J., Deductive systems and categories. III, Toposes, algebraic geometry and logic (Lawvere, F. W., editor), Lecture Notes in Mathematics, vol. 274, Springer-Verlag, Berlin, 1972, pp. 57–82.CrossRefGoogle Scholar
[La]Läuchli, H., An abstract notion of realizability for which intuitionistic predicate calculus is complete, Intuitionism and proof theory (Kino, A.et al., editors), North-Holland, Amsterdam, 1970, pp. 227–234.Google Scholar
[LS]Lambek, J. and Scott, P. J., Introduction to higher order categorical logic, Cambridge University Press, Cambridge, 1986.Google Scholar
[M1]Makkai, M., The fibrational formulation of intuitionistic predicate calculus. I: Completeness according to Gödel, Kripke and Läuchli, Notre Dame Journal of Formal Logic (submitted).Google Scholar
[M2]Makkai, M., The fibrational formulation of intuitionistic predicate calculus. II: The algebra of proofs (in preparation).Google Scholar
[MR]Makkai, M. and Reyes, G. E., First order categorical logic, Lecture Notes in Mathematics, vol. 611, Springer-Verlag, Berlin, 1977.CrossRefGoogle Scholar
[Pr]Prawitz, D., Ideas and results in proof theory, Proceedings of the second Scandinavian logic symposium (Fenstad, J. E., editor), North-Holland, Amsterdam, 1971, pp. 235–307.CrossRefGoogle Scholar
[Sz]Szabo, M. E., Algebras of proofs, North-Holland, Amsterdam, 1978.Google Scholar
[Tr]Troelstra, A. S. (editor), Metamathematical investigations of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin, 1973.CrossRefGoogle Scholar