Scholarlink

<p>This paper introduces a <InlineEquation ID="IEq1"> <EquationSource Format="TEX">\(\textsf{G3}\)</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="sans-serif">G</mi> <mn mathvariant="sans-serif">3</mn> </mrow> </math></EquationSource> </InlineEquation>-style sound and complete sequent calculus for the Russellian approach to definite description presented by Indrzejczak and some co-authors in previous works. We show that the calculi introduced have the good structural properties that are distinctive of <InlineEquation ID="IEq2"> <EquationSource Format="TEX">\(\textsf{G3}\)</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="sans-serif">G</mi> <mn mathvariant="sans-serif">3</mn> </mrow> </math></EquationSource> </InlineEquation>-style calculi: weakening and contraction are height-preserving admissible, all rules are height-preserving invertible, and cut is admissible. Having all rules invertible, the calculus allows to extract a countermodel from a failed proof search. Moreover, we use the calculus to give a Maehara-style constructive proof of Craig Interpolation Property. Finally, we extend the approach to intuitionistic logic.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

G3-Style Sequent Calculi and Craig Interpolation Property for Logics with Russellian Definite Descriptions

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年4月15日

查看全文
  • Norbert Gratzl,
  • Eugenio Orlandelli,
  • Edi Pavlović

摘要

This paper introduces a \(\textsf{G3}\) G 3 -style sound and complete sequent calculus for the Russellian approach to definite description presented by Indrzejczak and some co-authors in previous works. We show that the calculi introduced have the good structural properties that are distinctive of \(\textsf{G3}\) G 3 -style calculi: weakening and contraction are height-preserving admissible, all rules are height-preserving invertible, and cut is admissible. Having all rules invertible, the calculus allows to extract a countermodel from a failed proof search. Moreover, we use the calculus to give a Maehara-style constructive proof of Craig Interpolation Property. Finally, we extend the approach to intuitionistic logic.