×

Provability logic with modalities for arithmetical complexities. (English) Zbl 0714.03018

The propositional system HGL with modalities \(\square\) (for provability in classical arithmetic), \(\Sigma_ i\), \(\Sigma^+_ i\) (for the property of being provably equivalent to a \(\Sigma^ o_ i\) formula, resp. to a Boolean combination of such formulas) is axiomatized by the standard axioms for provability logic, closure property of \(\Sigma_ i\), \(\Sigma^+_ i\) with respect to \(\wedge\), \(\vee\), \(\neg\), implications \(\Sigma\) \(A\vee \square (A\to B)\to \Sigma B\), \(\Sigma\) \(A\to \square \Sigma A\), \(\Sigma A\to \Sigma 'A\) for suitable \(\Sigma\), \(\Sigma '\), and \(\Sigma\perp\), \(\Sigma\square A\), \(\Sigma_ 1A\to \square (A\to \square A)\), \(\Sigma \Sigma 'A\) for all \(\Sigma\), \(\Sigma '\) among \(\Sigma_ i\), \(\Sigma^+_ i\). The proof uses Kripke-type semantics with separate accessibility relations for different modalities.
Reviewer: G.Mints

MSC:

03B45 Modal logic (including the logic of norms)
03F30 First-order arithmetic and fragments
03F40 Gödel numberings and issues of incompleteness
PDFBibTeX XMLCite