Intrinsic reasoning about functional programs I: first order theories

Annals of Pure and Applied Logic 114 (1-3):117-153 (2002)

Daniel M. Leivant
Indiana University, Bloomington
We propose a rudimentary formal framework for reasoning about recursion equations over inductively generated data. Our formalism admits all equational programs , and yet singles out none. While being simple, this framework has numerous extensions and applications. Here we lay out the basic concepts and definitions; show that the deductive power of our formalism is similar to that of Peano's Arithmetic; prove a strong normalization theorem; and exhibit a mapping from natural deduction derivations to an applied λ -calculus, à la Curry–Howard, which provides a transparent proof of Gödel's result that the provably recursive functions of PA are definable by primitive recursion in finite types. Also of interest is the extent, uncommon among similar constructions, to which our mapping is oblivious to first order terms, including first order quantification and equality. Additional applications and extensions of the method will be presented in sequel papers. In particular, the methodology introduced here lends itself to systematic links between natural sub-formalisms and computational complexity classes. Since these sub-formalisms are largely transparent, allowing one to reason formally in the full system while leaving to automatic software tools the task of verifying that restrictions are complied with, the framework is particularly attractive for the development of Feasible Mathematics
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/s0168-0072(01)00078-1
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 47,413
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Ideas and Results in Proof Theory.Dag Prawitz & J. E. Fenstad - 1975 - Journal of Symbolic Logic 40 (2):232-234.
Mathematical Logic.Georg Kreisel - 1967 - Journal of Symbolic Logic 32 (3):419-420.
Universal Algebra.Karl Meinke & John V. Tucker - 1992 - In S. Abramsky, D. Gabbay & T. Maibaurn (eds.), Journal of Symbolic Logic. Oxford University Press. pp. 1--189.

Add more references

Citations of this work BETA

2003 Annual Meeting of the Association for Symbolic Logic.Andreas Blass - 2004 - Bulletin of Symbolic Logic 10 (1):120-145.

Add more citations

Similar books and articles


Added to PP index

Total views
3 ( #1,225,501 of 2,291,812 )

Recent downloads (6 months)
1 ( #825,549 of 2,291,812 )

How can I increase my downloads?


My notes

Sign in to use this feature