LF: a Foundational Higher-Order Logic


This paper presents a new system of logic, LF, that is intended to be used as the foundation of the formalization of science. That is, deductive validity according to LF is to be used as the criterion for assessing what follows from the verdicts, hypotheses, or conjectures of any science. In work currently in progress, we argue for the unique suitability of LF for the formalization of logic, mathematics, syntax, and semantics. The present document specifies the language and rules of LF, lays out some notational conventions, and states some basic technical facts about the system.



External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

Similar books and articles

An Overview of Type Theories.Nino Guallart - 2015 - Axiomathes 25 (1):61-77.
Higher-Order Logic or Set Theory: A False Dilemma.S. Shapiro - 2012 - Philosophia Mathematica 20 (3):305-323.
The Broadest Necessity.Andrew Bacon - 2018 - Journal of Philosophical Logic 47 (5):733-783.
The Clausal Theory of Types.D. A. Wolfram - 1993 - Cambridge University Press.
Higher Order Modal Logic.Reinhard Muskens - 2006 - In Patrick Blackburn, Johan Van Benthem & Frank Wolter (eds.), Handbook of Modal Logic. Elsevier. pp. 621-653.
CERES in higher-order logic.Stefan Hetzl, Alexander Leitsch & Daniel Weller - 2011 - Annals of Pure and Applied Logic 162 (12):1001-1034.
Extensionalizing Intensional Second-Order Logic.Jonathan Payne - 2015 - Notre Dame Journal of Formal Logic 56 (1):243-261.


Added to PP

293 (#65,635)

6 months
293 (#6,795)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Juhani Yli-Vakkuri
Australian Catholic University
Zachary Goodsell
National University of Singapore

Citations of this work

No citations found.

Add more citations

References found in this work

Uber Sinn und Bedeutung.Gottlob Frege - 1892 - Zeitschrift für Philosophie Und Philosophische Kritik 100 (1):25-50.
Universal grammar.Richard Montague - 1970 - Theoria 36 (3):373--398.
The Broadest Necessity.Andrew Bacon - 2018 - Journal of Philosophical Logic 47 (5):733-783.
A formulation of the simple theory of types.Alonzo Church - 1940 - Journal of Symbolic Logic 5 (2):56-68.
Principia Mathematica.Alfred North Whitehead & Bertrand Russell - 1950 - Cambridge,: Franklin Classics. Edited by Bertrand Russell.

View all 14 references / Add more references