Logics of Intuitionistic Kripke-Platek Set Theory
研究了直觉Kripke-Platek集合论IKP的逻辑结构，证明了IKP的一阶逻辑是直觉一阶逻辑IQC。
2021-06-09 math.LO
Copies of classical logic in intuitionistic logic
经典逻辑（非构造性数学的逻辑）比直觉主义逻辑（构造性数学的逻辑）更强。尽管如此，在直觉主义逻辑中仍然存在经典逻辑的副本。通常在文献中找到的所有副本都是相同的。这就提出了一个问题：副本是唯一的吗？我们通过提供三份不同的副本来否定回答。
2012-11-08 math.LO
Proof search in multi-succedent sequent calculi for intuitionistic logic under the Schuette's schema
继G. Mints（Kluwer 2000 and draft 2013），我们在Schuette模式的精神下，提出了直觉命题逻辑、直觉谓词逻辑的片段和完全直觉谓词逻辑的多后继递归演算中的终止和双完全证明搜索。
2017-01-03 math.LO
Sub-sub-intuitionistic logic
本文通过弱化蕴涵和移除分配律提出次次直觉主义逻辑，利用带选择函数的半格给出其语义，证明范畴对偶性并推导完备性，同时探讨了多种公理扩展。
2024-08-21 math.LO
Finite semantics for fragments of intuitionistic logic
1932年，哥德尔证明了直觉主义逻辑不存在有限语义。我们考虑直觉主义逻辑的所有片段，并在每种情况下检查是否存在有限语义。我们可以实现一个说教的目标，因为几乎没有逻辑和代数的先决条件。
2019-03-11 math.LO
The first-order logic of CZF is intuitionistic first-order logic
证明了CZF的一阶逻辑是直觉一阶逻辑。要做到这一点，我们引入了一个新的超限计算模型（集寄存器机），并结合由此产生的概念与贝丝语义的可实现性。同时，我们还证明了CZF的命题容许规则与直觉命题逻辑的命题容许规则完全相同。
2022-06-09 math.LO
An intuitionistically complete system of basic intuitionistic conditional logic
本文提出基本直觉主义条件逻辑IntCK，证明其相对克里普克模型和一阶直觉主义逻辑翻译的完备性，并分析其与CK、IK及Weiss的ICK的关系，讨论候选系统的优劣。
2023-06-17 math.LO
Embeddings into Free Heyting Algebras and Translations into Intuitionistic Propositional Logic
我们发现一个翻译具有特别好的性质，从直觉命题逻辑在可数多个变量的直觉命题逻辑在两个变量。此外，还证明了从任何可数逻辑到二元直觉命题逻辑的可能不那么好的翻译的存在性。证明了从经典逻辑到直觉主义命题逻辑的翻译不存在，它保留了“与”和“或”，但不一定是“真”。这些结果的翻译遵循额外的结果嵌入到自由海廷代数。
2007-02-22 math.LO
Intuitionistic Logic and Muchnik Degrees
我们证明，有一个因素的Muchnik格，捕捉直觉命题逻辑。这补充了现在经典的结果Skvortsova梅德韦杰夫格。
2010-03-23 math.LO
What Kinds of Connectives Cause the Difference between Intuitionistic Predicate Logic and the Logic of Constant Domains?
直觉Kripke语义可以推广到任意命题连接词的真假值函数。我们将这种广义Kripke语义推广到一阶逻辑，并研究了连接词的选择如何改变直觉谓词逻辑和常域逻辑之间在序列有效性方面的关系。我们的主要结果给出了直觉谓词逻辑中的有效序列集与常域逻辑中的有效序列集重合的一个简单的充要条件。
2022-05-12 math.LO
Intuitionistic predicate logic of constant domains does not have Beth property
借鉴以前的工作插值失败，我们表明，贝丝的可定义性定理不成立的直觉谓词逻辑的常数域没有身份。
2012-05-02 math.LO
The Lindstrom's Characterizability of Abstract Logic Systems for Analytic Structures Based on Measures
1969年，Per Lindstrom证明了他著名的刻画一阶逻辑的定理，并为离散结构的形式理论的一阶可定义性建立了标准。K. J. Barwise，S. Shelah，J.Vaananen和其他人将Lindstrom的特征化程序扩展到无穷逻辑系统的类别，包括M。Dzamonja和J.Vaananen关于Karp的链逻辑的一个新的结果，它满足内插、良序不可定义性，并且在具有这些性质的逻辑系统类中是极大的。链式逻辑的新颖之处在于它对可满足性的新定义。在我们的论文中，我们给出了一个框架Lindstrom的类型特征化的谓词逻辑系统的语义解释模型与对象的基础上的措施（分析结构）。特别地，Hajek积分逻辑被重新定义为具有一种新的Hajek可满足性的抽象逻辑，并构成了描述具有勒贝格积分的分析结构并满足紧性、初等链条件和弱否定的逻辑系统类中的极大逻辑。
2023-02-26 cs.CL cs.LO math.LO
Intuitionistic logic with a Galois connection has the finite model property
本文证明了作者提出的带伽罗瓦联络的直觉命题逻辑（IntGC）具有有限模型性质。
2011-02-01 math.LO
Proofs of some Propositions of the semi-Intuitionistic Logic with Strong Negation
我们提供的证明，完成我们的文章介绍了命题演算称为半直觉主义逻辑与强否定。
2017-08-30 math.LO
On algorithmic expressivity of finite-variable fragments of intuitionistic modal logics
本文证明了直觉主义模态逻辑FS和MIPC可多项式时间嵌入其正单变量片段，揭示了其算法表达力。
2023-06-27 math.LO
On the Various Translations between Classical, Intuitionistic and Linear Logic
本文以直觉主义线性逻辑的扩张为共同基础，提出统一方法设计和简化经典、直觉主义与线性逻辑之间的证明翻译，并由此重新得到文献中多数著名翻译。
2025-11-10 math.LO
Second order intuitionistic propositional logic of the real line is decidable
已知二阶直觉命题逻辑的重言式集合$\mathrm{IPC} 2$是不可判定的。本文证明了$\mathrm{IPC} 2$的公式集在实数或有理数的开子集的代数中是可判定的。
2016-12-21 math.LO
Decidability of quantified propositional intuitionistic logic and S4 on trees
量化命题直觉主义逻辑是由命题直觉主义逻辑通过在命题上添加量词\forall p，\exists p而得到的.在Kripke语义学的上下文中，一个命题是一个向上封闭的模型结构中世界的子集。Kremer（1997）证明了基于所有偏序类的量化命题直觉主义逻辑Hπ+与完全二阶逻辑递归同构。他提出了一个问题，即从限制到树的逻辑是否是可公理化的。事实证明，它是可判定的。所使用的方法也可以用来建立模态S4的可判定性与类似类型的Kripke结构的命题量化。
2002-03-18 math.LO
Intuitionistic Logic is a Connexive Logic
我们证明了直觉主义逻辑与连接Heyting逻辑（CHL）是演绎等价的，在此作为具有直觉语义的强连接逻辑的一个例子介绍。我们使用的反向代数化范式：CHL的断言逻辑的一个点经常品种（其结构理论进行了详细研究），原来是长期等价于各种海廷代数。我们提供了希尔伯特式和根森式的证明系统CHL，此外，我们提出了一个可能的计算解释其连接条件，我们重新Kapsner的想法superconnexivity。
2022-08-31 math.LO
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic
在他们的开创性论文中，阿特莫夫和Protopescu提供了希尔伯特形式系统，Brower-Heyting-Kolmogorov和Kripke语义的直觉信念和知识的逻辑。随后Krupski证明了直觉知识的逻辑是PSPACE完全的，Su和Sano提供了享有子公式属性的演算。本文通过提供具有子公式性质且终止于线性深度的隐式演算，继续了对直觉主义认知逻辑隐式演算的研究。我们的演算允许我们设计一个过程，对于无效的公式，返回一个最小深度的Kripke模型。最后我们还讨论了反驳的反演算，即证明无效性的反演算。
2021-03-04 math.LO
A Decidable Intuitionistic Temporal Logic
本文介绍了一种基于结构$(W,\preccurlyeq,S)$的直觉时态逻辑$\sf ITL^e$，其中$\preccurlyeq$用于解释直觉蕴涵，$S$是一个用于解释时态模态的$\preccurlyeq$-单调函数.我们的主要结果是$\sf ITL^e$的可满足性和有效性问题是可判定的。我们证明了这一点，显示逻辑享有强有限模型属性。相比之下，我们还考虑一个"持久"版本的逻辑，$\sf ITL^p$，其模型是类似的笛卡儿积。证明了与$\sf ITL^e$不同，$\sf ITL^p$不具有有限模型性质.
2017-04-10 math.LO
Supervaluations, truth, and intuitionistic logic
本文提出了一种基于超估值方法的直觉逻辑固定点真理理论，并展示了其在Kripke结构上的应用及与经典逻辑的对比。
2025-11-19 math.LO
Polytopological Semantics for Intuitionistic Modal Logics
Technische Universität Wien（维也纳工业大学）；University of Barcelona（巴塞罗那大学）；Institute of Science Tokyo（东京科学大学）
本文提出多拓扑语义用于构造、直觉及Goedel-Dummett的K4和S4变种，通过单一集合上的多种拓扑解释直觉和模态运算符，并证明这些逻辑在相应语义下是正确且强完备的。
2026-04-25 math.LO
Relative Unification in Intuitionistic Logic: Towards provability logic of HA
该研究将直觉主义逻辑的统一性与可容许性结果推广到 NNIL(par) 命题，用以刻画 HA 的可证性逻辑并证明其可判定性。
2025-10-06 math.LO
Carnap's problem for intuitionistic propositional logic
我们表明，直觉命题逻辑是\emph{Carnap categorical}：唯一的解释与直觉后果关系一致的连接词是标准的解释。这相对于最著名的语义学而言是成立的，直觉主义逻辑在这些语义学中是健全的和完备的;其中包括克里普克语义学、贝斯语义学、德拉加林语义学和拓扑语义学。它也适用于代数语义，尽管在这种情况下的范畴性与相对于可能世界样式语义的范畴性在种类上不同。
2022-12-25 math.LO
Projectivity meets Uniform Post-Interpolant: Classical and Intuitionistic Logic
本文研究经典与直觉主义命题逻辑中投射性与一致后插值的关系，证明经典逻辑中二者对所有公式等价，并给出直觉主义逻辑的Kripke语义刻画，进而证明某些直觉主义逻辑扩张的统一类型是有穷的。
2024-03-29 math.LO
De Jongh's Theorem for Intuitionistic Zermelo-Fraenkel Set Theory
证明了直觉集合论IZF的命题逻辑是直觉命题逻辑IPC。更一般地说，我们表明，IZF有德容财产方面的每一个中间的逻辑是完整的一类有限树。对于CZF也有相同的结果。
2019-05-13 math.LO
Bi-intuitionistic logics through the abstract algebraic logic lens
针对双直觉主义逻辑缺乏代数处理的问题，研究者用抽象代数逻辑等方法对wBIL和sBIL开展代数分析，相关结果已在Rocq中形式化。
2025-03-21 math.LO
Esakia's theorem for the amended monadic intuitionistic calculus
New Mexico State University（新墨西哥州立大学）；University of Milan（米兰大学）
该研究证明修正的单子直觉逻辑M^+IPC的Esakia定理成立，揭示了其与修正的单子Grzegorczyk逻辑之间的关系。
2025-12-19 math.LO
Classical logic and intuitionistic logic: equivalent formulations in natural deduction, Gödel-Kolmogorov-Glivenko translation
本文首先证明了直觉主义逻辑中几种经典逻辑公式（非数据第三定律、反证法、皮尔斯定律）之间的等价性。然后，它建立了正确的哥德尔-柯尔莫哥洛夫翻译，其限制的命题的情况下，是由于格利文科。这种转换将一阶逻辑的公式$F$映射为公式$F^{\lnot\lnot}$，使得$F$在经典逻辑中可证明当且仅当$F^{\lnot\lnot}$在直觉主义逻辑中可证明。所有的形式证明都是在自然演绎中提出的。这些问题是众所周知的证明理论事实，但在教科书中，它们往往被忽略或留给读者。由于组合困难的一些必要的正式证明，我们希望这份报告可能是有用的，特别是学生和同事从其他领域。
2016-02-25 math.LO
Failure of interpolation in the intuitionistic logic of constant domains
本文证明了内插定理在常域的直觉主义逻辑中是不成立的。这一结果驳斥了两个先前发表的主张，插值性质举行。
2012-04-02 math.LO
Uniform Definability in Propositional Dependence Logic
命题依赖逻辑和探究逻辑都是表达完备的。因此，任何具有直觉析取或直觉蕴涵的公式都可以等价地翻译成命题依赖逻辑语言中的公式，而不需要这两个连接词。我们表明，虽然这样的（非成分）翻译存在，既不是直觉析取也不是直觉蕴涵是一致定义的命题依赖逻辑。
2016-11-16 math.LO
An Arithmetical Interpretation of Verification and Intuitionistic Knowledge
直觉主义认识逻辑向直觉主义逻辑引入了一个认识运算符，该运算符反映了直觉主义的预期BHK语义。关于直觉主义知识和信念的基本假设是，它是验证的产物。BHK对直觉主义逻辑的解释在《证明的逻辑》及其算术语义学中有一个精确的表述。我们在这里表明，这种解释可以扩展到验证的概念，直觉知识的基础上，从而提供了系统的直觉认知逻辑扩展的认知算子的基础上验证算术语义。
2016-01-12 math.LO
Following all the rules: Intuitionistic completeness for generalised proof-theoretic validity
普拉维茨指出，证明理论上有效的逻辑是直觉主义逻辑。最近的工作证明理论的有效性已经推翻了这一点。事实上，它已经表明，证明理论的有效性甚至不是封闭的替代。在本文中，我们对Prawitz（1973）中发现并由Schroeder-Heister（2006）完善的证明理论有效性的定义进行了微小的修改。我们将把这个新概念称为广义证明理论有效性，并证明广义证明理论有效性的逻辑是直觉主义逻辑。
2022-11-22 math.LO
Intuitionistic and Constructive Modal Logics for Classical Modal Logicians
本文面向经典模态逻辑研究者，综述直觉主义框架下的两类命题模态逻辑，研究介于两者间的新逻辑$\textbf{KI}$并证其完备性，还指出$\textbf{CK}$语义缺陷并证明$\textbf{CK}$、$\textbf{WK}$的Lyndon插值定理。
2026-10-12 math.LO
Expressive power of basic modal intuitionistic logic as a fragment of classical FOL
本文讨论了模态直觉主义逻辑的Kripke式语义的四种不同版本所导出的一阶逻辑片断。为了捕捉这些片段，asimulation的概念进行了修改和扩展，以产生Van Benthem类型的语义表征各自的表达能力。它示出，进一步，这种特征可以很容易地进行到任意一阶可定义的子类的经典一阶模型。
2015-11-06 math.LO
A complete axiomatization of infinitary first-order intuitionistic logic over $\mathcal{L}_{κ^+, κ}$
给定一个弱紧基数$κ$，给出了$\mathcal{L}_{κ^+, κ}$上直觉一阶逻辑的公理化，并证明了它对于Kripke模型是可靠的和完备的.因此，我们得到了该逻辑的析取和存在性质。这推广了Nadel关于$\mathcal{L}_{ω_1, ω}$上的直觉主义逻辑的工作。当$κ$是一个正则基数使得$κ^{<κ}=κ$时，我们通过一个简单的证明修改，推导出$\mathcal{L}_{κ^+, κ, κ}$上的直觉一阶逻辑的一个完全公理化，该语言具有至多$κ$公式的析取，小于$κ$公式的合取和小于$κ$许多变量的量化.特别地，这适用于广义连续统假设下的任何正则基数。
2020-12-28 math.LO
Generalized Realizability and Intuitionistic Logic
设V是一组数论函数。我们定义了谓词公式的V -可实现性概念，使得V中函数的下标用于解释蕴涵和全称量词。本文证明了直觉谓词演算关于V -可实现的语义是合理的当且仅当V的某些自然条件成立。
2022-05-17 math.LO
Multi-topological semantics for intuitionistic modal logic
我们提出了三个例子的\textit{multi-topological}语义的直觉模态逻辑与一个模态运算符$\Box$（其行为在某种意义上像必要性）。我们表明，它是可能的处理邻域模型，前面介绍的，作为多拓扑。从邻域的角度来看，我们的方法是基于最小和最大邻域的属性之间的差异。并提出了多拓扑空间到邻域结构的变换。虽然我们的邻居可以被认为是双关系模型，我们相信，推理的邻居提供了更好的拓扑直觉。
2019-03-16 math.LO
Stable Canonical Rules for Intuitionistic Modal Logics
本文研究了直观模态逻辑的稳定公理规则，证明了多结论推论关系可由稳定公理规则 axiomatize，并以此证明了Blok-Esakia定理的替代证明及扩展，同时解决了Dummett-Lemmon猜想。
2026-02-10 math.LO
Mathematical semantics of intuitionistic logic
这项工作是一个数学家试图理解直觉主义逻辑。它可以从两个方面来阅读：作为一篇研究论文，穿插着对标准材料的反思的冗长离题;或者作为对一阶直觉主义逻辑的基本（但非常非传统）介绍。对于后一个目的，不需要在形式逻辑的培训，但在数学，如拓扑空间和偏序集适度识字，是假设。这项工作的主要主题是寻找一个正式的语义足以Kolmogorov的非正式解释的直觉主义逻辑（其最简单的部分是或多或少相同的所谓BHK解释）。这种搜索超越了通常的模型论，基于塔斯基的语义后果的概念，并超越了通常的形式主义的一阶逻辑，基于图式。因此，我们研究形式语义的简化版本的保尔森的元逻辑，在伊莎贝尔证明。通过构造性地解释元逻辑连接词和量词，我们得到了一个广义的模型论，它特别涵盖了直觉主义逻辑的可实现型解释。另一方面，通过分析Kolmogorov的语义后果概念（它是Tarski标准概念的替代），我们得到了替代的模型论。通过对元逻辑的扩展，我们进一步得到了一个广义的替代模型论，它足以形式化Kolmogorov的语义。另一方面，我们也制定了修改Kolmogorov的解释，这是兼容的通常，塔斯基风格的模型论。也就是说，它可以通过层值模型形式化，这是Palmgren的范畴模型的一个特例;直觉主义逻辑在这个语义上是完备的。
2017-05-01 math.LO
Proof Theory for Intuitionistic Strong Löb Logic
本文介绍了两种直觉强Löb逻辑的终结演算${\sf iSL}_\Box$：一种是基于直觉命题逻辑${\sf IPC}$的终结演算${\sf G4ip}$的终结演算${\sf G4iSL}_\Box$，另一种是标准无割演算${\sf G3ip}$的无结构规则的扩展${\sf G3iSL}_\Box$.主要结果之一是${\sf G3iSL}_\Box$的割消定理的句法证明。此外，还建立了${\sf iSL}_\Box$的微积分与Hilbert系统之间的等价关系.从文献中可知，${\sf iSL}_\Box$对于一类直觉模态Kripke模型是完备的，其中模态关系是传递的，相反是良基的，并且是直觉关系的子集.在这里，这一事实的建设性证明是通过使用一个反模型的基础上的一个变种的${\sf G4iSL}_\Box$建设。因此，该文件包含两个证明削减消除，语义和句法证明。
2023-03-06 math.LO
Hypersequents and the Proof Theory of Intuitionistic Fuzzy Logic
Takeuti和Titani介绍并研究了他们称为直觉模糊逻辑的逻辑。这种逻辑被刻画为基于真假值集[0，1]的一阶Goedel逻辑。逻辑是已知的公理化，但没有演绎系统服从证明理论，因此，计算处理，已被称为。这样一个系统在这里提出，根据以前的工作hypereclithography命题哥德尔逻辑的Avron。结果表明，该系统是完善的，并允许切割消除。高野提出的一个关于Takeuti-Titani密度规则是否可消除的问题得到了肯定的回答。
2000-08-27 math.LO
Intuitionistic Epistemic Logic
我们概述了一个直观的知识观，保持原来的Brouwer-Heyting-Kolmogorov语义的直觉主义，是一致的，与著名的方法，直观的知识被视为验证的结果。我们认为，在这种情况下，共同反思$A \rightarrow {\bf{K}} A$是有效的，知识的事实性持有的形式${\bf{K}} A \rightarrow \neg\neg A$“已知的命题不能是假的”。我们表明，传统形式的事实${\bf{K}} A \rightarrow A$是一个明显的经典原则，像{ \it tertium non datur} $A\vee\neg A$，不持有直观，但随着整个经典的认知逻辑，是直观有效的双重否定形式$\neg\neg({\bf{K}} A\rightarrow A)$。在直觉主义的认识框架内，可知性悖论以一种建设性的方式得到解决。我们认为，这一悖论是一个毫无根据的建设性原则的经典阅读的结果，因此并没有传统上归因于它的建设性基础的后果。
2016-01-16 math.LO
Hennessy-Milner Properties via Topological Compactness
本文给出了直觉Kripke模型下的直觉逻辑、对偶直觉逻辑和双直觉逻辑的Hennessy-Milner类，并将这些结果推广到模态（对偶和双）直觉主义逻辑.我们的主要技术工具是图像紧凑和预图像紧凑的关系，提供了一个语义描述的模态饱和度属性。
2021-05-05 math.LO
Realisability for Infinitary Intuitionistic Set Theory
我们介绍了一个基于有序图灵机（OTM）的无穷直觉集合论的可实现性语义。我们表明，我们的OTM-可实现性的概念是健全的某些系统的无穷直觉主义逻辑，并实现了所有公理的无穷Kripke-Platek集合论。最后，我们使用我们的可实现性概念的一个变体来证明（有限）直觉Kripke-Platek集合论的命题容许规则正是直觉命题逻辑的容许规则。
2022-12-13 math.LO
A Galois connection between classical and intuitionistic logics. I: Syntax
在1985年对他的作品集的评论中，Kolmogorov评论说，他1932年的论文“是希望随着时间的推移，解决问题的逻辑[即，直觉主义逻辑]将成为逻辑学[标准]课程的永久部分。一个统一的逻辑装置是打算创建，这将处理两种类型的对象-命题和问题。“我们构造了这样一个形式系统，以及它的谓词版本QHC，它是直觉谓词演算QH和经典谓词演算QC的保守扩展。唯一的新连接词？还有！的QHC诱导伽罗瓦连接（即，QH和QC的Lindenbaum偏序集（即Lindenbaum代数的基础偏序集）之间的一对伴随函子。Kolmogorov的双重否定翻译的命题到问题延伸到一个撤回的QHC到QH;而哥德尔的可证明性翻译的问题到模态命题延伸到一个撤回的QHC到其QC+（？！）片段，用模态逻辑QS 4标识。QH+（！？）片段是一个直觉主义的模态逻辑，它的模态是谁的？在Aczel意义上是一个严格的松弛模态，因此类似于直觉类型理论中的squash/bracket操作。QHC的公理试图对直觉主义逻辑的两个最著名的内容解释给出一个更完整的形式化（相对于直觉主义逻辑的公理）：柯尔莫哥洛夫的问题解释（包含海廷和克赖塞尔的标准改进）和奥尔洛夫和海廷的证明解释（如哥德尔所澄清的）。虽然这两种解释经常被混为一谈，但从QHC公理的观点来看，它们都没有减少到另一个，尽管它们确实重叠。
2022-10-02 math.LO
The intuitionistic temporal logic of dynamical systems
本文提出动力系统的直觉主义时态逻辑变体 ITL^c，证明其可判定性，并表明它能表达极小性和庞加莱回归，可用于推理非平凡渐近行为。
2018-07-19 math.LO
On an Inferential Semantics for Intuitionistic Sentential Logic
本文揭示了Sandqvist的B-eS与Mints基于归结的方法之间的联系，证明B-eS的可靠性与完备性可直接由Mints定理得出，强调了证明搜索与归结方法在构造性推理中的概念作用。
2025-04-28 math.LO
Monadic Intuitionistic and Modal Logics Admitting Provability Interpretations
哥德尔翻译提供了一种将直觉主义逻辑$\mathsf{IPC}$嵌入模态逻辑$\mathsf{Grz}$的方法，然后模态逻辑通过分裂翻译嵌入模态逻辑$\mathsf{GL}$。结合Solovay定理，$\mathsf{GL}$是Peano算术$\mathsf{PA}$的可证性谓词的模态逻辑，$\mathsf{IPC}$和$\mathsf{Grz}$都允许算术解释。当试图将这些结果“提升”到这些逻辑的一元扩展$\mathsf{MIPC}$、$\mathsf{MGrz}$和$\mathsf{MGL}$时，相同的技术不再起作用。根据Esakia的猜想，我们将Casari公式的适当版本添加到这些一元扩展中（用"+“表示），得到哥德尔翻译将$\mathsf{M^{+}IPC}$嵌入$\mathsf{M^{+}Grz}$，分裂翻译将$\mathsf{M^{+}Grz}$嵌入$\mathsf{MGL}$。正如Japaridze所证明的那样，Solovay的结果扩展到一元系统$\mathsf{MGL}$，这使我们对$\mathsf{M^{+}IPC}$和$\mathsf{M^{+}Grz}$都有了算术解释。
2021-03-21 math.LO
A note on the intuitionistic logic of false belief
本文分析了直觉主义背景下的错误信念逻辑。这种逻辑，在其经典版本中由Steinsvold，Fan，Gilbert和Venturi研究，描述了以下情况：公式F在给定的世界中不满足，但我们仍然相信它（或者我们认为它应该被接受）。另一种解释也是可能的：例如，我们不接受F，但它是由一种理事会或咨询委员会强加给我们的。从数学的角度来看，这一思想是由一个适当形式的模态算子W，它是在关系框架与邻域解释。我们讨论了强迫的单调性，可靠性，完备性和其他几个问题。我们还提出了一些简单的系统，其中确认以前接受的公式建模。
2020-11-04 math.LO
Intuitionistic Implication in Elementary Team Logics
University of Gothenburg（哥德堡大学）；University of Helsinki（赫尔辛基大学）
本文研究初等团队逻辑FOT的两种修改：其无包含原子片段的量词消去，以及添加直觉主义蕴涵后表达能力提升至全二阶逻辑，导致有效性等价。
2026-09-15 math.LO
Mass problems and intuitionistic higher-order logic
本文研究了直觉高阶逻辑的一个模型，我们称之为\emph{the Muchnik topos}。Muchnik拓扑可以简单地定义为在由图灵度组成的拓扑空间上的集合层的范畴，其中图灵锥形成拓扑的基础。我们注意到，我们的直觉数学的Muchnik topos解释是直觉命题演算的著名Kolmogorov/Muchnik解释通过Muchnik度的扩展，即，弱约化下的质量问题我们引入了直觉实数的一种新的层表示，即\emph{the Muchnik reals}，它不同于柯西实数和戴德金实数。在Muchnik拓扑中，我们得到了\emph{choice principle} $(\forall x\,\exists y\,A(x,y))\Rightarrow\exists w\,\forall x\,A(x,wx)$和\emph{bounding principle} $(\forall x\,\exists y\,A(x,y))\Rightarrow\exists z\,\forall x\,\exists y\,(y\le_{\mathrm{T}}(x,z)\land A(x,y))$，其中$x,y,z$的范围是Muchnik实数，$w$的范围是从Muchnik实数到Muchnik实数的函数，而$A(x,y)$是不包含$w$或$z$的公式。为了方便读者，我们解释了所有关于直觉主义，层理论，直觉高…
2014-08-12 math.LO
Intuitionistic logic with two Galois connections combined with Fischer Servi axioms
早些时候，作者介绍了逻辑IntGC，它是通过两个模仿伽罗瓦连接性能的推理规则对直觉命题逻辑的扩展（Logic J. of the IGPL，18：837-858，2010）。本文研究了IntGC的扩展Int 2GC和Int 2GC +FS。Int 2GC可以看作是两个IntGC逻辑的融合，Int 2GC +FS是通过添加由G. Fischer Servi（Rend. Sem等Mat.宇宙Politecn. Torino，42：179-194，1984），用于互连Int 2GC的两个伽罗瓦连接。给出了Int 2GC和Int 2GC +FS的Kripke风格和代数语义，并证明了其逻辑在这两种语义下都是完备的。我们证明了定义在完备Heyting代数上的粗糙格值模糊集是Int 2GC +FS的适当代数模型。我们还证明了Int 2GC +FS等价于直觉时态逻辑IKt，以及IKt的一个公理化，其公理数目减少到W给出的公理数目的一半。B. Ewald（J. Symb. Log，51：166-179，1986）。
2012-08-14 math.LO
