Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4662718 | Annals of Pure and Applied Logic | 2009 | 16 Pages |
Abstract
We establish the bi-modal forgetful projection of the Logic of Proofs and Formal Provability GLA. That is to say, we present a normal bi-modal provability logic with modalities □ and ⊠ whose theorems are precisely those formulas for which the implicit provability assertions represented by the ⊠ modality can be realized by explicit proof terms.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic