zbMATH — the first resource for mathematics

Solution of a problem of David Guaspari. (English) Zbl 0923.03025
Orłowska, Ewa (ed.), Logic at work. Essays dedicated to the memory of Helena Rasiowa. Heidelberg: Physica-Verlag. Stud. Fuzziness Soft Comput. 24, 246-254 (1999).
If \(L\) is a logic with a collection of arithmetical interpretations, then we call a formula \(A\) of \(L\) essentially \(\Sigma_1\) with respect to theory \(T\) if, under any arithmetical interpretation \(*\) of \(L\) into \(T\), \(A^*\) is a \(\Sigma_1\)-formula. D. Guaspari [J. Symb. Log. 48, 777-789 (1983; Zbl 0547.03035)] stated as a question: whether in the Guaspari-Solovay system \(R\), which extends the system \(GL\) (Gödel-Löb) with symbols for witness comparisons, the essentially \(\Sigma_1\) formulae w.r.t. an r.e. theory extending \(I\Sigma_1\) are the ones which are, provably in \(R\), equivalent to a (possibly empty) disjunction of conjunctions of \(\square\)-formulae and witness comparison formulae. A. Visser answered Guaspari’s question for the system \(GL\) positively. In the paper under review, the authors prove first the conjecture for the simple case of \(GL\), because this clarifies the method (very different from Visser’s) used in the more complicated case of \(R\). By using interpretability logic \(ILM\) and Kripke models, the authors solve the Guaspari problem for the system \(R\).
For the entire collection see [Zbl 0910.00016].

03B45 Modal logic (including the logic of norms)
03F30 First-order arithmetic and fragments