Intermediate logics and factors of the Medvedev lattice
Andrea Sorbi, Sebastiaan A. Terwijn
我们将Medvedev格的初始段看作Brouwer代数，并研究了与之相关的命题逻辑。
We investigate the initial segments of the Medvedev lattice as Brouwer algebras, and study the propositional logics connected to them.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
First-order logic in the Medvedev lattice
柯尔莫哥洛夫引入了一种非正式的演算问题，试图为直觉主义逻辑提供一种经典的语义。这后来被梅德韦杰夫和穆奇尼克正式定义为梅德韦杰夫和穆奇尼克晶格。然而，他们只是形式化的命题逻辑，而哥洛夫还讨论了全称量词。我们扩展梅德韦杰夫的工作，一阶逻辑使用的概念，一阶hyperdoctrine从范畴逻辑的结构，我们将呼吁梅德韦杰夫hyperdoctrine。我们还研究了中间的逻辑，梅德韦杰夫hyperdoctrine给我们，在那里我们特别关注的子区间的梅德韦杰夫hyperdoctrine，试图获得一个类似的Skvortsova的结果，有一个因素的梅德韦杰夫格特征直观命题逻辑。最后，我们考虑海廷算术在梅德韦杰夫hyperdoctrine和证明类似的Tennenbaum定理的可计算模型的算术。
The Logics of Individual Medvedev Frames
本文研究基于大小为 n 的集合的非空子集的 n-梅德韦杰夫框架，通过极大点性质给出统一公理化，并比较其与梅德韦杰夫逻辑在紧致性、析取性质及结构完全性方面的异同。
Levin's and Prucnal's theorems on Medvedev's logic of finite problems
本文统一重述关于 Medvedev 有限问题逻辑的 Prucnal 结构完全性定理与 Levin 最大扩张定理，借助共同引理简化证明。
An Intermediate Logic Contained in Medvedev's Logic with Disjunction Property
本文定义并研究中间逻辑 SU，刻画其在 S4 框架上的“强并”性质，证明强完全性与析取性质，使其成为 Medvedev 逻辑之下兼具公理化和析取性质的最强已知逻辑。
Natural Factors of the Medvedev Lattice Capturing IPC
Skvortsova表明，有一个因素的梅德韦杰夫格捕捉直觉命题逻辑（IPC）。然而，她的因素是不自然的，因为它是以一种特别的方式构建的。我们提出了一个更自然的例子，这样一个因素。我们还证明，对于梅德韦杰夫格的每个非平凡因子，其理论都包含在扬科夫逻辑、IPC的演绎闭包加上弱排中律中。这回答了Sorbi和Terwijn的一个问题。
Medvedev logic is undecidable
本文通过将周期性平铺问题归约到非定理性，证明了Medvedev逻辑不可判定，并类似地证明了Skvortsov逻辑的不可判定性及两者的区别，解决了一个长期开放问题。
Medvedev Logic is Not Decidable. It is π01 -complete. Who Would Have Guessed?
本研究证明Medvedev逻辑ML在可计算多一归约下是π₀¹完全的，从而不可判定且非递归可枚举；通过构造Wang-Medvedev对，将周期性平铺与直觉主义公式反模型联系起来，给出证明。
Intuitionistic Logic and Muchnik Degrees
我们证明，有一个因素的Muchnik格，捕捉直觉命题逻辑。这补充了现在经典的结果Skvortsova梅德韦杰夫格。
On Intermediate Justification Logics
我们研究抽象的中间证明逻辑，即任意的中间命题逻辑扩展的（经典）证明逻辑的特定公理的子集。对于这些，我们介绍了各种语义相结合，无论是海廷代数或Kripke框架与通常的语义机器所使用的Mkrtychev的，拟合的或莱曼的和Studer的模型为经典的理由逻辑。我们证明了统一的完整性定理，所有中间的理由逻辑和相应的语义使用相应的命题完整性定理的基础中间逻辑。进一步，通过对Fitting方法的改进，我们证明了一大类中间证明逻辑和伴随的中间模态逻辑的统一实现定理。
Lyndon interpolation property for extensions of $\mathbf{S4}$ and intermediate propositional logics
该研究针对S4扩展逻辑及中间命题逻辑，分析Lyndon插值性质（LIP）与一致Lyndon插值性质（ULIP），明确18个有限高度S4正规扩展逻辑的LIP成立情况，并证明中间命题逻辑中三类插值性质等价。
Epsilon Theorems in Intermediate Logics
任何中间命题逻辑（即，包括直觉主义逻辑并包含在经典逻辑中的逻辑）可以被扩展到具有π-和τ-算子以及临界公式的微积分。对于经典逻辑，这导致希尔伯特的$\varepsilon$ -演算。经典逻辑的第一和第二$\varepsilon$ -定理建立了$\varepsilon$ -演算在其经典基本逻辑上的保守性。众所周知，第二个$\varepsilon$ -定理对于直觉的$\varepsilon$ -演算是失败的，因为预解是不可能的。本文研究了添加临界$\varepsilon$ -和$τ$ -公式以及将量词翻译成$\varepsilon$ -和$τ$ -项对中间逻辑的影响。它表明，保守性的命题基础逻辑也持有这样的中间$\varepsilonτ$ -演算。“扩展的”第一$\varepsilon$ -定理在基逻辑是有限值哥德尔-达米特逻辑时成立，否则不成立，但对无限值哥德尔逻辑中的某些可证明公式成立。第二个$\varepsilon$ -定理也适用于有限值一阶哥德尔逻辑。用于证明无限值哥德尔逻辑的扩展的$\varepsilon$ -第一定理的方法建议应用于算术理论。
Intermediate logics in the setting of team semantics
最近几位作者定义了基于团队语义的直觉主义逻辑（tIPC）。在本文中，我们提供了两种替代方法，中间逻辑的团队语义设置。我们通过修改tIPC与公理写两个不同版本的析取逻辑，一个本地和全球之一。在第一种方法中，我们证明了一个特征定理，在第二种方法中，我们引入了一个广义的团队语义。
Characterizing intermediate tense logics in terms of Galois connections
我们提出了一个统一的方式来定义每个逻辑${\sf L}$之间的直觉和经典逻辑，相应的中间最小时态逻辑${\sf LK_t}$的中间。这是通过建立两个中间逻辑副本与伽罗瓦连接${\sf LGC}$的融合，然后通过两个Fischer Servi公理将它们的运算符相互连接来完成的。由此产生的系统在这里称为${\sf L2GC{+}FS}$。在直觉逻辑${\sf Int}$和经典逻辑${\sf Cl}$的情况下，注意到${\sf IK_t}$在语法上等价于W. B. Ewald和${\sf Cl2GC{+}FS}$等价于经典最小时态逻辑${\sf K_t}$。这证明将${\sf L2GC{+}FS}$视为任何中间逻辑${\sf L}$的最小${\sf L}$时态逻辑${\sf LK_t}$是合理的。本文定义H2 GC + FS-代数为E.奥洛斯卡和我。雷维茨基对于每一个中间逻辑${\sf L}$，我们证明了${\sf L2GC{+}FS}$的代数完备性及其在${\sf L}$上的保守性。我们证明了${\sf IK}$关于定义在G.菲舍尔·塞尔维我们还证明了一个表示定理，说明每个H2 GC + FS-代数可以嵌入到它的标准${\sf IK}$ -框架的复代数。
Unification types and union splittings in intermediate logics
根据Kripke模型对具有有限（或酉）统一的局部表逻辑的特征[10]，我们确定了一些中间逻辑的统一类型（{ \sf INT}的扩展）。有零元统一的极大逻辑${\mathsf L}(\mathfrak R_{2}+)$，${\mathsf L}(\mathfrak R_{2})\cap{\mathsf L}(\mathfrak F_{2})$，${\mathsf L}(\mathfrak G_{3})$和${\mathsf L}(\mathfrak G_{3}+)$正好有四个，它们是表格式的.只有两个具有遗传酉统一的最小逻辑：${\mathsf L}$（$\mathbf F_{un}$），具有遗传酉统一的最小逻辑，和${\mathsf L}$（$\mathbf F_{pr}$），具有遗传射影近似的最小逻辑;它们是局部表的。酉逻辑和非投射逻辑需要对某些可统一公式的多边形组附加变量，而具有投射近似的酉逻辑是正投射的。没有一个局部表列中间逻辑是无穷统一的。具有有限性而非遗传有限性的统一逻辑是罕见的，并且分散在大多数具有零统一的逻辑中，参见$\mathsf H_3\mathsf B_2$及其扩展的例子。
An Epistemic Interpretation of Tensor Disjunction
本文的目的是给依赖逻辑中的张量析取一个认识论的解释，通过一个相当令人惊讶的连接到所谓的弱析取在梅德韦杰夫的早期工作下的Brouwer-Heyting-Kolmogorov（BHK）解释的中间逻辑。我们在Ciardelli和Barbero（2019）讨论的具有张量析取的探究逻辑的设置中揭示了这种联系，但是从认识论的角度。更具体地说，我们按照Wang（2021）的提议，将具有张量的探究逻辑的命题公式转换为“知道如何”的强大认知语言中的模态公式。我们给出了一个完整的公理化的逻辑，我们的全语言的基础上Fine的公理化的S5模态逻辑与命题量词。最后，我们推广了带参数$k$和$n$的张量算子，它直观地描述了一个人知道$n$问题的$n$可能答案并且确信它们的$k$答案一定是正确的认识情形.原始张量析取是当$k=1$和$n=2$。我们表明，广义张量算子不增加我们的逻辑，好奇的逻辑，命题依赖逻辑的表达能力，虽然大多数这些广义张量不是统一定义的这些逻辑，除了在我们的动态认知逻辑知道如何。
Hypersequent Calculi for Intermediate Predicate Logics
我们报告的当前状态，我们正在进行的项目，以开发良好的hypererascites演算的中间谓词逻辑，如线性公理$\mathbf{LIN}\colon\left(φ\toψ\right)\lor\left(ψ\toφ\right)$和恒定域公理$\mathbf{CD}\colon\forall x\left(φ\lorψ\left(x\right)\right)\toφ\lor\forall xψ\left(x\right)$。
On Intermediate Inquisitive and Dependence Logics: An Algebraic Study
本文对中间查询逻辑和依赖逻辑进行了代数研究。虽然这些逻辑通常是使用团队语义研究，在这里，我们引入了另一种代数语义，我们证明它是完整的所有中间的好奇和依赖逻辑。为此，我们定义好奇和依赖代数，我们调查他们的模型理论的性质。我们表明，它们是基本的结构公理化霍恩句子，我们用我们的完整性结果来说明一个版本的algebraisability的好奇和依赖逻辑。然后，我们专注于有限的，核心生成的，良好连接的好奇和依赖代数：我们证明他们见证的有效性，真正的好奇代数公式，以及真正的公式连接依赖代数。最后，我们得到了有限代数、核生成代数、良连通代数、查询代数和依赖代数的表示定理，并证明了一些连接群和代数语义的结果。
Ł-Axiomatizability in intermediate and normal modal logics
一个公式集$F$相对于一个给定的逻辑类是完备的，如果这个类中的每个逻辑都可以用$F$中的公式公理化。一个公式集$F$相对于一个给定的逻辑类是完全的，如果这个类的每个逻辑都可以用来自$F$的公式来公理化，也就是说，这些逻辑中的每一个都可以由一个$Ł$ -演绎系统来定义，该系统具有来自$F$的公理和反公理以及推理规则肯定前件、否定前件、替换和反向替换.证明了相对于$\Ext\Int$（或$\Ext\KF$）的每一个完备公式集都是n-完备的.特别地，来自$\Ext\Int$（或$\Ext\KF$）的每一个逻辑都可以用Zakharyaschev的规范公式来进行公理化。
Lattices of Intermediate Theories via Ruitenburg's Theorem
对于每一个单变量公式$χ$，我们引入一个中间理论格：$χ$ -逻辑格。定义chi-logics的关键思想是将原子命题解释为公式$χ^2$的不动点，可以使用Ruitenburg定理在语法上描述。我们建立了$χ$ -逻辑格与一类特殊的Heyting代数簇之间的代数对偶。这种方法使我们能够建立五个不同的格对应的可能不动点的单变量公式|其中包括中间逻辑的负变体格。我们更详细地描述这些晶格。
Structural completeness in propositional logics of dependence
本文证明了三种主要的命题依赖逻辑（包括命题依赖逻辑和查询逻辑），它们都不是结构的，但它们关于一类替换是结构完备的，在这类替换下逻辑是闭的。我们得到了类似的结果稳定的替代，一些著名的中间逻辑，这是密切相关的中间理论，是密切相关的探究逻辑的负变体。
Topologies for intermediate logics
本文研究了在Heyting代数理论中，内部逻辑满足给定断言的Grothendieck拓扑类的特征问题，并在一个初等拓扑上为一类广泛的中间逻辑引入了双重否定拓扑和De Morgan拓扑的自然类比.
Hereditarily Structurally Complete Superintuitionistic Logics and Primitive Varieties of Heyting Algebras
本文通过代数方法证明了中间逻辑的可遗传结构完备性与Heyting代数变种的原始性之间的等价性。
Degree-preserving Godel logics with an involution: intermediate logics and (ideal) paraconsistency
本文研究了介于具有involution的度保持Goedel逻辑与经典逻辑之间的中间逻辑，并探讨了其paraconsistency特性及饱和paraconsistency的特性。
Local Tabularity is Decidable for Bi-Intermediate Logics of Trees and of Co-Trees
本文证明了判定 bi-Gödel 代数所代数化的双直觉逻辑扩张 bi-GD 的有限可公理化扩张是否具有局部表格性是可判定的，核心在于证明特定有限余树族（有限梳）的逻辑 Log(FC) 是有限可公理化且可判定的。
Multiple Conclusion Rules in Logics with the Disjunction Property
证明了对于具有析取性质的中间逻辑，任何一个可容许规则的基都可以约化为一个可容许m-规则（多结论规则）的基，并且每一个可容许m-规则的基都可以约化为一个可容许规则的基.这些结果可以推广到一个广泛的逻辑类，包括正逻辑及其扩展，Johansson逻辑，S4的正规扩张，n-传递逻辑和直觉模态逻辑。
Characteristic formulas over intermediate logics
将特征公式的概念推广到无限可表示的亚直不可约代数。证明了Heyting代数簇的连续统中含有无限个可表示的次直不可约代数。此外，我们证明了存在一个连续的中间逻辑，可以公理化的特征公式的无限代数，而它们是不可公理化的标准Jankov公式。给出了不能用无限代数的特征公式公理化的中间逻辑的例子。同时，利用Goedel-McKinsey-Tarski变换，我们将这些结果推广到了S4的内部代数和正规扩张
Translating Labels to Hypersequents for Intermediate Logics with Geometric Kripke Semantics
我们给出了一个将几何Kripke框架公理转化为Int^*/Geo中相应的中间逻辑的结构超代数规则的过程，这些中间逻辑允许弱化、收缩，在某些情况下还允许切割。我们给出了一个过程，翻译相应的逻辑标记序列的超序列，共享相同的线性模型（对应于哥德尔-达米特逻辑）。我们证明了标记证明Int^*/Geo可以被转换成hyperereremantic证明，可以使用线性规则，这对应于著名的哥德尔-达米特逻辑的通信规则。
Skolemization In Intermediate Logics
本文刻画了允许标准及Andrews Skolem化的中间一阶逻辑，并为其他逻辑开发新型Skolem函数，同时证明带量词移位公理的谓词直觉主义逻辑的Kripke框架不完全性，以促进非经典逻辑的消解式定理证明。
Bi-intermediate logics of trees and co-trees
本文研究由 Gödel-Dummett 公理公理化的双直觉主义逻辑扩张 bi-LC 的扩张格，利用 Jankov 型公式证明其恰有连续统多个扩张，并借助有限梳共树刻画了其中的局部表格扩张。
There are only countably many locally tabular bi-intermediate logics of co-trees
本文证明只存在可数多个co-trees的局部表格生物中间逻辑，所有都是有限公理化的。
De Jongh's Theorem for Intuitionistic Zermelo-Fraenkel Set Theory
证明了直觉集合论IZF的命题逻辑是直觉命题逻辑IPC。更一般地说，我们表明，IZF有德容财产方面的每一个中间的逻辑是完整的一类有限树。对于CZF也有相同的结果。
Polyhedral completeness of intermediate logics: the Nerve Criterion
我们研究了最近设计的多面体语义的中间逻辑，其中公式被解释在n维多面体。一个中间逻辑是多面体完备的，如果它关于某类多面体是完备的。本文的第一个主要结果是逻辑的多面体完备性的一个充要条件。这个条件，我们称之为神经判据，用亚历山德罗夫的偏序集神经的概念来表达。它提供了多面体完备逻辑的纯组合特征。使用神经准则，我们表明，很容易，有连续的许多中间逻辑，不是多面体完整的，但有有限的模型属性。我们还提供了，在相当大的组合劳动，一个可数无限类的逻辑公理化的扬科夫精细公式的'星形树'，所有这些都是多面体完成。这些“星形逻辑”的多面体完备性定理是本文的第二个主要结果。
Axiomatizing logics of finite Gödel-Kripke models
研究模态戈德尔逻辑对有限戈德尔-克里普克模型的完备性，发现原有逻辑不满足，并提出新的公理化方法以实现完备性。
Weihrauch goes Brouwerian
我们证明了Weihrauch格可以转化为一个Brouwer代数的连续应用程序的两个封闭运营商在适当的顺序：第一次完成，然后并行化。完备闭包算子是我们引入的一个新的闭包算子。它将任何问题转换为一个完整的问题，在完成各自的类型，我们允许任何值以外的原始域的问题。这个闭包算子本身是有趣的，因为它生成了Weihrauch约简的一个全版本，它的定义类似于Weihrauch约简的通常版本，但是是根据全实现子定义的。从逻辑的角度来看，完成可以被看作是一种使问题独立于其前提的方法。除了完备算子和全Weihrauch约简外，我们还需要研究描述这些概念所需的预完备表示。为了证明平行化的全Weihrauch格构成一个Brouwer代数，我们引入了一个新的乘法蕴涵。虽然并行化的全Weihrauch格形成了具有这种蕴涵的Brouwer代数，但全Weihrauch格在两个不同的方面不能成为直觉线性逻辑的模型。为了查明这一失败的代数原因，我们引入了Weihrauch代数的概念，使我们能够制定准确和整洁的条款失败。最后，我们证明了Medvedev Brouwer代数可以嵌入到我们的Brouwer代数中，这也意味着我们的Brouwer代数的理论是Jankov逻辑。
Nested Sequents for Intermediate Logics: The Case of Gödel-Dummett Logics
本文通过引入线性规则和可达性规则，并推广嵌套矢列以包含签名，为命题及一阶Gödel-Dummett逻辑构建了具有高度保持可逆性、可靠且无割完备的嵌套矢列系统，同时为更广泛的中间逻辑提供了无割嵌套矢列系统的构造思路。
The Intermediate Logic of Convex Polyhedra
本文研究了基于多面体的中间逻辑语义，为所有紧凸多面体类的中间逻辑 PL 提出了有限公理化，并通过提取几何约束、利用多面体几何经典结果及引入“锯齿树”的几何实现，证明了该公理化的可靠性与完备性。
Wright's Strict Finitistic Logic in the Classical Metatheory: The Propositional Case
克里斯平·赖特在他1982年的论文中主张严格有限主义，这是一种比直觉主义更具限制性的建设性观点。在附录中，他提出了严格有限算术的模型。它们是树状结构，形成于他严格的有限元理论，数字之间的方程，具体的算术句子进行评估。作为第一步，对经典形式化的严格有限性，我们提出了一个额外的假设，在经典的元理论的同行，然后提取命题的一部分，“严格有限逻辑”，从它和调查。我们将提供一个健全和完整的Kripke风格的语义和一个演算，并与其他逻辑比较。这种逻辑缺乏排中律和前件式，弱于经典逻辑，但在定理性上强于任何真正的中介逻辑。事实上，所有其他著名的经典定理都被发现是定理。最后，我们将观察到这种语义的模型可以被看作是直觉模型的节点。
On the Blok-Esakia theorem for universal classes
Blok-Esakia定理指出，存在从中间逻辑格到Grzegorczyk模态逻辑的正规扩张格的同构。Emil Jeábek作为典范规则的一个应用得到了多结论推论关系的推广。我们表明，Jeanábek的结果如下已经从布洛克的代数证明。我们还证明了强结构完备性和强泛完备性的性质被保持并反映在上述同构中。这些性质分别与单结论推论关系的结构完备性和泛完备性相一致，特别是对于逻辑。
Topological completeness of logics above S4
McKinsey和Tarski [28]的一个著名结果是：S4是任何自密可分度量空间上的闭包代数X+的逻辑。特别地，S4是实数R、有理数Q或康托空间C上的闭包代数的逻辑。根据[5]，S4以上的每个具有有限模型性质的逻辑都是Q+的子代数的逻辑，也是C+的子代数的逻辑。这对R不再成立，并且[5]的主要结果指出，S4以上的每个具有有限模型性质的连通逻辑都是闭包代数R+的子代数的逻辑。在本文中，我们将这些结果推广到所有的逻辑S4以上。也就是说，对于正规模态逻辑L，我们证明了下列条件是等价的：（i）L在S4之上，（ii）L是Q+的子代数的逻辑，（iii）L是C+的子代数的逻辑.在S4上引入了良连通逻辑的概念，并证明了以下条件是等价的：（i）L是良连通逻辑，（ii）L是无限二叉树上闭包代数T_2^+的子代数的逻辑，（iii）L是极限为Scott拓扑的无限二叉树上闭包代数L_2^+的子代数的逻辑.最后证明了S4以上的逻辑L是连通的当且仅当L是R+的一个子代数的逻辑，并将结果推广到中间逻辑的情形。
A negative solution of Kuznetsov's problem for varieties of bi-Heyting algebras
我们表明，存在（连续许多）品种的双Heyting代数不是由其完整的成员。因此，存在（连续许多）扩展的海廷-布劳威尔逻辑$\mathsf{HB}$是拓扑不完整的。这一结果提供了进一步的洞察到长期开放的库兹涅佐夫问题，产生一个负的解决方案的问题，从中间逻辑的扩展$\mathsf{HB}$的重新制定。
From Intuitionism to Many-Valued Logics through Kripke Models
直觉命题逻辑是由Kurt Gödel（1932）证明的无限多值逻辑，它是由Stanismartaw Jaumkowski（1936）证明的可数多值逻辑。在本文中，我们使用Saul Kripke（1959）的模型为这些定理提供了另一种证明。哥德尔的证明产生了一个中间命题逻辑（介于直觉主义和经典之间），现在被称为哥德尔或哥德尔-达米特逻辑，也被模糊逻辑学家研究。我们还提供了一些结果，在此逻辑命题连接词的可定义性。
Conditionals and Modalities in Constructive Quantum Logics
研究推广直觉主义逻辑和量子逻辑的逻辑系统，提出iEx-逻辑作为直觉主义逻辑与带有Sasaki钩的orthomodular逻辑的交集，并刻画其扩展格。
Algebraic semantics for one-variable lattice-valued logics
任何一阶逻辑的单变量片段都可以被认为是模态逻辑，其中全称量词和存在量词分别被盒模态和菱形模态所取代。在一些情况下，这些逻辑的代数语义的公理化已经得到：最值得注意的是，分别为一阶经典逻辑和直觉主义逻辑的单变量片段的模态对应物S5和MIPC。然而，在一阶中间逻辑的设置之外，缺乏一种通用的方法。本文提供了这样一种方法的基础上设置的一阶格值逻辑，其中公式解释的代数结构与格约简。特别是，公理化得到的模态对应的一个广泛的家庭这些逻辑的一个变量片段通过推广的功能表示定理Bezhanishvili和哈丁一元Heyting代数。一个替代的证明理论的证明也提供了一个变量片段的一阶子结构逻辑，有一个切自由的插值演算，并承认一定的有界插值性质。
Tarski's Theorem on Intuitionistic logic, for polyhedra
1938年，塔斯基证明了一个公式不是直觉有效的当且仅当它在某个拓扑空间的开集的海廷代数中有一个反模型。事实上，塔斯基表明，任何欧几里得空间R^n与n >= 1就足够了，因为这样做，例如康托空间。特别地，直觉主义逻辑不能在欧几里得空间的所有开集的框架中检测拓扑维数。与此相反，我们考虑了紧致多面体P \subseteq R^n的开子多面体格，证明了它是R^n的所有开集的（非局部有限）代数的局部有限Heyting子代数，并证明了直觉主义逻辑能够通过有界深度公理图式来捕捉P的拓扑维数.此外，我们表明，直觉主义逻辑正是有效的公式在所有海廷代数所产生的多面体以这种方式的逻辑。因此，我们的主要定理调和通过多面体几何两个经典的结果：拓扑完备性的风格塔斯基，和Jaskowski的定理，直觉主义逻辑享有有限的模型属性。几个令人感兴趣的问题仍然悬而未决。例如，在一个示例中，所有闭可三角流形的中间逻辑是什么？
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。