Term-generic logic

Andrei Popescu, Grigore Roşu

Research output: Contribution to journalArticlepeer-review

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 λ-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 π-calculus, are captured as theories inside TGL. For two particular, but rather typical instances-untyped λ-calculus and System F-the general-purpose TGL models are shown to be equivalent with standard ad hoc models.

Original languageEnglish (US)
Pages (from-to)1-24
Number of pages24
JournalTheoretical Computer Science
Volume577
Issue number1
DOIs
StatePublished - 2015

Keywords

  • Semantics
  • Substitution
  • Term-generic logic
  • λ-Calculus
  • π-Calculus

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Term-generic logic'. Together they form a unique fingerprint.

Cite this