Clone wiki

constructive-provability-logic / Home

Constructive Provability Logic

This repository collects the code (currently all in Agda) for "Constructive Provability Logic," a research project by Robert J. Simmons and Bernardo Toninho.

Principles of Constructive Provability Logic

Tech report, December 2010. (paper and code)(repository tag "2010-tech-report")

The directory Accessibility introduces converse well-founded accessibility relations and contexts (lists) indexed by a converse well-founded accessibility relation, and the directory MinimalCPL describes the formalization and metatheory of a minimal fragment of constructive provability logic as discussed in the tech report.

Constructive Provability Logic

Submitted, January 2011. (submitted version) (repository tag "2011-imla-submission")

In addition to minor updates to the minimal CPL discussed in the tech report, as well as two variants of intuitionistic constructive provability logic (the "tethered" variant is in the directory IntuitionisticCPL, and the "de-tethered" variant is in the directory DetetheredCPL). The proofs of the theorems in Section 3 can all be found in TetheredCPL/Axioms.agda and DetetheredCPL/Axioms.agda, but the proofs of the theorems in Section 2 that deal with the metatheory of CPL and CPL* are a bit scattered; you can find them by clicking these links:

  • Theorem 2.1, Weakening in CPL - here and here.
  • Theorem 2.1, Identity in CPL - here.
  • Theorem 2.1, Cut in CPL - here.
  • Theorem 2.2, Weakening in CPL* - proof here and here, exported here.
  • Theorem 2.2, Identity in CPL* - proof here, exported here.
  • Theorem 2.2, Cut in CPL* - proof here, exported here. An unknown performance issue in Agda means that, even with the termination checker disabled, this proof takes about half an hour to compile. As long as the computational content of cut admissibility is not needed, the file CutAxiom.agda can be used. To add the real cut theorem to the code path, uncomment this line and comment the following line.
  • Theorem 2.2, Decut in CPL* - proof here and here, exported here.

Updated