# Term-Generic Logic

From FSL

## J. of TCS

**Term-Generic Logic**- Andrei Popescu and Grigore Rosu
, Volume 577(1), pp 1-24. 2015**Journal of Theoretical Computer Science**

*Abstract.*We introduce term-generic logic (TGL), a first-order logic parameterized with terms defined axiomatically (rather than constructively), by requiring terms to only provide free variable and substitution operators satisfying some reasonable axioms. TGL has a notion of model that generalizes both first-order models and Henkin models of the lambda-calculus. The abstract notions of term syntax and model are shown to be sufficient for obtaining the completeness theorem of a Gentzen system generalizing that of first-order logic. Various systems featuring bindings and contextual reasoning, ranging from pure type systems to the pi-calculus, are captured as theories inside TGL. For two particular, but rather typical instances---untyped lambda-calculus and System F---the general-purpose TGL models are shown to be equivalent with standard ad hoc models.

## WADT'08

- Andrei Popescu and Grigore Rosu
, LNCS 5486, pp 290-307. 2009**WADT'08**

*Abstract.**Term-generic logic (TGL)*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. TGL has a complete Gentzen system generalizing that of first-order logic. A certain fragment of TGL, called Horn^2, possesses a much simpler Gentzen system, similar to traditional typing derivation systems of lambda-calculi. Horn^2 appears to be sufficient for defining a whole plethora of lambda-calculi as*theories*inside the logic. Within intuitionistic TGL, a Horn^2 specification of a calculus is likely to be*adequate by default*. A bit of extra effort shows adequacy w.r.t. classic TGL as well, endowing the calculus with a complete loose semantics.