# Logical framework

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Logical_framework
> Markdown URL: https://mediated.wiki/source/Logical_framework.md
> Source: https://en.wikipedia.org/wiki/Logical_framework
> Source revision: 1345093488
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

In [logic](/source/logic), a '''logical framework''' provides a means to define (or present) a logic as a signature in a higher-order [type theory](/source/type_theory) in such a way that [provability](/source/Provability_logic) of a formula in the original logic reduces to a [type inhabitation](/source/type_inhabitation) problem in the framework type theory.<ref name="Jacobs2001">{{cite book|author=Bart Jacobs|title=Categorical Logic and Type Theory|year=2001|publisher=Elsevier|isbn=978-0-444-50853-9|page=598}}</ref><ref name="Gabbay1994">{{cite book|editor=Dov M. Gabbay|title=What is a logical system?|url=https://books.google.com/books?id=XqCu4XjHrIQC&pg=PA382|year=1994|publisher=[Clarendon Press](/source/Clarendon_Press)|isbn=978-0-19-853859-2|page=382}}</ref> This approach has been used successfully for (interactive) [automated theorem proving](/source/automated_theorem_proving). The first logical framework was [Automath](/source/Automath); however, the name of the idea comes from the more widely known Edinburgh Logical Framework, '''LF'''. Several more recent proof tools like [Isabelle](/source/Isabelle_(theorem_prover)) are based on this idea.<ref name="Jacobs2001"/> Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system.<ref name="BoveBarbosa2009">{{cite book|author1=Ana Bove|author2=Luis Soares Barbosa|author3=Alberto Pardo|title=Language Engineering and Rigorous Software Development: International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised, Selected Papers|url=https://books.google.com/books?id=YOqHiA5MYpEC&pg=PA48|year=2009|publisher=Springer|isbn=978-3-642-03152-6|pages=48}}</ref>

==Overview==
A logical framework is based on a general treatment of syntax, rules and proofs by means of a [dependently typed lambda calculus](/source/dependent_type_theory). Syntax is treated in a style similar to, but more general than [Per Martin-Löf](/source/Per_Martin-L%C3%B6f)'s system of arities.

To describe a logical framework, one must provide the following:

# A characterization of the class of object-logics to be represented;
# An appropriate meta-language;
# A characterization of the mechanism by which object-logics are represented.

This is summarized by:

:"''Framework = Language + Representation''."

==LF==
In the case of the '''LF logical framework''', the meta-language is the [λΠ-calculus](/source/%CE%BB%CE%A0-calculus). This is a system of first-order dependent function types which are related by the [propositions as types principle](/source/propositions_as_types_principle) to [first-order](/source/first-order_logic) [minimal logic](/source/minimal_logic). The key features of the λΠ-calculus are that it consists of entities of three levels: objects, types and kinds (or type classes, or families of types). It is [predicative](/source/Impredicativity), all well-typed terms are [strongly normalizing](/source/strongly_normalizing) and [Church-Rosser](/source/Church-Rosser) and the property of being well-typed is [decidable](/source/Decidability_(logic)). However, [type inference](/source/type_inference) is undecidable.

A logic is represented in the '''LF logical framework''' by the judgements-as-types representation mechanism. This is inspired by [Per Martin-Löf](/source/Per_Martin-L%C3%B6f)'s development of [Kant](/source/Immanuel_Kant)'s notion of [judgement](/source/judgement_(mathematical_logic)), in the 1983 Siena Lectures. The two higher-order judgements, the hypothetical <math>J\vdash K</math> and the general, <math>\Lambda x\in J. K(x)</math>, correspond to the ordinary and dependent function space, respectively. The methodology of judgements-as-types is that judgements are represented as the types of their proofs. A [logical system](/source/logical_system) <math>{\mathcal L}</math> is represented by its signature which assigns kinds and types to a finite set of constants that represents its syntax, its judgements and its rule schemes. An object-logic's rules and proofs are seen as primitive proofs of hypothetico-general judgements <math>\Lambda x\in C. J(x)\vdash K</math>.

An implementation of the LF logical framework is provided by the [Twelf](/source/Twelf) system at [Carnegie Mellon University](/source/Carnegie_Mellon_University). Twelf includes
* a logic programming engine
* meta-theoretic reasoning about logic programs (termination, coverage, etc.)
* an inductive [meta-logic](/source/meta-logic)al theorem prover

==See also==
* [Grammatical Framework](/source/Grammatical_Framework)
* [Turnstile (symbol)](/source/Turnstile_(symbol))

==References==
{{reflist}}

==Further reading==
* {{cite book|editor=[Helmut Schwichtenberg](/source/Helmut_Schwichtenberg), Ralf Steinbrüggen|title=Proof and system-reliability|chapter=Logical frameworks – a brief introduction|year=2002| publisher=[Springer](/source/Springer_Science%2BBusiness_Media) |isbn=978-1-4020-0608-1|author=[Frank Pfenning](/source/Frank_Pfenning)|url=https://www.cs.cmu.edu/~fp/papers/mdorf01.pdf}}
*[Robert Harper](/source/Robert_Harper_(computer_scientist)), Furio Honsell and [Gordon Plotkin](/source/Gordon_Plotkin). ''A Framework For Defining Logics''. Journal of the Association for Computing Machinery, 40(1):143-184, 1993.
*[Arnon Avron](/source/Arnon_Avron), Furio Honsell, Ian Mason and Randy Pollack. ''Using typed lambda calculus to implement formal systems on a machine''. Journal of Automated Reasoning, 9:309-354, 1992.
*Robert Harper. ''An Equational Formulation of LF''. Technical Report, [University of Edinburgh](/source/University_of_Edinburgh), 1988. LFCS report ECS-LFCS-88-67.
*Robert Harper, Donald Sannella and Andrzej Tarlecki. ''Structured Theory Presentations and Logic Representations''. Annals of Pure and Applied Logic, 67(1–3):113-160, 1994.
*Samin Ishtiaq and David Pym. ''A Relevant Analysis of Natural Deduction''. Journal of Logic and Computation 8, 809–838, 1998.
* Samin Ishtiaq and David Pym. ''Kripke Resource Models of a Dependently-typed, Bunched <math>\lambda</math>-calculus''. Journal of Logic and Computation 12(6), 1061–1104, 2002.  
* Per Martin-Löf. "[https://web.archive.org/web/20060104064335/http://www.hf.uio.no/filosofi/njpl/vol1no1/meaning/meaning.html On the Meanings of the Logical Constants and the Justifications of the Logical Laws]." "[Nordic Journal of Philosophical Logic](/source/Nordic_Journal_of_Philosophical_Logic)", 1(1): 11–60, 1996.
* Bengt Nordström, Kent Petersson, and  Jan M. Smith. ''Programming in Martin-Löf's Type Theory''. [Oxford University Press](/source/Oxford_University_Press), 1990.  (The book is out of print, but [http://www.cs.chalmers.se/Cs/Research/Logic/book/ a free version] has been made available.)
*David Pym. ''A Note on the Proof Theory of the <math>\lambda\Pi</math>-calculus''. Studia Logica 54: 199–230, 1995. 
*David Pym and [Lincoln Wallen](/source/Lincoln_Wallen). ''Proof-search in the <math>\lambda\Pi</math>-calculus''. In: G. Huet and G. Plotkin (eds), Logical Frameworks, Cambridge University Press, 1991.  
*Didier Galmiche and David Pym. ''Proof-search in type-theoretic languages:an introduction''. Theoretical Computer Science 232 (2000) 5-53.    
*Philippa Gardner. ''Representing Logics in Type Theory''. Technical Report, University of Edinburgh, 1992. LFCS report ECS-LFCS-92-227.
*Gilles Dowek. ''The undecidability of typability in the lambda-pi-calculus''. In M. Bezem, J.F. Groote (Eds.), Typed Lambda Calculi and Applications. Volume 664 of ''Lecture Notes in Computer Science'', 139–145, 1993. 
*David Pym. ''Proofs, Search and Computation in General Logic''. Ph.D. thesis, University of Edinburgh, 1990.
*David Pym. ''A Unification Algorithm for the <math>\lambda\Pi</math>-calculus.'' International Journal of Foundations of Computer Science 3(3), 333–378, 1992.

==External links==
* [https://www.cs.cmu.edu/~fp/lfs-impl.html Specific Logical Frameworks and Implementations] (a list maintained by [Frank Pfenning](/source/Frank_Pfenning), but mostly dead links from 1997)

Category:Logic in computer science
Category:Type theory
Category:Proof assistants
Category:Dependently typed programming

---
Adapted from the Wikipedia article [Logical framework](https://en.wikipedia.org/wiki/Logical_framework) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Logical_framework?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.