Denotational Proof Languages (DPLs)

Overview

DPLs are languages for expressing formal proofs and proof-search algorithms in arbitrary logics. Roughly speaking, there are two types of DPLs: type-alpha and type-omega. Type-alpha DPLs allow for proof presentation and checking, but not for proof search. Type-omega DPLs are supersets of type-alpha DPLs, so they allow for proof presentation and checking, but they also allow for proof search, and indeed for arbitrary computation. So type-omega DPLs are actually Turing-complete programming languages, as well as proof frameworks. The languages are structured in such a way that soundness is ensured: the conclusion of a proof D is guaranteed to be a logical consequence of the assumption base in which D is evaluated (more on assumption bases below).

DPLs have formalized key notions such as assumption scope and eigenvariable scope in novel ways (most notably, without reducing them to variable scope in the typed lambda calculus, as is done in Curry-Howard systems via higher-order abstract syntax). In addition, type-omega DPLs have introduced a notion of teasing apart the syntax of computation and deduction in a way that allows the two to be integrated seamlessly and soundly. One of the main contribution of DPLs is the introduction of assumption-base semantics.

An assumption base is just a set of premises: a set of propositions that we take for granted for the purposes of a given stretch of logical discourse. This is traditionally known in logic as a "context," a notion that has been around for a while, particularly in connection with sequent systems, where the basic unit of inference is a pair consisting of a context and a conclusion. What is novel about DPLs is how assumption bases are used to give formal semantics to proofs: the idea that the formal meaning of a proof is a function over assumption bases . That is, the meaning of a proof is specified relative to a given assumption base, in the same way that in denotational semantics the formal meaning of an imperative program is a function over stores. Unlike sequent systems, where the manipulation of the context is explicit and falls on the user, the manipulation and threading of the context in DPLs is implicit and relegated to the underlying semantics---again, much as the manipulation and threading of the store in imperative languages is hidden from the user.

This turns out to be an apt viewpoint that is particularly conducive to giving a rigorous semantics to Fitch-style natural deduction. In general, the introduction of assumption bases as a fundamental semantic abstraction on a par with lexical environments, stores, and continuations allows for an elegant treatment of proof theory, even for logics that have been difficult to formalize in a non-graphical manner. The approach is different from that of systems based on higher-order constructive type theory, such as LF, Coq, or Nuprl. It is more similar to systems of the LCF variety (HOL, Isabelle, etc.), but again, the introduction of assumption bases and the syntactic separation of deduction and computation bring several advantages, e.g. sequents are no longer necessary, and proof abstraction is facilitated.

Moreover, assumption-base semantics enable a rich theory of observational equivalence for proofs, facilitating the formulation---and answering---of questions such as the following:

This is illustrated in a recent paper (to appear in the Journal of Automated Reasoning), which uses ideas of observational proof equivalence based on assumption-base semantics to develop a a procedure for simplifying natural-deduction proofs in first-order logic. You can find a copy of the paper here.

Additional information and downloads

Some DPL resources: