Term-Generic First-Order Logic

Papescu, Andrei; Rosu, Grigore

Permalink

https://hdl.handle.net/2142/11196 Copy

Description

Title

Term-Generic First-Order Logic

Author(s)

• Papescu, Andrei
• Rosu, Grigore

Issue Date

2006-04

Keyword(s)

computer science

Abstract

Term-generic first-order logic, or simply generic first-order logic (GFOL), is presented as a first-order logic parameterized with terms defined axiomatically (rather than constructively), by requiring them to only provide generic notions of free variable and substitution satisfying reasonable properties. A complete Gentzen deduction system is given, as well as complete equational and many-sorted extensions. It is shown that various calculi with binding, such as lambda-calculus and System F, can be faithfully defined as GFOL theories. Since GFOL is complete, by defining a logic or calculus as a GFOL theory one gets, at no additional effort, a semantics for that logic or calculus. A fragment of GFOL called Horn^2 is also defined, on whose theories, under certain conditions, the generic Gentzen deduction system is equivalent to a simplified deduction system which resembles the derivation system of the calculi that we intend to explicitly capture. Consequently, GFOL and especially its fragment Horn^2 can serve as a foundationaldefinitional framework for other calculi and logics, providing these with models and complete deduction.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11196

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections