Generic generalized Rosser fixed points (Q1099165): Difference between revisions

The usual provability predicate \(\Pr_{PA}\) for Peano arithmetic enjoys a generalized fixed point property: for every total recursive function h there is a sentence C such that \(\vdash_{PA}\Pr_{PA}(\ulcorner C\urcorner)\leftrightarrow \Pr_{PA}(\ulcorner hC\urcorner).\) The formalized Rosser theorem is an instance of this construction. The paper introduces a modal system LR\(=GL+\{\square c_ i\leftrightarrow \square A_ i(c_ i)\), \(c_ i\to \square c_ i|\) \(i\in \omega \}+\square A/A\) (here GL is the logic of arithmetical provability and \(\{c_ i\}_{i\in \omega}\) is the set of new propositional constants). A usual provability interpretation \(\psi\) of GL is extended in such a way that \(\phi c_ i\) is a \(\Sigma\) \(0_ 1\)-sentence and \(\vdash_{PA}\phi (\square c_ i\leftrightarrow \square A_ i(c_ i))\). A modal completeness and a uniform arithmetical completeness theorem with respect of PA are established for LR. A \(\Sigma\) \(0_ 1\)-sentence C for which \(\vdash_{PA}\Pr_{PA}(\ulcorner C\urcorner)\leftrightarrow \Pr_{PA}(\ulcorner \neg C\urcorner)\) is called a generalized Rosser sentence. Corollary: for \(\Pr_{PA}\) there are two non-equivalent generalized Rosser sentences.