Generic First-Order Logic

From FSL
Jump to: navigation, search

Generic first-order logic (GFOL) is 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. GFOL has a complete Gentzen system generalizing that of FOL. GFOL can conveniently define a wide variety of lambda-calculi as theories, by instanciating its syntax and stating the appropriate axioms. GFOL endows its theories with a default loose semantics, complete for the specified calculi.

Why Consider GFOL?

GFOL is yet another logic, in the wide spectrum of existing ones (including de Bruijn encodings, Combinatory Logics, HOAS, Nominal Logic and many others) aimed toward specification of calculi. What makes GFOL special?

  • It develops a "special relationship" with its defined calculi, as it does not encode them, but rather generalizes all of them.
  • It provides a complete set-theoretic semantics for all its specified calculi in a uniform way - interestingly, this semantics turns out to be equivalent to the ad-hoc, "domain specific" one previously proposed for some of these calculi.
  • It encourages a semantic specification style, which brings:
    • Significantly more compact definitions than the purely syntactic definitions: the latter need to handle all the syntactic details of a calculus (such as variable capturings, typing environments) from scratch;
    • Meaningful intuitions: the calculus' axioms are stated about models, and they have a straightforward intuitive content.

For more details, including a large pool of GFOL calculi specifications, see the publications below.

What GFOL is Not

GFOL is not a framework for implementing lambda-calculi (at least not yet). The problems that GFOL addresses are different from the ones that a technique like HOAS addresses. We capture lambda-calculi conceptually, in that GFOL generalizes all these calculi. As it stands right now, GFOL is just model theory that provides a convenient higher-order language and built-in semantics for defining calculi, just like equational logic provides these features for its particular theories, like group theory. On the other hand, a HOAS framework like Edinburgh LF addresses convenient encoding and reasoning techniques, and GFOL's model theory is not competing with these.


Term-Generic Logic 
Andrei Popescu and Grigore Rosu
WADT'08, LNCS 5486, pp 290-307. 2009
GFOL: a Term-Generic Logic for Defining Lambda-Calculi 
Andrei Popescu and Grigore Rosu
Technical Report UIUCDCS-R-2006-2756, July 2006

Personal tools