<p>A standard sequent system (the system <InlineEquation ID="IEq1"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq1.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="28" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{L}\mathcal{J}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">L</mi> <mi mathvariant="script">J</mi> </mrow> </math></EquationSource> </InlineEquation>), a standard natural deduction system (the system <InlineEquation ID="IEq2"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq2.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="33" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{N}\mathcal{J}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">N</mi> <mi mathvariant="script">J</mi> </mrow> </math></EquationSource> </InlineEquation>) and an extended natural deduction system (the system <InlineEquation ID="IEq3"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq3.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="30" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{N}\mathcal{E}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">N</mi> <mi mathvariant="script">E</mi> </mrow> </math></EquationSource> </InlineEquation>) will be considered. The <InlineEquation ID="IEq4"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq1.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="28" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{L}\mathcal{J}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">L</mi> <mi mathvariant="script">J</mi> </mrow> </math></EquationSource> </InlineEquation>-images of <InlineEquation ID="IEq5"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq2.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="33" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{N}\mathcal{J}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">N</mi> <mi mathvariant="script">J</mi> </mrow> </math></EquationSource> </InlineEquation>-derivations and <InlineEquation ID="IEq6"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq3.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="30" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{N}\mathcal{E}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">N</mi> <mi mathvariant="script">E</mi> </mrow> </math></EquationSource> </InlineEquation>-derivations (<InlineEquation ID="IEq7"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq7.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="40" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal {GLJ}$</EquationSource> <EquationSource Format="MATHML"><math> <mi mathvariant="script">GLJ</mi> </math></EquationSource> </InlineEquation>-derivations and <InlineEquation ID="IEq8"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq8.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="42" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal {PLJ}$</EquationSource> <EquationSource Format="MATHML"><math> <mi mathvariant="script">PLJ</mi> </math></EquationSource> </InlineEquation>-derivations) and the <InlineEquation ID="IEq9"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq3.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="30" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{N}\mathcal{E}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">N</mi> <mi mathvariant="script">E</mi> </mrow> </math></EquationSource> </InlineEquation>-images of <InlineEquation ID="IEq10"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq2.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="33" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{N}\mathcal{J}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">N</mi> <mi mathvariant="script">J</mi> </mrow> </math></EquationSource> </InlineEquation>-derivations (<InlineEquation ID="IEq11"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq11.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="41" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal {ENE}$</EquationSource> <EquationSource Format="MATHML"><math> <mi mathvariant="script">ENE</mi> </math></EquationSource> </InlineEquation>-derivations) will be presented. It will be shown that <InlineEquation ID="IEq12"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq8.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="42" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal {PLJ}$</EquationSource> <EquationSource Format="MATHML"><math> <mi mathvariant="script">PLJ</mi> </math></EquationSource> </InlineEquation>-derivations and <InlineEquation ID="IEq13"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq7.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="40" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal {GLJ}$</EquationSource> <EquationSource Format="MATHML"><math> <mi mathvariant="script">GLJ</mi> </math></EquationSource> </InlineEquation>-derivations have special cuts, nde-cuts and nd-cuts, respectively. Nd-cuts corresponding to maximum segments of <InlineEquation ID="IEq14"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq2.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="33" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{N}\mathcal{J}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">N</mi> <mi mathvariant="script">J</mi> </mrow> </math></EquationSource> </InlineEquation>-derivations (ndam-cuts) and nde-cuts corresponding to maximum segments of <InlineEquation ID="IEq15"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq3.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="30" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{N}\mathcal{E}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">N</mi> <mi mathvariant="script">E</mi> </mrow> </math></EquationSource> </InlineEquation>-derivations (ndeam-cuts) will be studied. It will be shown that (A) an <InlineEquation ID="IEq16"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq2.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="33" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{N}\mathcal{J}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">N</mi> <mi mathvariant="script">J</mi> </mrow> </math></EquationSource> </InlineEquation>-derivation is normal iff its <InlineEquation ID="IEq17"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq3.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="30" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{N}\mathcal{E}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">N</mi> <mi mathvariant="script">E</mi> </mrow> </math></EquationSource> </InlineEquation>-image is normal iff its <InlineEquation ID="IEq18"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq1.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="28" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{L}\mathcal{J}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">L</mi> <mi mathvariant="script">J</mi> </mrow> </math></EquationSource> </InlineEquation>-image has no ndam-cuts; (B) an <InlineEquation ID="IEq19"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq7.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="40" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal {GLJ}$</EquationSource> <EquationSource Format="MATHML"><math> <mi mathvariant="script">GLJ</mi> </math></EquationSource> </InlineEquation>-derivation has no ndam-cuts iff its <InlineEquation ID="IEq20"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq2.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="33" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{N}\mathcal{J}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">N</mi> <mi mathvariant="script">J</mi> </mrow> </math></EquationSource> </InlineEquation>-image is normal iff its <InlineEquation ID="IEq21"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq3.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="30" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{N}\mathcal{E}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">N</mi> <mi mathvariant="script">E</mi> </mrow> </math></EquationSource> </InlineEquation>-image is normal; and (C) an <InlineEquation ID="IEq22"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq11.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="41" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal {ENE}$</EquationSource> <EquationSource Format="MATHML"><math> <mi mathvariant="script">ENE</mi> </math></EquationSource> </InlineEquation>-derivation is normal iff its <InlineEquation ID="IEq23"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq2.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="33" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{N}\mathcal{J}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">N</mi> <mi mathvariant="script">J</mi> </mrow> </math></EquationSource> </InlineEquation>-image is normal iff its <InlineEquation ID="IEq24"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10849_2025_9435_Article_IEq1.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="28" /> </InlineMediaObject> <EquationSource Format="TEX">$\mathcal{L}\mathcal{J}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">L</mi> <mi mathvariant="script">J</mi> </mrow> </math></EquationSource> </InlineEquation>-image has no ndeam-cuts.</p>

Sequent Images of Normal Derivations and Natural Deduction Images of Derivations without M-cuts

期刊论文
发表日期：

2025年9月11日

查看全文

Mirjana Borisavljević

摘要

A standard sequent system (the system $\mathcal{L}\mathcal{J}$ $L J$ ), a standard natural deduction system (the system $\mathcal{N}\mathcal{J}$ $N J$ ) and an extended natural deduction system (the system $\mathcal{N}\mathcal{E}$ $N E$ ) will be considered. The $\mathcal{L}\mathcal{J}$ $L J$ -images of $\mathcal{N}\mathcal{J}$ $N J$ -derivations and $\mathcal{N}\mathcal{E}$ $N E$ -derivations ( $\mathcal {GLJ}$ $GLJ$ -derivations and $\mathcal {PLJ}$ $PLJ$ -derivations) and the $\mathcal{N}\mathcal{E}$ $N E$ -images of $\mathcal{N}\mathcal{J}$ $N J$ -derivations ( $\mathcal {ENE}$ $ENE$ -derivations) will be presented. It will be shown that $\mathcal {PLJ}$ $PLJ$ -derivations and $\mathcal {GLJ}$ $GLJ$ -derivations have special cuts, nde-cuts and nd-cuts, respectively. Nd-cuts corresponding to maximum segments of $\mathcal{N}\mathcal{J}$ $N J$ -derivations (ndam-cuts) and nde-cuts corresponding to maximum segments of $\mathcal{N}\mathcal{E}$ $N E$ -derivations (ndeam-cuts) will be studied. It will be shown that (A) an $\mathcal{N}\mathcal{J}$ $N J$ -derivation is normal iff its $\mathcal{N}\mathcal{E}$ $N E$ -image is normal iff its $\mathcal{L}\mathcal{J}$ $L J$ -image has no ndam-cuts; (B) an $\mathcal {GLJ}$ $GLJ$ -derivation has no ndam-cuts iff its $\mathcal{N}\mathcal{J}$ $N J$ -image is normal iff its $\mathcal{N}\mathcal{E}$ $N E$ -image is normal; and (C) an $\mathcal {ENE}$ $ENE$ -derivation is normal iff its $\mathcal{N}\mathcal{J}$ $N J$ -image is normal iff its $\mathcal{L}\mathcal{J}$ $L J$ -image has no ndeam-cuts.