<p>The notion of <InlineEquation ID="IEq1"> <EquationSource Format="TEX">\((\varOmega , \varepsilon )\)</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mo stretchy="false">(</mo> <mi>Ω</mi> <mo>,</mo> <mi>ε</mi> <mo stretchy="false">)</mo> </mrow> </math></EquationSource> </InlineEquation>-inductive sequents plays an important role in correspondence theory and proof theory. This paper simplifies the definition of <InlineEquation ID="IEq2"> <EquationSource Format="TEX">\((\varOmega , \varepsilon )\)</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mo stretchy="false">(</mo> <mi>Ω</mi> <mo>,</mo> <mi>ε</mi> <mo stretchy="false">)</mo> </mrow> </math></EquationSource> </InlineEquation>-inductive sequents for distributive modal logic by ‘internalizing’ the dependency order <InlineEquation ID="IEq3"> <EquationSource Format="TEX">\(&lt;_\varOmega \)</EquationSource> <EquationSource Format="MATHML"><math> <msub> <mo>&lt;</mo> <mi>Ω</mi> </msub> </math></EquationSource> </InlineEquation>. The new definition is called <InlineEquation ID="IEq4"> <EquationSource Format="TEX">\(\varepsilon \)</EquationSource> <EquationSource Format="MATHML"><math> <mi>ε</mi> </math></EquationSource> </InlineEquation><i>-inductive sequents</i>. Furthermore, this paper shows that every <InlineEquation ID="IEq5"> <EquationSource Format="TEX">\(\varepsilon \)</EquationSource> <EquationSource Format="MATHML"><math> <mi>ε</mi> </math></EquationSource> </InlineEquation>-inductive sequent is elementary by an adapted proof. The adapted proof suggests that the order to eliminate propositional variables in an inductive sequent is irrelevant.</p>

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

Inductive Sequents for Distributive Modal Logic

  • Jinsheng Chen

摘要

The notion of \((\varOmega , \varepsilon )\) ( Ω , ε ) -inductive sequents plays an important role in correspondence theory and proof theory. This paper simplifies the definition of \((\varOmega , \varepsilon )\) ( Ω , ε ) -inductive sequents for distributive modal logic by ‘internalizing’ the dependency order \(<_\varOmega \) < Ω . The new definition is called \(\varepsilon \) ε -inductive sequents. Furthermore, this paper shows that every \(\varepsilon \) ε -inductive sequent is elementary by an adapted proof. The adapted proof suggests that the order to eliminate propositional variables in an inductive sequent is irrelevant.