Robert J. Simmons: HomeResearch

Constructive provability logic

Constructive provability logic is the generic name for two families of modal logics. Both variants of constructive provability logic are broadly similar to Alex Simpson's intuitionistic Kripke semantics as presented in his thesis, "The Proof Theory and Semantics of Intuitionistic Modal Logic." Like constructive provability logic, the intuitionistic Kripke semantics is a set of logical principles describing the behavior of a hypothetical judgment. Within the framework of the logic's defining principles, various modal connectives can be defined by giving introduction and elimination rules that respect the defining principles.

The two variants of constructive provability logic can be distinguished by whether contradiction at an accessible world implies contradiction at the current world (whether ◊⊥ implies ⊥). In "tethered" constructive provability logic (or CPL), this is not the case: ◊⊥ does not imply ⊥. In "de-tethered" constructive provability logic (or CPL*), contradiction at any accessible world implies a contradiction at the current world.

The logic's presentation co-evolved with a formalization of the logic and its metatheory in the Agda proof assistant. All claimed results about the metatheory of constructive provability logic have been formalized in Agda, though the claimed connection between hybrid CPL* and logic programming with stratified negation has not been formalized.


Papers are listed in reverse chronological order.


This is a presentation given at IMLA 2011 in Nancy, France on July 25, 2011. An earlier version of this presentation was given at CMU on May 11, 2011, and an extended version of this presentation was given at INRIA Saclay on July 26, 2011.