On Rosser's Provability Predicate

✍ Scribed by V. Yu. Shavrukov

• Book ID: 102940826
• Publisher: John Wiley and Sons
• Year: 1991
• Tongue: English
• Weight: 693 KB
• Volume: 37
• Category: Article
• ISSN: 0044-3050
• DOI: 10.1002/malq.19910371906

✦ Synopsis

In their paper [4] GUASPARI and SOLOVAY investigate the system R of modal provability logic extended with witness comparison operators o A < B and D A I o B (see also SMO-RYI~SKI (91 and DE JONGH 151). These are intended to express that there is a proof of A whose Godel-number is smaller than resp. smaller than or equal to the Godel-number of any proof of B. They prove an arithmetical completeness theorem which states that R is precisely all that can be generally said (i. e. proved in arithmetic) about i and 5 .

In this paper we restrict our attention to witness comparison formulas of the form A < e 7 A . This is abbreviated by oRA because "to have a proof smaller than any refutation" is, in essence, the provability concept used by ROSSER [7] to strengthen GODEL'S First Incompleteness Theorem. Some modal principles valid for 0, which stands for the usual provability formula, and O R were listed in VISSER 1111.