Abstract
The purpose of a logical framework such as LF is to provide a language for defining logical systems suitable for use in a logic-independent proof development environment. In previous work we have developed a theory of representation of logics in a logical framework and considered the behaviour of structured theory presentations under representation. That work was based on the simplifying assumption that logics are characterized as families of consequence relations on “closed” sentences. In this report we extend the notion of logical system to account for open formula, and study its basic properties. Following standard practice, we distinguish two types of logical system of open formulae that differ in the treatment of free variables, and show how they may be induced from a logical system of closed sentences. The technical notions of a logic presentation and a uniform encoding of a logical system in LF are generalized to the present setting.
Most definitions in this paper are rather tentative and may change at further stages of our work on these problems.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
A. Avron, F. Honsell, and I. Mason. Using typed lambda calculus to implement formal systems on a machine. Technical Report ECS-LFCS-87-31, Laboratory for the Foundations of Computer Science, Edinburgh University, June 1987.
A. Avron. Simple consequence relations. Technical Report ECS-LFCS-87-30, Laboratory for the Foundations of Computer Science, Edinburgh University, June 1987.
K.J. Barwise. Axioms for abstract model theory. Ann. of Mathematical Logic 7:221–265, 1974.
R. Burstall and J. Goguen. The semantics of CLEAR, a specification language. In Proc. of Advanced Course on Abstract Software Specifications, Copenhagen, pages 292–332, Springer LNCS 86, 1980.
J. Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209–243, 1986.
R.L. Constable, et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, 1986.
N.G. de Bruijn. A survey of the project AUTOMATH. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pages 589–606, Academic Press, 1980.
J. Fiadeiro and A. Sernadas. Structuring theories on consequence. In D. Sannella and A. Tarlecki, editors, Selected Papers from the Fifth Workshop on Specification of Abstract Data Types, Gullane, Scotland, pages 44–72, Springer LNCS 332, 1988.
J. Goguen and R. Burstall. Introducing institutions. In E. Clarke and D. Kozen, editors, Logics of Programs, pages 221–256, Springer LNCS 164, 1984.
R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. In Proc. of the 2nd IEEE Symp. on Logic in Computer Science, Ithaca, New York, pages 194–204, 1987.
R. Harper, D. Sannella, A. Tarlecki. Structure and representation in LF. In Proc. of the 4th IEEE Symp. on Logic in Computer Science, Asilomar, California, pages 226–237, 1989.
J. Meseguer. General logics. In Proc. Logic Colloquium '87, North-Holland, 1989.
D. Sannella and R. Burstall. Structured theories in LCF. In Proc. of the 8th Colloq. on Algebra and Trees in Programming, L'Aquila, Italy, pages 377–391, Springer LNCS 159, 1983.
D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Computation, 76:165–210, 1988.
A. Tarlecki. Quasi-varieties in abstract algebraic institutions. Journal of Computer and System Sciences, 33:333–360, 1986.
A. Tarlecki, R. Burstall, and J. Goguen. Some fundamental algebraic tools for the semantics of computation, Part III: Indexed categories. To appear, Theoretical Computer Science.
D.T. van Daalen. The Language Theory of AUTOMATH. Ph.D. thesis, Technical University of Eindhoven, Eindhoven, Netherlands, 1980.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Harper, R., Sannella, D., Tarlecki, A. (1989). Logic representation in LF. In: Pitt, D.H., Rydeheard, D.E., Dybjer, P., Pitts, A.M., Poigné, A. (eds) Category Theory and Computer Science. Lecture Notes in Computer Science, vol 389. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0018356
Download citation
DOI: https://doi.org/10.1007/BFb0018356
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51662-0
Online ISBN: 978-3-540-46740-3
eBook Packages: Springer Book Archive