<p>We study interpolation properties for Shavrukov’s bimodal logic <InlineEquation ID="IEq3"> <EquationSource Format="TEX">$\textbf{GR}$</EquationSource> <EquationSource Format="MATHML"><math> <mi mathvariant="bold">GR</mi> </math></EquationSource> </InlineEquation> of usual and Rosser provability predicates. For this purpose, we introduce a new sublogic <InlineEquation ID="IEq4"> <EquationSource Format="TEX">$\textbf{GR}^\circ $</EquationSource> <EquationSource Format="MATHML"><math> <msup> <mi mathvariant="bold">GR</mi> <mo>∘</mo> </msup> </math></EquationSource> </InlineEquation> of <InlineEquation ID="IEq5"> <EquationSource Format="TEX">$\textbf{GR}$</EquationSource> <EquationSource Format="MATHML"><math> <mi mathvariant="bold">GR</mi> </math></EquationSource> </InlineEquation> and its relational semantics. Based on our new semantics, we prove that <InlineEquation ID="IEq6"> <EquationSource Format="TEX">$\textbf{GR}^\circ $</EquationSource> <EquationSource Format="MATHML"><math> <msup> <mi mathvariant="bold">GR</mi> <mo>∘</mo> </msup> </math></EquationSource> </InlineEquation> and <InlineEquation ID="IEq7"> <EquationSource Format="TEX">$\textbf{GR}$</EquationSource> <EquationSource Format="MATHML"><math> <mi mathvariant="bold">GR</mi> </math></EquationSource> </InlineEquation> enjoy Lyndon interpolation property and uniform interpolation property. As a consequence of our proofs, we obtain the completeness and the finite frame property of <InlineEquation ID="IEq8"> <EquationSource Format="TEX">$\textbf{GR}^\circ $</EquationSource> <EquationSource Format="MATHML"><math> <msup> <mi mathvariant="bold">GR</mi> <mo>∘</mo> </msup> </math></EquationSource> </InlineEquation> and <InlineEquation ID="IEq9"> <EquationSource Format="TEX">$\textbf{GR}$</EquationSource> <EquationSource Format="MATHML"><math> <mi mathvariant="bold">GR</mi> </math></EquationSource> </InlineEquation> with respect to our new semantics.</p>

Interpolation Properties for the Bimodal Provability Logic $\textbf{GR}$

期刊论文
出版模式：

开放获取
发表日期：

2025年2月5日

查看全文

Haruka Kogure,
Taishi Kurahashi

摘要

We study interpolation properties for Shavrukov’s bimodal logic $\textbf{GR}$ $GR$ of usual and Rosser provability predicates. For this purpose, we introduce a new sublogic $\textbf{GR}^\circ $ ${GR}^{\circ}$ of $\textbf{GR}$ $GR$ and its relational semantics. Based on our new semantics, we prove that $\textbf{GR}^\circ $ ${GR}^{\circ}$ and $\textbf{GR}$ $GR$ enjoy Lyndon interpolation property and uniform interpolation property. As a consequence of our proofs, we obtain the completeness and the finite frame property of $\textbf{GR}^\circ $ ${GR}^{\circ}$ and $\textbf{GR}$ $GR$ with respect to our new semantics.

Interpolation Properties for the Bimodal Provability Logic \(\textbf{GR}\)

摘要