# 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