Formulas with only one atomic formula in Grzegorczyk logic and provability logic(Proof Theory of Arithmetic)
Katsumi Sasaki · Institutional Repositories DataBase (IRDB) · 2007
Here we discuss the set $\mathrm{S}(p)$ of the formulas having only one atomic formula $p$ in Grzegorczyk logicGrzand the set $\mathrm{S}(\perp)$ of the formulas having only one atomic formula 1 in provability logic $\mathrm{G}\mathrm{L}$ .We give an inductive construction of representatives in the quotient set $\mathrm{S}(p)/\equiv_{\mathrm{G}\mathrm{r}\mathrm{z}}$ modulo the provability of Grz.On the other hand, in Boolos [1], it was shown that any formula $A\in \mathrm{S}(\perp)$ is equivalent to some truth-functional combination of formulas of the form $\square ^{k}\perp \mathrm{i}\mathrm{n}\mathrm{G}\mathrm{L}$ .We modify it and give representatives in the quotient set $\mathrm{S}(\perp)/\equiv_{\mathrm{G}\mathrm{L}}$ , which correspond to the representatives for Grz.By these representatives, we clarify structures $\langle \mathrm{S}(p)/\equiv_{\mathrm{G}\mathrm{r}\mathrm{z}}, \leq_{\mathrm{G}\mathrm{r}\mathrm{z}}\rangle$ and $\langle \mathrm{S}(\perp)/\equiv_{\mathrm{G}\mathrm{L}}, \leq_{\mathrm{G}\mathrm{L}}\rangle$ , where $\leq_{\mathrm{L}}$is the derivation in $\mathrm{L}\in$ {Grz, $\mathrm{G}\mathrm{L}$ }.Comparing these two structures, we also give a way to express the $\mathrm{G}\mathrm{L}$ -provability of formulas in $\mathrm{S}(\perp)$ in Grz.In spite of the simplicity of $\mathrm{S}(p)$ and $\mathrm{S}(\perp)$ , it is worth considering since the quotient sets are infinite.There is few result on such structures with infinite quotient sets.One result was given in Nishimura [7] in intuitionistic propositional logic, however, the target set of formulas are also simple, with only two atomic formulas $p\mathrm{a}\mathrm{n}\mathrm{d}\perp$ .Shehtman [11] considered more general structure for Grz.however, in our simple case, our results have more infomation.