拓扑拟布尔代数的多型显示演算

可在www.sciencedirect.com在线获取理论计算机科学电子笔记344（2019）101-118www.elsevier.com/locate/entcs粗糙代数的真多型显示演算朱塞佩·格列柯乌得勒支大学-乌得勒支，荷兰费亮山东大学哲学与社会发展学院-中国山东克里希纳·马努尔卡印度理工学院-坎普尔，印度亚历山德拉·帕尔米贾诺Delft University of Technology - Delft，the Netherlands约翰内斯堡大学-南非约翰内斯堡摘要本文赋予拓扑拟布尔代数、拓扑拟布尔代数5、1-3型中间代数和预粗代数的逻辑以适当的多型显示演算，这些演算是可靠的、完备的、保守的，并具有割消和子公式性质.我们的建议建立在代数分析和应用的原则，多类型的方法在显示结石的设计。关键词：粗糙集，拓扑拟布尔代数，拓扑拟布尔代数5，准粗代数，中间代数，标准扩张，多型演算，真显示演算。1介绍粗糙代数和相关结构与不完美信息的形式模型紧密相关[24]，并且已经使用泛代数和代数逻辑的技术研究了20多年，产生了一个新的概念。1 第四作者的研究得到了NWO Vidi赠款016.138.314，NWO Aspasia的支持。 补助金015.008.054，以及2013年颁发的代尔夫特技术奖学金https://doi.org/10.1016/j.entcs.2019.07.0071571-0661/© 2019作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。102G. Greco等人/理论计算机科学电子笔记344（2019）101丰富的理论，发展了代数语义，对偶，表示和证明理论，其相关的逻辑（参见。例如[1，20，4，25，26]）。特别地，在[25，26]中，已经为这些逻辑引入了健全的和完全的微积分。然而，这些演算中的切割规则是不可消除的。最近，在[22]中为这些逻辑中的一些引入了具有割消和子公式性质的非标准版本的代数演算，但不是为所谓的3型中间代数的逻辑（参见[23]）。[25]，定义2.11）。在这些演算中，子公式性质是非标准的，因为每个逻辑连接词有四个引入规则，其中两个是非标准的，在否定的范围内引入给定的逻辑连接词。在本文中，我们引入了一族与[ 25 ]中讨论的“粗糙代数”2类相关的逻辑的真显示演算定义2.1）。我们采用多类型演算的方法，其主要特点是系统地使用代数逻辑，对偶和表示的概念和见解来解决结构证明理论中的问题。 多类型演算在[10，8，9]中被引入，受[14，11]的启发，并且已经证明在赋予广泛的多样性和不同动机的逻辑系统方面是有效的，从基本格逻辑跨越到[18]到探究逻辑[12]，微积分的可靠性、完备性、守恒性、割消和子公式性质都得到了广义理论的一致保证。这种方法有助于创建一个总体框架，在这个框架中，次协调逻辑（如半德摩根逻辑[15]和双格逻辑[16，21]）的代数证明理论可以与非常知名的和表现良好的逻辑（如线性逻辑[19]和一阶逻辑[27]）联系起来研究。多类型演算还允许捕获给定逻辑的广泛类别的公理扩展[17]，因此为新逻辑家族的设计提供了强大且灵活的环境，例如[2]中引入的那些逻辑家族，以推理代理本文的第一个贡献是粗糙代数的等价表示，基于所谓的异质代数[3]。直觉上，异质代数是具有多个定义域的代数，它们的运算可能跨越不同的定义域。对应于粗糙代数的异质代数类有三个域，分别对应于近似空间的一般集和上、下可定义这三个域中的每一个对应于不同的类型。捕获一般集合的上下可定义近似的模态运算符然后被建模为从一般类型到两个可定义类型之一的异构映射。给出了粗糙代数的等价非均匀表示2 虽然“粗糙代数”这个名字在本文中，我们发现用它作为拓扑拟布尔代数类及其子类的通名是很方便的。G. Greco等人/理论计算机科学电子笔记344（2019）101103自然地配备了多类型的逻辑语言，并且其特征在于可以容易地被识别为分析归纳的公理化（cf. [17，定义55]），因此，通过多类型演算的一般理论，可以有效地由适当的多类型显示演算来捕获，这些演算是健全的、完整的、保守的，并且享有切割消除和标准子公式属性，假定所有连接词的引入规则是标准的。本文的第二个贡献是对这些结石的与[22]相比，多类型方法允许更多的模块性，这不仅使其有可能解释IA 3的逻辑（否则无法编码在分析规则中，见脚注6），而且还使其有可能扩展本理论，以便覆盖基于例如半德摩根代数[15]或甚至一般格[5，13]的粗糙代数的较弱版本，这将解释粗糙概念逻辑的证明理论方面。更一般地说，由于多类型方法，粗糙代数的逻辑已经被嵌入到更广泛的逻辑环境中，这些逻辑是可以正确显示的。将可适当显示的逻辑作为一个类来研究，并对大子类统一给出了语义割消去、有限嵌入性、有限模型性质等元理论结果此外，适当可显示逻辑的证明论环境的模块性使得不同逻辑以系统的方式相互作用成为可能，从而获得例如基于粗糙代数逻辑的动态认知逻辑这开辟了新的有趣的可能性，以丰富理论的逻辑粗糙代数。2预赛2.1粗糙代数定义2.1（参见第2节[26]）T=（L，I）是拓扑拟布尔代数（tqBa）如果L=（L，λ，T，λ）是一个De Morgan代数且对所有a，b∈L，T1 I（ab）=IaIb，T2. IIa=Ia，T3。 Ia≤a，T4。 IT=T。对于任何a∈T，令Ca：=<$I<$a。我们考虑tqBas的子类，定义如下表所示。IA1tqBatqBa5IA2IA3预粗粗糙粗糙代数是完备的、完全分配的准粗糙代数。引理2.2任何tqBaT=（L，k，k，k，I，T，k）满足以下等式：(i) I（Ia <$Ib）= Ia <$Ib（ii）C（Ca <$Cb）= Ca <$Cb。证据（ i）I（Ia <$Ib）≤ Ia <$Ib是T 3 的直接结果。至于代数缩略词公理拓扑拟布尔代数5tqBa5T5：CIa=Ia1型中间代数IA1T5，T6：Ia，Ia=T2型中间代数IA2T5、T7：Ia=Ib=I（a=b）3型中间代数IA3T5、T8：Ia≤Ib和Ca≤Cb表示a≤b准粗代数PRAT5 T6 T7 T8104G. Greco等人/理论计算机科学电子笔记344（2019）101我相反方向，足以证明Ia≤I（Ia<$Ib）和Ib≤I（Ia<$Ib）。让我们来说明这些不等式中的第一个。从T1开始，它立即遵循单调性。因此Ia≤Ia <$Ib意味着IIa≤I（Ia<$Ib）。因此，到T2时，Ia≤IIa≤I（Ia<$Ib）。类似地，我们证明Ib≤I（Ia<$Ib）。（2）证明是双重的。□下面，我们使用“黑板粗体”中写的代数的缩写名称（例如TQBA等）。以指示其对应的类。当它是unam-bixel时，我们将使用粗糙代数作为这些类的通用名称2.2粗糙代数确定一个命题变量的可数集Atprop，设p表示Atprop中的一个元素。粗糙代数的逻辑共享语言L，其递归定义如下：A：：= p|不|⊥|欧阿|IA|CA|AA|一辆皮卡。定义2.3TQBA类的逻辑H.TQBA是通过将下列公理添加到德摩根逻辑来定义的：IAkA，IAkIIA，I（AB）kIAIB，IAIBkI（AB），T kITCAk <$I<$A，<$I <$AkCA，<$C<$AkIA，IAk <$C<$A.我们考虑H.TQBA的以下扩展，其对应于上文报告的TQBA代数类逻辑名称公理/规则TQBA5H.TQBA51：CIAkIAIA1H.IA11、2： T kIAIA2H.IA21，3：I（AB）kIAIBIA3H.IA3IAkIB CAkCB1、4：AkBPRAH.PRA一、二、三、四令H表示上表中的任何逻辑（第二列），A表示上表中相应的代数类（第一列，与H相同的行定理2.4（完备性）H关于A是可靠的和完备的，如果AkB是L-半群，则AkB在H i∈h（A）≤h（B）中可导，对所有T ∈ A和每个解释h：L→ T.3走向多类型的列报：代数分析在这一节中，我们等价地将粗糙代数表示为异质代数。3.1粗糙代数对于任何tqBa T（参见定义2.1），我们令Ki：={Ia|a∈ L}和KC：={Ca|a∈ L}，设i：L →KI和γ：L →KC分别由赋值a<$→Ia和a<$→Ca定义。设eI：KI <$→L和eC：KC <$→L表示自然嵌入。公理T1、T2和T3意味着I：L→ L是内部算子，C：L→LG. Greco等人/理论计算机科学电子笔记344（2019）101105∈∈是L上的闭包算子，可看作偏序集。 因此，通过一般的秩序理论的事实（cf。[7，第7章]），eI（resp.左（左），右（右）。右）的伴随（相应地）γ），用符号表示：eIci和γceC，即对于任何α∈ KI，γ∈ KC和a∈L，eIα≤ai α≤ iaγ ≤ai≤eC a.（一）下面的等式是映射和（1）的定义的直接结果：i（eIα）=αeI（ia）=Iaγ（eCα）=αeC（γa）=Ca。（二）定义3.1对于任何tqBa T =（L，k，k，I，k，T，k），左核KI=（KI，1I，0I）和右核KC=（KC，1C，0C）使得对所有α，β∈KI和所有，χ∈KC，K1 αβ：= i（e Iα）e Iβ） K3。1 I：= iTKJ1. ξ п χ := γ(e C ξ ∨ e C χ)KJ3.1C：=γTK2 α β：= i（e Iαe Iβ）K4。0 I：= 1KJ2. [ 001 pdf 1st-31files][001 pdf 1st-31files][001 PDF 1ST-31FILES] 0C=γ如果T是tqBa 5，我们通过下面的等式：K5定义：K I→K I和−：K C→K C。α：= i <$e I αK J5. − ε：= γ <$e C ε下一个引理通过它们的连接映射的属性捕获tqBa和它的内核之间的关系：引理3.2对于任何tqBaT，1. i：T-KI和γ：T-KC是满足下列方程的满射a，b∈L，(a) IaIb=I（ab），I T=1I，IT=0I;(b) γ a <$γ b = γ（a <$b），γT= 1 C，γT = 0 C。2. eI：KI→ T和eC：KC→ T是满足以下方程的内射映射：(a) eIαeIβ=eI（αβ），eIαeIβ=eI（αβ）;(b) eCeCx=eC（x），eCeCx=eC（x）;(c) e I1 I= T，e I0 I= T，e C1 C= T，e C0 C= T。证据我们只证明了1（a）和2（a），1（b）和2（b）的论证是对偶的。利用K3，K4，Kj 3，KJ4和T的定义，可以很容易地得出2（c）中的恒等式。i的满射性是KI定义的直接结果（参见第3.1节开始）。在下面的例子中，我们证明了i满足1（a）。Ia Ib=I（eIae Ib）K2=i（Ia <$Ib）（2）=iI（ab）T1=ie i（ab）（2）=i（ab）（2）1（a）中其余恒等式可以用K3和K4类似地表示。 让我们证明eI满足2（a）和2（c）。 对于任何α，β K I，让a，bL使得α=1a且β=1b。106G. Greco等人/理论计算机科学电子笔记344（2019）101C我□接下来的命题和引理提供了一个命题3.3如果T是tqBa 5，则K I≠ K C。证据 设f：KI→KC定义为f：=γeI。 为了证明f是满射的，令对于某个a∈L，设k∈KC，k= γa，γa=γeC γa附加=γCa（2）=γICaT5=γeIieC γa（2）=γeI ieC（= γa）=feeC（f：=γeI）由于γ和eI都是单调的，所以f：=γeI也是单调的。 为了完成证明，我们需要证明对所有α，β∈KI，如果γeI（α）≤γeI（β），则α≤ β。由于eC是一个序嵌入，所以这个假设可以等价地改写为eCγeI（α）≤eCγeI（β），设a，b∈L使得α= ιa，β=ιb。然后我们可以等价地将假设重写为eCγe I I Ia≤eC γe II Ib。由于I：=eIi和C：=eCγ，我们可以再次等效地将假设重写为CIa≤CIb，因此，到T5时，可以重写为Ia≤Ib，即eIia≤eI ib。由于eI是一个序嵌入，这就产生了ιa≤ ιb，即α≤ β。这就完成了KI和 KC是格的证明。最后，我们需要证明f（<$α）=−f（α），对任何α∈KI。对于这样的α，设a∈Ls. t. a= i（a）。fα=γeI α=γe Ia–=γ <$eCγeI α=γ <$eγe ιa=γeI<$eI <$a=γeI<$Ia=γI<$Ia=γIC<$a=γC<$a=γ <$CeIιa=γ <$CIa=γI<$Ia=γIC<$a=γC<$a□通过上面的命题，我们可以去掉KI（或KC）以及eI和eC中的下标，并将K称为T的核下面的引理有一个简单的证明，使用K5：引理3.4（1）如果T是tqBa 5，则e∈ α=<$e α;（2）如果T是IA 1，则i（ab）= i ai b。命题3.5如果T是tqBa 5，则K是De Morgan代数。 此外，如果T是IA1，则K是布尔代数。证据 对任意α，β ∈ KI，设a，b ∈ L，使得α = ι a，β = ι b. 让我们证明，∼∼α= α and∼(α∪ β)=∼α∩∼β.e（αβ）=e（ιaιb）=ei（eiaeib）=I（Ia<$Ib）（α= ιa，β=ιb）K2（2）e（α<$ β）===e（ιa ιb）ei（eia<$ eib）I（Ia<$Ib）（α=ιa，β=ιb）通过K1（二）=IIa<$IIbT1=IaIb推论2.2=IaIbT2=埃布（二）=eiaeib（二）=eαe β（α= ιa，β=ιb）G. Greco等人/理论计算机科学电子笔记344（2019）101107⊥∼∼ ¬ ¬ T ¬ T∼∼α=我爱你K5（α=e（αK5=我爱我爱（一）=i<$e i（eαe β）K1=ι¬I¬Ia（二）=e i（e i a（α= ιa，β=ιb）=ιCiaC=<$I<$=I（Ia）（二）=天一T5=（Ia）引理2.2=伊埃埃阿（二）=I（<$Ia<$Ib）L的定义=伊阿（二）=i（C<$a<$C<$b）C=<$I <$和L=α（一）=i（IC<$a<$IC<$b）T5，C=<$I <$和L=i（I<$Ia<$I<$Ib）C=<$I <$和L=i（e<$eiae< $eib）（二）=i（e<$eαe <$eβ）（α=i（a），β=i（b））=ι（eαe β）K5=∼α ∩∼βK2利用K5，K3，（2）和T7，可以证明恒等式1I= Ie 1I= Ie i= II. 0I= 1I的论证可以对偶给出。因此，K1是一个德摩根代数。如果T是IA 1，为了证明KI是布尔代数，我们只需要证明<$α<$α = 1I。∼α ∪α=eααK5=i（ei <$eα<$eα）K1=i（e<$eiaeia）（一）=i（I<$IaIa）（二）=i（<$CIaIa）C=<$I<$=i（<$Ia<$Ia）T5=TT6=1IK33.2非均匀粗糙代数□在本小节中，我们证明了我们已经证明的粗糙代数、它们的核和连接映射的性质产生了粗糙代数定义3.6异构tqBa（htqBa）是元组H=（D，LI，LC，eI，eC，i，γ）使得：H 1 D=（D，n，n，n，n，T，n）是一个De Morgan代数;H2 LI=（LI，0I，1I）和LC=（LC，−，0C，1C）是有界分配格，H3eI：LI <$→D和eC：LC <$→D是格同态;H41：D→L1和γ：D→ L1C满足以下恒等式：I（ab）=Ia ibIT=1 I= 0 γ（ab）=γa γbγT= 1 γ= 0; H5eIci γceCieI a= α γeC= 0;3H6eC γa=<$eI I<$a。ιγLIEIDeCLC对应于2.1节中考虑的tqBas的子类的异质代数定义如下：KK108G. Greco等人/理论计算机科学电子笔记344（2019）1013条件H5意味着 i是满射，e是内射。G. Greco等人/理论计算机科学电子笔记344（2019）101109代数缩写条件异质tqBa5htqBa5H7：LI=LC=L是一个德摩根代数，eI=eC=e是一个德摩根同态异源IA1hIA1H7，H8：L是布尔代数异源IA2免疫球蛋白A2H7、H9：i（ab）= iaib异源IA3hIA3H7、H10：ιa≤ι b和γa≤γ b意味 a≤b非均质praHPRAH7、H8、H9、H10在下面的内容中，我们使用以“黑板粗体”书写的异质代数的缩写名称（例如HTQBA等）。以指示其对应的类。 一个异质代数H是完美的，如果在签名中的每个格约简H是完美的，4和每一个连接（分别）。（meet）保存（resp.在H的签名中的反向）映射是完全连接（分别地，（meet）保存（resp.反转）。定义3.7如果T=（L，I）是tqBa，我们令T+：=（L，KI，KC，eI，eC，i，γ），其中：· KI和KC是T的左核和右核（参见定义3.1）;· eI：KI <$→L和eC：KC <$→L被定义为KI的域的嵌入和KC到L的域中;· i：L→KI和γ：L→KC分别定义为i（a）= Ia和γ（a）= Ca。如果T=（L，I）是一个tqBa 5，则KI和KC可以被识别，eI和eC也可以，因此我们写T+：=（L，K，e，i，γ）。定义3.8如果H=（D，LI，LC，eI，eC，i，γ）是一个htqBa，我们令H+：=（D，I，C），其中D上的一元运算I和C由赋值a<$→eIia定义，a<$→eCγa。设A表示一类粗糙代数（cf. 2.1节），以及HA它的相应的异质代数类。提案3.9（i）若T∈ A，则 T+∈ HA;(ii) 若H∈ HA，则 H+∈ A;(iii) T（T+）+和H（H+）+。3.3异质代数的典范扩张正如采用多类型方法的其他文件所讨论的那样（参见第10段）。例如[15，19]），多类型环境中的规范性既为基本逻辑的分析扩展（即通过添加分析归纳公理获得的扩展）提供完整的语义，又证明其相关显示的保守性结石 在下文中，我们令Dδ，Lδ和Lδ表示的典型扩展I C代数D，LI和LC分别，eδ，eδ，ιπ和γπ表示扩张关于E，EI C、i和γ。5I C4.分配格是完美的，如果它是完全的，完全分配的，并且是由它的完全并素元素的集合完全并生成的。5e I，e C，i和γ的序论性质保证了它们是光滑的，也就是说，对于它们中的每一个，σ-扩张和π-扩张一致。然而，上标中的不同符号是为了强调，尽管嵌入的平滑性在规范性证明中使用，但它并不是必需的。在π和γ σ的情况下。110G. Greco等人/理论计算机科学电子笔记344（2019）101∈e∈ ∈ {}定义3.10如果H =（D，L I，L C，e I，e C，i，γ）HA是htqBa，则H的标准扩张是异质代数H δ=（D δ，K δ，K δ，e δ，eδ，i π，γ σ）。IC我C定义3.6的异质代数的定义条件可以表示为解析归纳不等式（参见：定义4.3），而每一个这样的不平等都是典型的。因此：命题3.11如果H ∈ HA，则H δ是HA的完全元。ιπγσLIδDδLCδδ δI C联系我们ιγLIEIDeCLC图1.一、 非均匀代数的标准扩张在第6.1节中，每个多类型演算的可靠性将被证明w.r.t.完美类型为.4异构粗糙代数的多类型语言异构代数为以下多类型语言LMT提供了自然的解释，该语言由类型D、KI和KC的项组成（核类型否定适用于H.TQBA5及其扩展的语言D3 A：：= p |βI α |C|不|⊥|AA |AA|欧阿K I3 α：：= ■IA |1我|0 I|α∪α |α∩α |αK C3 |1 C|0 ℃|ξ п ξ |ξ п ξ |−ξ逻辑H.TQBA5也可以用由如上所述的两个类型D和如下所述的K组成的更简单的语言来捕获：K3 α：：= ■IA|公司简介|1 |0 |∼α|α∪α |αα4.1解析归纳LMT-不等式在本节中，我们专门定义了解析归纳不等式（cf。[17，定义55]）到多类型语言LMT。这个定义也适用于解释它的htqBas代数语言，因此我们将讨论分析归纳项不等式。我们将使用以下辅助定义：n上的序型N是n元组z1，图1。 对于每种订单类型z，我们用z表示它的反序类型，即z（i）=1 i z（i）= ， 对 于 每 个1≤i≤n 。 上 述 语 言 的 连 接 词 分 为 以 下 家 族 F ：=FD<$FMT<$FKI<$FKC和G：=GD<$GMT <$GKI<$GKC：KKKKKKeG. Greco等人/理论计算机科学电子笔记344（2019）101111∗SJS∗ ∗∈{−}FD：={T，，<$} FKI：={1I，，<$} GD：={，，<$} GKI：={0I，，<$}FMT：={◆I，◆C，I，C} FKC：={1C，，−} GMT：={■I，■C，I，C} GKC：={0C，，−}对于任意的f∈F（resp. g∈G），我们令nf∈N（分别为. ng∈N）表示f（resp. g）和序型zf（resp.zg）onnf（resp. ng）表明是否f的第i个坐标（分别为g）是正的（zf（i）=1，zg（i）=1）或负的（zf（i）=1，zg（i）=1）。这种分组的序理论动机是F-连接词的代数解释（分别是：G-连接词）保持有限连接（分别为在每一个正坐标和反向有限满足（分别）。在每个负坐标中。 对于任何项s（p1，. pn），n上的任意阶型z，且任意1≤i≤n，s的有符号生成树中的z-临界节点是叶节点+pi且z（i）=1或−pi且z（i）=1。 树中的z临界分支是以z临界节点。对于任何项s（p1，. p n）和n上的任何阶型z，我们说+s（resp.−s）与z一致，并写z（+s）（resp. z（-s）），如果+s（resp. -s）是z临界的。我们还将编写+sjs（resp.−sJs）来指示子项sJ继承正的（相应地，负）符号。最后，我们将写z（sJ）s（resp.z（sJ）s）来表示有符号子树，继承自，同意z（resp. z）。定义4.1[有符号的生成树] 负）生成树的定义，通过标记的根节点的生成树的s与符号+（resp.−），然后在每个剩余的节点上传播标签如下：对于任何标记为4∈F <$G且arity n4≥ 1的节点，以及对于任何1 ≤i≤n4，分配相同的（分别为相反）符号到其第i个子节点如果z4（i）=1（分别如果z4（i）=0）。有符号生成树中的节点是正的（分别为 负的），如果是有符号的+（相应地，−）。定 义 4.2[ 好 分 支 ]有 符号 生成 树 中的 节点 被称 为 Δ- 伴 随、 语 法左 残差（SLR）、语法右残差（SRR）和语法右伴随（SRA），根据表1中给出的规范。一个有符号生成树s中的分支，如果它是两条路径P1和P2的级联，其中一条路径的长度可能为0，使得P1是来自叶子的路径，该叶子（除了变量节点）仅由PIA节点组成（对于术语的解释，我们参考[23，注释3.24]），并且P2（除了变量节点）仅由PIA节点组成。骨架PiaΔ-adjoints+⎪⎩⎧−∨∧∪∩电子邮件0I1我0℃1CSRA中国+⎧⎪⎩−电子邮件0 I0 ℃1我1C∧ ∩ п ◦ I简体中文¬ ∼−∨ ∪ п ◦ IC◆ C¬ ∼−单反相机+⎪⎩−不⊥1我0I1C0℃∧∨∩∪п ◦I ◦C ◆C ¬ ∼− п◦I ◦C■C ¬ ∼−公司简介⎪⎩−∨∧∪ п∩ п+骨架≤−骨架Pia+ps1+ps2Pia112G. Greco等人/理论计算机科学电子笔记344（2019）101–≤定义4.3 [解析归纳不等式，参见[17，定义55]]对任意序型z和任意p 1上的任意自同构传递关系<Ω，. pn，项s（p1，.pn）是解析（Ω，z）-归纳的，如果(i) 每一个分支都是好的（参见）。定义4.2）;(ii) 对于所有1 ≤ i ≤ n，在具有叶p i的任何z临界分支中出现的每个m元SRR节点具有S（s1，...，s j−1，β，s j+1.，s m），其中对于任何h ∈ {1，.，m}\j：(a) z（sh）s（cf. 定义4.2之前的讨论），以及(b) p k<Ωpi，对于每个p k出现在s h中且对于每个1≤k≤ n。一个不等式st是解析（Ω，z）-归纳的，如果符号生成树+s和t是解析（Ω，z）-归纳的.一个不等式st是解析归纳的，如果对某个Ω和z是解析（Ω，z）-归纳的.在每一种定义它们的环境中，解析归纳不等式都是归纳不等式的一个子类（参见：[17]）。反过来，归纳不等式是规范的（也就是说，在规范扩张下保持不变，就像在每个设置中定义的那样，参见。[6]）。因此，下面是归纳不等式的一般规范性的直接结果定理4.4解析归纳LMT-不等式是标准的.4.2粗糙代数的原始语言到多型语言的单型代数与其对应的异质代数之间的切换通过平移（·）t：L →LMT在系统上反映，定义如下：pt=pt= Tt =T（<$A）t=<$At（AB）t=AtBt（AB）t=AtBt （IA）t=C■IAt （CA）t=I◆CAt回想一下，T+表示与给定代数相关联的异质代数T（cf.定义3.7）。下面的命题是由一个常规归纳法证明的关于L-公式。命题4.5对于所有的L-公式 A和 B和每个L-代数T， 不|=A ≤B我的T +|=A t≤ B t。我们现在能够把2.2节中定义的任何逻辑H的公理和规则翻译成LMT。G. Greco等人/理论计算机科学电子笔记344（2019）101113∧ ≤ ∨IAk我我我我C cCC~eII Ia≤eI I Ib和eC γa≤eC γb意味着a≤b（x）由于eI和eC是序嵌入，eIi（a）≤eIi（b）和eCγ（a）≤eCγ（b）分别等价于i（a）≤i（b）和γ（a）≤γ（b），因此拟不等式(x)可以等价地重写为下面的拟不等式，它定义了类HIA3：i（a）≤i（b）和γ（a）≤γ（b）意味着a≤b。通过附加，前件中的不等式可以等价地改写为a=eC（γ（b））<$a和b=b<$eI（i（a））.因此，初始的拟不等式可以等价地重写为以下的L-MT-不等式：a≤eCγ（b）≤eIi（a）≤b。（三）上面的不等式是解析归纳的，因此它可以与其他异质代数公理一起使用，如3.3节所述，这些公理是解析归纳的，以生成所引入的演算的解析结构规则。在第5节中，使用类似于[17]中介绍的方法。 正如我们将在6.2节中讨论的，不等式（i）-（ix）可以用这种方法得到的适当演算导出。5粗糙代数逻辑的真显示演算在本节中，我们为与第2.1节中提到的每类代数A相关联的逻辑引入适当的多类型显示演算D. A。语言这 些 演算有D、KI和KC类型，由结构和操作（也称为逻辑）连接词组成。在异质代数中，异质连接词<$I，<$C，■I，<$C分别表示为eI，eC，i，γ.每一个结构连接词都是通过用符号（分别）装饰其相应的逻辑连接词来表示的。 或）。下面，我们采用一元连接词比二元连接词更强的约定。5.1语言• 结构和操作术语：6请注意，在单类型环境中应用类似的步骤将导致不等式一CpCBB IbIB（其中Cp和Ib分别表示C的右伴随和I的左伴随）是归纳的但不是解析的。原始语言翻译解释IAkA~I■IAkA~eIιa≤a（一）T kI T~T kI■IT~T≤eIT（二）I（AB）kIAB~I■I（AB）kI■IAI■IB~eIi（ab）≤eIiaeIib（三）其他事项I（AB）~I■IAI■IBkI■I（AB）~eII Iae IIIb≤e I II（ab）（四）IA kIIA~I■IAkI■II■IA~eIιa≤eIιeIιa（五）中情局 kIA~C<$CI■IAkI■IA~eCγeIιa≤eIιa（六）I（AB）kIAB~I■I（AB）kI■IAI■IB~eIi（ab）≤eIiaeIib（七）I（AB）~I■IAI■IBkI■I（AB）~eII Iae IIIb≤e I II（ab）（八）114G. Greco等人/理论计算机科学电子笔记344（2019）101中文（简体）|1|0|ξпξ|ξпξ|（−K）KCQC⎪⎨Kα：：=■IA|1我|0I|α ∩α |α ∪α|（α）I⎧⎪⎩DA：：= p|不|⊥|βI α |C|欧阿|AA |AA⎪⎩X::=A|⊥ˇ|T|◦˜CΠ|◦˜ IΓ |¬˜X|XX|XX|X>X|X→XΓ：：=α|■IX|◆IX|0分|1美元|Γ ∩ˆΓ |Γ ∪ˇΓ |Γ ⊃ˆΓ |Γ ˇ⊃Γ|（中文）CCC：：=|公司简介|■■CX|0℃|1摄氏度|ΠпˆΠ|ΠпˇΠ|ΠˇhΠ|ΠhˆΠ|（−）上表中括号中的公式和结构属于D.TQBA5及其扩展的语言。• 结构连接词作为逻辑对应词的解释(i) 结构和操作纯D型联结词：结构上的作业T⊥ˇ∧ˆ∨ˇ¬˜公司简介→ˇ逻辑操作不⊥∧∨¬（>）（→）(ii) 结构和操作纯KI型和KC型连接词：结构上的作业1美元0分∩ˆ∪ˇ⊃ˆˇ⊃1摄氏度0℃пˆпˇ拉克什h逻辑操作1我0I∩∪（）（）1C0℃пп（h）（h）(iii) 如上所述，D.TQBA5及其扩展语言包括以下结构和操作纯KI型和KC型连接词：结构上的作业∼˜−˜逻辑操作∼−(iv) 结构和操作的多类型连接词，以及它们的代数对应部分：类型D →KID →KCKI→ DKC→ D结构上的作业中文（简体）■公司简介公司简介◦˜ I公司简介逻辑操作（◆一）■一◆C（■C）IC代数对应物伊日ιπγσγJeδ我eδC5.2规则在下文中，我们将使用X、Y、W、Z作为结构D-变量，使用Γ、Δ、Λ作为结构KI-变量，并且使用λ、λ、Ω作为结构KC-变量。适当的多类型显示演算D.TQBA包括以下公理和规则：8• 身份和切割：IDX k AAkY切割Γkα αk Δ割Πkξ ξk Σ切割KDpk pXkYDKIΓk Δ克雷奇• 纯D型显示规则：ResDXXXYkZYkX→ZXkYZ resDY>XkZgalD<$XkY¬˜YkXXkuoYgalDYX• 纯KI型和KC型显示规则：K分辨率τΔkΛΓkΔΛresKK分辨率联系我们ΠkΣпˇΩresKIΔk<$Λ• 多类型显示规则：我ΔkΛCkhΩCΣhˆΠkΩ7在概要表中，只在结构一级出现的操作符号将出现在圆括号之间。[8]为了简洁起见，我们采用这样的约定：规则名称的位置--在推理线的左边或右边--与正确识别每个给定规则有G. Greco等人/理论计算机科学电子笔记344（2019）101115关。 例如，名称每个逻辑规则的“”被放置在推理线的右边或左边，这取决于给定的规则是右引入规则还是左引入规则。 一些结构化规则具有双推理线，这意味着规则是两个规则的缩写（一个自上而下阅读，另一个自下而上阅读）。 在这种情况下，我们对两个规则使用同一个名称116G. Greco等人/理论计算机科学电子笔记344（2019）101⊥我我我◆ˆ广告YkIΓadadYk◦˜CXkΠadDKIY◆IYkrDKIDKC公司简介YkXk■CDKC• 纯型结构规则：这些规则包括每种类型中的标准弱化（W ），收缩（C），交换性（E）和结合性（A）。 我们不报道他们。 9XkYcont<$Yk<$XXkYXXkYXkY1kΔ我Γ ∩ˆ1ˆ IkΔ<$kΔ0<$<$kΔ<$$>0<$ I1ˆ 克雷奇CΠпˆ1ˆCkΣk• 多类型结构规则：◦˜1ˆ杜伊ˆk■中文（简体）我◆ˆTCTkXk0ˇ我我◦˜I1IkYk0C1CkC CXkC0C˜◦˜ IΓ k◦˜ IΔΓk Δ◦˜CΠk◦˜CΣΠkΣ公司简介公司简介◆CXk■ CYXkY◆IXk■IYXkYI■ICXkI■Y XC<$CYXkC■C<$YICX<$k I<$IYCIC<$C<$XkY¬˜◦˜I■ˇIXkY◦˜I◆ˆI¬˜XkYCI¬˜◦˜C■ˇCXkY• 逻辑规则：纯类型连接词的规则是标准的，可以省略;多类型连接词的规则：◆◆IAkr我◆IA KI<$kA<$I◆k◆AIαkX◦ IαkX■ 我Ak r■ IAk■Ir<$k ■A■IIACCkX◦ CkX◆公司简介公司简介Xk IαI■AkA■CXkCCC◆CAk公司简介C公司简介XkIαC■CAk■CCAXkC通过将以下规则添加到D.TQBA来获得演算D. TQBA 5• 显示规则：半乳糖K∼˜ΓkΔΓkΔ半乳糖K半乳糖K-克什克-克什克半乳糖K∼˜ΔkΓΔk∼˜Γ-克什克-克什克• 纯KI型和KC型结构规则：IΓkΔ∼˜Δk∼˜Γ克雷奇−阿罗克−阿罗克• 多类型结构规则：XkI■IY我XkC■CY• 和−的逻辑规则：■XkIX IΓ◦˜ I∼˜XkC−XkC◦˜C−˜∼˜αkΓαkΓΓkαΓkα−αk–克什克-克什克克-什第2.2节中讨论的H.TQBA5的公理扩展的正确显示演算是通过添加下表为微积分D.TQBA5。逻辑名称显示微积分规则H.IA1D.IA1cgr i<$Δk<$kΩcgr iΔk<$$><$k−<$$><$ΩH.IA2D.IA2◆Y）kY）公司简介◆ˆ ˆ ˇ X轴IY中文（简体）CX<$CYk<$k■I■H.IA3D.IA3XkY WkZia3XC<$CWkI■IYZ不◦◦◦∼∼−−我C◦公司简介我我CC˜G. Greco等人/理论计算机科学电子笔记344（2019）101117H.PRAD.PRAcg r i，◆C，■I，ia3.9在下文中，我们使用下标（表示类型）来区分不同类型规则中的格算子规则。118G. Greco等人/理论计算机科学电子笔记344（2019）101KK6性能在本节中，我们让H表示2.2节中定义的任何逻辑;设 A和HA分别表示其对应的单型和异质代数类，D. A表示H的显示演算. 真实的，每个D.A.的性质非常接近于使用多类型结石的一般方法设计的其他结石的类似性质的性质（参见例如[19、15、18、16]）。因此，我们只画了草图。6.1完全HA代数在本节中，我们概述了D.A.w.t.规则的合理性的验证。HA的完美元素的语义（见定义3.6）。第一步是根据结构符号的位置（前序或后序）将结构符号解释为逻辑符号，如本节开头所示。五、这使得有可能把数列解释为不等式，把规则解释为拟不等式.例如，下面左手边的规则被解释为右手边的准不等式：XkY WkZia3XC◆CWk I■IYZ~<$a<$b<$c <$d[（a ≤ c &b ≤ d）<$a<$e C γ（b）≤ e Ii（c）<$d]。因此，对D. A规则的合理性的验证在于验证它们相应的拟不等式在HA的任意完美元中的有效性。 纯型规则和引入规则的可靠性的验证遵循这个过程是例行的，并且被省略。 上面的规则ia3的可靠性通过下面的ALBA-约化来验证，它表明上面的准不等式等价于不等式（3），如第4节所讨论的，它对每个H ∈HIA 3都有效。p<$q[p<$eCγ（q）≤eIi（p）<$q]i <$p<$q<$a<$b<$c<$d[（a≤pb≤qp≤cq≤d）<$a<$eCγ（b）≤eIi（c）<$d]ia bcd [（a ≤ c &b ≤ d）a eC γ（b）≤ eI i（c）d].对应于其余结构规则的准不等式的有效性以类似的方式遵循。6.2完整性设AτkBτ是任何L-代数AkB到D. A语言的翻译，它构成了第4节中介绍的翻译，以及5.1节表（iv）中指出的代数运算和逻辑连接词之间的对应关系。命题6.1对于每个H-可导的A B，AτBτ在D. A中可导。T7◆我们只给出了规则T8、公理T6和公理的一个方向的推导T8IAkIB和CAkCB表示AkB~<$I ■IAk <$I■IB和<$C<$CAk <$CCB隐含AkBG. Greco等人/理论计算机科学电子笔记344（2019）101119I∨◦IKKKL|KA B我 I（A）ckIIAI■I◦ C◆CA kC ◆CBId D+◆C +切割C+切割D◦˜C◆ˆCAk◦˜C◆CB◦ I■IAkI■IB IdD+■I+I+切割D˜