Skip Navigation

Journal of Logic and Computation 2005 15(6):821-854; doi:10.1093/logcom/exi055
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by DeMarco, M.
Right arrow Articles by Lipton, J.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

Vol. 15 No. 6, © The Author, 2005. Published by Oxford University Press. All rights reserved.

Original Articles

Completeness and Cut-elimination in the Intuitionistic Theory of Types

Mary DeMarco1 and Jame Lipton2

1 1615 Commonwealth Ave # 18, Brighton, MA 02135, USA. Email: mcdemarco{at}gmail.com, 2 Dept. of Math and Computer Science, Wesleyan University, Middletown, CT 06457, USA, and Visiting Researcher, Facultad de Informática, Universidad Politécnica de Madrid, Spain. Email: jlipton{at}wesleyan.edu

In this paper we define a model theory and give a semantic proof of cut-elimination for ICTT, an intuitionistic formulation of Church's theory of types defined by Miller et al. and the basis for the {lambda}Prolog programming language. Our approach, extending techniques of Takahashi and Andrews and tableaux machinery of Fitting, Smullyan, Nerode and Shore, is to prove a completeness theorem for the cut-free fragment and show semantically that cut is a derived rule. This allows us to generalize a result of Takahashi and Schütte on extending partial truth valuations in impredicative systems. We extend Andrews' notion of Hintikka sets to intuitionistic higher-order logic in a way that also defines tableau-provability for intuitionistic type theory. In addition to giving a completeness theorem without using cut we then show, using cut, how to establish completeness of more conventional term models. These models give a declarative semantics for the logic underlying the {lambda}Prolog programming language.

Keywords: Mathematical logic, type theory, lambda calculus, theorem proving, logic programming, proof theory, cut-elimination, impredicative formal systems

Received 27 April 2004.


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.