A Constructive Canonical Model for the Logic of Proofs

Following Artemov (2001), we proceed with establishing arithmetical com­pleteness of the logic of proofs by building a decidable version of the canonical model for LP and then embedding this model into PA.

Though the logic of proofs has a basic model, cf. Chapter 3, we need more information about the structure of this model for its arithmetization. For his­torical reasons, we present the original construction of a decidable canonical model for the logic of proofs from Artemov (1995, 2001) because this was the first nonarithmetical model of the logic of proofs.

Sequents were discussed in Chapter 5, though primarily with respect to modal logics. We now need a corresponding version for the justification logic LP itself. By a sequent we mean a pair Γ ) A where Γ and A are finite sets of LP-formulas. By Γ, F we mean Γ U {F}. Without loss of generality we assume a Boolean basis →, ? and treat the remaining Boolean connectives as defined.

Axioms of LPq are sequents of the form A ) A and ? ). Along with the usual Gentzen sequent rules of classical propositional logic, cf. Chapter 5, including the cut and weakening rules, the system LPq contains the rules

1

Basically, this means that A tries all possible paths.

Saturated sequents get us halfway to the desired constructive version of the canonical model for LP₀. What we need is also a closure of the “true set” under operations and LP-principles (which makes such “true set” infinite and forces us to abandon the convenient framework of sequents).

Lemma 9.11 (Completion Lemma) For each saturated sequentnot

9.3