Logic of proofs with complexity operators
Sergei Nikolaevich Artemov, Artëm Chuprina · 2017
The logic of proofs is the modal provability logic enriched by new operators (labeled modalities) for individual proofs. In the current paper we add to the logic of proofs also new labeled modalities which stand for the complexity of proofs. The Kripke style completeness, decidability, and arithmetical completeness theorems are obtained. The complexity logics introduced here correspond to two major classes of complexity measures: decidable and recursively enumerable ones; the completeness theorems relate either of these logics to the entire class of the relevant complexity measures.