Failure of interpolation in the intuitionistic logic of constant domains
Grigori Mints, Grigory Olkhovikov, Alasdair Urquhart
本文证明了内插定理在常域的直觉主义逻辑中是不成立的。这一结果驳斥了两个先前发表的主张，插值性质举行。
This paper shows that the interpolation theorem fails in the intuitionistic logic of constant domains. This result refutes two previously published claims that the interpolation property holds.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Intuitionistic logic, dual intuitionistic logic, and modality
本文通过余海廷代数与拓扑空间的关系研究对偶直觉主义逻辑的语义，并证明其与直觉主义逻辑通过Kripke语义共同关联于模态逻辑S4。
Logics of Intuitionistic Kripke-Platek Set Theory
研究了直觉Kripke-Platek集合论IKP的逻辑结构，证明了IKP的一阶逻辑是直觉一阶逻辑IQC。
Copies of classical logic in intuitionistic logic
经典逻辑（非构造性数学的逻辑）比直觉主义逻辑（构造性数学的逻辑）更强。尽管如此，在直觉主义逻辑中仍然存在经典逻辑的副本。通常在文献中找到的所有副本都是相同的。这就提出了一个问题：副本是唯一的吗？我们通过提供三份不同的副本来否定回答。
Proof search in multi-succedent sequent calculi for intuitionistic logic under the Schuette's schema
继G. Mints（Kluwer 2000 and draft 2013），我们在Schuette模式的精神下，提出了直觉命题逻辑、直觉谓词逻辑的片段和完全直觉谓词逻辑的多后继递归演算中的终止和双完全证明搜索。
Sub-sub-intuitionistic logic
本文通过弱化蕴涵和移除分配律提出次次直觉主义逻辑，利用带选择函数的半格给出其语义，证明范畴对偶性并推导完备性，同时探讨了多种公理扩展。
Finite semantics for fragments of intuitionistic logic
1932年，哥德尔证明了直觉主义逻辑不存在有限语义。我们考虑直觉主义逻辑的所有片段，并在每种情况下检查是否存在有限语义。我们可以实现一个说教的目标，因为几乎没有逻辑和代数的先决条件。
The first-order logic of CZF is intuitionistic first-order logic
证明了CZF的一阶逻辑是直觉一阶逻辑。要做到这一点，我们引入了一个新的超限计算模型（集寄存器机），并结合由此产生的概念与贝丝语义的可实现性。同时，我们还证明了CZF的命题容许规则与直觉命题逻辑的命题容许规则完全相同。
An intuitionistically complete system of basic intuitionistic conditional logic
本文提出基本直觉主义条件逻辑IntCK，证明其相对克里普克模型和一阶直觉主义逻辑翻译的完备性，并分析其与CK、IK及Weiss的ICK的关系，讨论候选系统的优劣。
Maximality of bi-intuitionistic propositional logic
本文采用经典一阶逻辑的Lindström定理的形式，将命题双直觉主义逻辑刻画为满足某种形式的紧性、Tarski并性质和双模拟下的保持性的极大（就表达能力而言）抽象逻辑。由于双直觉主义逻辑通过增加向后看模态的模拟在直觉设置中引入了新的复杂性，本文构成了作者在G. Badia和G.奥尔霍维科夫直觉主义命题逻辑的林斯特龙定理。Notre Dame Journal of Formal Logic，61（1）：11-30（2020）.
Embeddings into Free Heyting Algebras and Translations into Intuitionistic Propositional Logic
我们发现一个翻译具有特别好的性质，从直觉命题逻辑在可数多个变量的直觉命题逻辑在两个变量。此外，还证明了从任何可数逻辑到二元直觉命题逻辑的可能不那么好的翻译的存在性。证明了从经典逻辑到直觉主义命题逻辑的翻译不存在，它保留了“与”和“或”，但不一定是“真”。这些结果的翻译遵循额外的结果嵌入到自由海廷代数。
Intuitionistic Logic and Muchnik Degrees
我们证明，有一个因素的Muchnik格，捕捉直觉命题逻辑。这补充了现在经典的结果Skvortsova梅德韦杰夫格。
What Kinds of Connectives Cause the Difference between Intuitionistic Predicate Logic and the Logic of Constant Domains?
直觉Kripke语义可以推广到任意命题连接词的真假值函数。我们将这种广义Kripke语义推广到一阶逻辑，并研究了连接词的选择如何改变直觉谓词逻辑和常域逻辑之间在序列有效性方面的关系。我们的主要结果给出了直觉谓词逻辑中的有效序列集与常域逻辑中的有效序列集重合的一个简单的充要条件。
A Lindström theorem for intuitionistic first-order logic
推广了（G. Badia和G.奥尔霍维科夫直觉主义命题逻辑的林斯特龙定理。Notre Dame Journal of Formal Logic，61（1）：11- 30（2020））到一阶直觉主义逻辑（有和没有相等），表明它是满足某种形式的紧性、塔斯基并性质和在模拟下保持的最大（关于表达能力）抽象逻辑。对于常域的直觉主义逻辑也得到了类似的结果。
A Lindström theorem for intuitionistic propositional logic
证明了命题直觉主义逻辑是满足某种拓扑性质的最大（就表达能力而言）抽象逻辑，这些拓扑性质包括紧性、Tarski并性质和模拟下的保持性.
Intuitionistic predicate logic of constant domains does not have Beth property
借鉴以前的工作插值失败，我们表明，贝丝的可定义性定理不成立的直觉谓词逻辑的常数域没有身份。
Intuitionistic logic with a Galois connection has the finite model property
本文证明了作者提出的带伽罗瓦联络的直觉命题逻辑（IntGC）具有有限模型性质。
Proofs of some Propositions of the semi-Intuitionistic Logic with Strong Negation
我们提供的证明，完成我们的文章介绍了命题演算称为半直觉主义逻辑与强否定。
On algorithmic expressivity of finite-variable fragments of intuitionistic modal logics
本文证明了直觉主义模态逻辑FS和MIPC可多项式时间嵌入其正单变量片段，揭示了其算法表达力。
On the Various Translations between Classical, Intuitionistic and Linear Logic
本文以直觉主义线性逻辑的扩张为共同基础，提出统一方法设计和简化经典、直觉主义与线性逻辑之间的证明翻译，并由此重新得到文献中多数著名翻译。
Second order intuitionistic propositional logic of the real line is decidable
已知二阶直觉命题逻辑的重言式集合$\mathrm{IPC} 2$是不可判定的。本文证明了$\mathrm{IPC} 2$的公式集在实数或有理数的开子集的代数中是可判定的。
Decidability of quantified propositional intuitionistic logic and S4 on trees
量化命题直觉主义逻辑是由命题直觉主义逻辑通过在命题上添加量词\forall p，\exists p而得到的.在Kripke语义学的上下文中，一个命题是一个向上封闭的模型结构中世界的子集。Kremer（1997）证明了基于所有偏序类的量化命题直觉主义逻辑Hπ+与完全二阶逻辑递归同构。他提出了一个问题，即从限制到树的逻辑是否是可公理化的。事实证明，它是可判定的。所使用的方法也可以用来建立模态S4的可判定性与类似类型的Kripke结构的命题量化。
Completeness and interpolation for intuitionistic infinitary predicate logic, in connection to finitizing the class of representable Heyting polyadic algebras
研究了Heyting多进代数的各种约简的表示定理。超合并证明了几个（自然约简）和我们的结果进行了比较，在经典代数逻辑处理圆柱和polyadic（布尔代数）的有限性问题。我们还证明了几个新的整齐嵌入定理，并得到了基于（广义）Kripke语义的可表示代数类与具有整齐嵌入性质的代数类，即那些代数是具有$ω$额外维数的代数的次整齐约化.
Intuitionistic Logic is a Connexive Logic
我们证明了直觉主义逻辑与连接Heyting逻辑（CHL）是演绎等价的，在此作为具有直觉语义的强连接逻辑的一个例子介绍。我们使用的反向代数化范式：CHL的断言逻辑的一个点经常品种（其结构理论进行了详细研究），原来是长期等价于各种海廷代数。我们提供了希尔伯特式和根森式的证明系统CHL，此外，我们提出了一个可能的计算解释其连接条件，我们重新Kapsner的想法superconnexivity。
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic
在他们的开创性论文中，阿特莫夫和Protopescu提供了希尔伯特形式系统，Brower-Heyting-Kolmogorov和Kripke语义的直觉信念和知识的逻辑。随后Krupski证明了直觉知识的逻辑是PSPACE完全的，Su和Sano提供了享有子公式属性的演算。本文通过提供具有子公式性质且终止于线性深度的隐式演算，继续了对直觉主义认知逻辑隐式演算的研究。我们的演算允许我们设计一个过程，对于无效的公式，返回一个最小深度的Kripke模型。最后我们还讨论了反驳的反演算，即证明无效性的反演算。
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$不具有有限模型性质.
Craig interpolation theorem fails in bi-intuitionistic predicate logic
本文通过改编Mints等人的反例，证明双直觉谓词逻辑缺乏Craig插值性质，并澄清该结果与Rauszer的“演绎插值”定理不矛盾。
Supervaluations, truth, and intuitionistic logic
本文提出了一种基于超估值方法的直觉逻辑固定点真理理论，并展示了其在Kripke结构上的应用及与经典逻辑的对比。
Polytopological Semantics for Intuitionistic Modal Logics
本文提出多拓扑语义用于构造、直觉及Goedel-Dummett的K4和S4变种，通过单一集合上的多种拓扑解释直觉和模态运算符，并证明这些逻辑在相应语义下是正确且强完备的。
Relative Unification in Intuitionistic Logic: Towards provability logic of HA
该研究将直觉主义逻辑的统一性与可容许性结果推广到 NNIL(par) 命题，用以刻画 HA 的可证性逻辑并证明其可判定性。
Carnap's problem for intuitionistic propositional logic
我们表明，直觉命题逻辑是\emph{Carnap categorical}：唯一的解释与直觉后果关系一致的连接词是标准的解释。这相对于最著名的语义学而言是成立的，直觉主义逻辑在这些语义学中是健全的和完备的;其中包括克里普克语义学、贝斯语义学、德拉加林语义学和拓扑语义学。它也适用于代数语义，尽管在这种情况下的范畴性与相对于可能世界样式语义的范畴性在种类上不同。
Projectivity meets Uniform Post-Interpolant: Classical and Intuitionistic Logic
本文研究经典与直觉主义命题逻辑中投射性与一致后插值的关系，证明经典逻辑中二者对所有公式等价，并给出直觉主义逻辑的Kripke语义刻画，进而证明某些直觉主义逻辑扩张的统一类型是有穷的。
De Jongh's Theorem for Intuitionistic Zermelo-Fraenkel Set Theory
证明了直觉集合论IZF的命题逻辑是直觉命题逻辑IPC。更一般地说，我们表明，IZF有德容财产方面的每一个中间的逻辑是完整的一类有限树。对于CZF也有相同的结果。
Bi-intuitionistic logics through the abstract algebraic logic lens
针对双直觉主义逻辑缺乏代数处理的问题，研究者用抽象代数逻辑等方法对wBIL和sBIL开展代数分析，相关结果已在Rocq中形式化。
Esakia's theorem for the amended monadic intuitionistic calculus
该研究证明修正的单子直觉逻辑M^+IPC的Esakia定理成立，揭示了其与修正的单子Grzegorczyk逻辑之间的关系。
Interpolation in extensions of first-order logic
证明了前原引理的一个推广，证明了经典和直觉主义一阶逻辑的扩展具有一种特殊类型的几何公理，称为奇异几何公理，具有Craig的插值性质。作为推论，我们得到了（经典的和直觉主义的）一阶逻辑有恒等式的插值的直接证明，以及几个数学理论的插值，包括等价关系理论，（严格）偏序和线性序，以及各种直觉主义序理论，如不相合性和正偏序和线性序.
Classical logic and intuitionistic logic: equivalent formulations in natural deduction, Gödel-Kolmogorov-Glivenko translation
本文首先证明了直觉主义逻辑中几种经典逻辑公式（非数据第三定律、反证法、皮尔斯定律）之间的等价性。然后，它建立了正确的哥德尔-柯尔莫哥洛夫翻译，其限制的命题的情况下，是由于格利文科。这种转换将一阶逻辑的公式$F$映射为公式$F^{\lnot\lnot}$，使得$F$在经典逻辑中可证明当且仅当$F^{\lnot\lnot}$在直觉主义逻辑中可证明。所有的形式证明都是在自然演绎中提出的。这些问题是众所周知的证明理论事实，但在教科书中，它们往往被忽略或留给读者。由于组合困难的一些必要的正式证明，我们希望这份报告可能是有用的，特别是学生和同事从其他领域。
Uniform Definability in Propositional Dependence Logic
命题依赖逻辑和探究逻辑都是表达完备的。因此，任何具有直觉析取或直觉蕴涵的公式都可以等价地翻译成命题依赖逻辑语言中的公式，而不需要这两个连接词。我们表明，虽然这样的（非成分）翻译存在，既不是直觉析取也不是直觉蕴涵是一致定义的命题依赖逻辑。
Definable Classes of Models and Frames in Bi-intuitionistic Logic
研究双直觉逻辑语言对框架和模型的表达能力，通过提供类似戈德布拉特 - 托马森定理的结果，结合先前成果，完整刻画了命题双直觉逻辑的表达能力。
An Arithmetical Interpretation of Verification and Intuitionistic Knowledge
直觉主义认识逻辑向直觉主义逻辑引入了一个认识运算符，该运算符反映了直觉主义的预期BHK语义。关于直觉主义知识和信念的基本假设是，它是验证的产物。BHK对直觉主义逻辑的解释在《证明的逻辑》及其算术语义学中有一个精确的表述。我们在这里表明，这种解释可以扩展到验证的概念，直觉知识的基础上，从而提供了系统的直觉认知逻辑扩展的认知算子的基础上验证算术语义。
Following all the rules: Intuitionistic completeness for generalised proof-theoretic validity
普拉维茨指出，证明理论上有效的逻辑是直觉主义逻辑。最近的工作证明理论的有效性已经推翻了这一点。事实上，它已经表明，证明理论的有效性甚至不是封闭的替代。在本文中，我们对Prawitz（1973）中发现并由Schroeder-Heister（2006）完善的证明理论有效性的定义进行了微小的修改。我们将把这个新概念称为广义证明理论有效性，并证明广义证明理论有效性的逻辑是直觉主义逻辑。
Intuitionistic and Constructive Modal Logics for Classical Modal Logicians
本文面向经典模态逻辑研究者，综述直觉主义框架下的两类命题模态逻辑，研究介于两者间的新逻辑$\textbf{KI}$并证其完备性，还指出$\textbf{CK}$语义缺陷并证明$\textbf{CK}$、$\textbf{WK}$的Lyndon插值定理。
Expressive power of basic modal intuitionistic logic as a fragment of classical FOL
本文讨论了模态直觉主义逻辑的Kripke式语义的四种不同版本所导出的一阶逻辑片断。为了捕捉这些片段，asimulation的概念进行了修改和扩展，以产生Van Benthem类型的语义表征各自的表达能力。它示出，进一步，这种特征可以很容易地进行到任意一阶可定义的子类的经典一阶模型。
A complete axiomatization of infinitary first-order intuitionistic logic over $\mathcal{L}_{κ^+, κ}$
给定一个弱紧基数$κ$，给出了$\mathcal{L}_{κ^+, κ}$上直觉一阶逻辑的公理化，并证明了它对于Kripke模型是可靠的和完备的.因此，我们得到了该逻辑的析取和存在性质。这推广了Nadel关于$\mathcal{L}_{ω_1, ω}$上的直觉主义逻辑的工作。当$κ$是一个正则基数使得$κ^{<κ}=κ$时，我们通过一个简单的证明修改，推导出$\mathcal{L}_{κ^+, κ, κ}$上的直觉一阶逻辑的一个完全公理化，该语言具有至多$κ$公式的析取，小于$κ$公式的合取和小于$κ$许多变量的量化.特别地，这适用于广义连续统假设下的任何正则基数。
Generalized Realizability and Intuitionistic Logic
设V是一组数论函数。我们定义了谓词公式的V -可实现性概念，使得V中函数的下标用于解释蕴涵和全称量词。本文证明了直觉谓词演算关于V -可实现的语义是合理的当且仅当V的某些自然条件成立。
Multi-topological semantics for intuitionistic modal logic
我们提出了三个例子的\textit{multi-topological}语义的直觉模态逻辑与一个模态运算符$\Box$（其行为在某种意义上像必要性）。我们表明，它是可能的处理邻域模型，前面介绍的，作为多拓扑。从邻域的角度来看，我们的方法是基于最小和最大邻域的属性之间的差异。并提出了多拓扑空间到邻域结构的变换。虽然我们的邻居可以被认为是双关系模型，我们相信，推理的邻居提供了更好的拓扑直觉。
Stable Canonical Rules for Intuitionistic Modal Logics
本文研究了直观模态逻辑的稳定公理规则，证明了多结论推论关系可由稳定公理规则 axiomatize，并以此证明了Blok-Esakia定理的替代证明及扩展，同时解决了Dummett-Lemmon猜想。
Intuitionistic modal logics: a minimal setting
本文提出一种严格包含于IK的直觉主义模态逻辑，作为最小正规直觉主义模态逻辑的候选，并探讨其设定。
Goldblatt-Thomason Theorems for Modal Intuitionistic Logics
证明了双代数直觉主义逻辑的Goldblatt-Schlason定理，并将其实例化为文献中各种模态直觉主义逻辑的Goldblatt-Schlason定理.
Mathematical semantics of intuitionistic logic
这项工作是一个数学家试图理解直觉主义逻辑。它可以从两个方面来阅读：作为一篇研究论文，穿插着对标准材料的反思的冗长离题;或者作为对一阶直觉主义逻辑的基本（但非常非传统）介绍。对于后一个目的，不需要在形式逻辑的培训，但在数学，如拓扑空间和偏序集适度识字，是假设。这项工作的主要主题是寻找一个正式的语义足以Kolmogorov的非正式解释的直觉主义逻辑（其最简单的部分是或多或少相同的所谓BHK解释）。这种搜索超越了通常的模型论，基于塔斯基的语义后果的概念，并超越了通常的形式主义的一阶逻辑，基于图式。因此，我们研究形式语义的简化版本的保尔森的元逻辑，在伊莎贝尔证明。通过构造性地解释元逻辑连接词和量词，我们得到了一个广义的模型论，它特别涵盖了直觉主义逻辑的可实现型解释。另一方面，通过分析Kolmogorov的语义后果概念（它是Tarski标准概念的替代），我们得到了替代的模型论。通过对元逻辑的扩展，我们进一步得到了一个广义的替代模型论，它足以形式化Kolmogorov的语义。另一方面，我们也制定了修改Kolmogorov的解释，这是兼容的通常，塔斯基风格的模型论。也就是说，它可以通过层值模型形式化，这是Palmgren的范畴模型的一个特例;直觉主义逻辑在这个语义上是完备的。
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$建设。因此，该文件包含两个证明削减消除，语义和句法证明。
Hypersequents and the Proof Theory of Intuitionistic Fuzzy Logic
Takeuti和Titani介绍并研究了他们称为直觉模糊逻辑的逻辑。这种逻辑被刻画为基于真假值集[0，1]的一阶Goedel逻辑。逻辑是已知的公理化，但没有演绎系统服从证明理论，因此，计算处理，已被称为。这样一个系统在这里提出，根据以前的工作hypereclithography命题哥德尔逻辑的Avron。结果表明，该系统是完善的，并允许切割消除。高野提出的一个关于Takeuti-Titani密度规则是否可消除的问题得到了肯定的回答。
Intuitionistic monotone modal logic via translation
本文通过翻译到直觉主义一阶逻辑，提出直觉主义正规模态逻辑IK的单调模态类比，给出公理化与直觉主义邻域模型语义，并比较其他直觉主义单调模态逻辑及嵌入到IK多模态版本的方法。
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)$。在直觉主义的认识框架内，可知性悖论以一种建设性的方式得到解决。我们认为，这一悖论是一个毫无根据的建设性原则的经典阅读的结果，因此并没有传统上归因于它的建设性基础的后果。
Hennessy-Milner Properties via Topological Compactness
本文给出了直觉Kripke模型下的直觉逻辑、对偶直觉逻辑和双直觉逻辑的Hennessy-Milner类，并将这些结果推广到模态（对偶和双）直觉主义逻辑.我们的主要技术工具是图像紧凑和预图像紧凑的关系，提供了一个语义描述的模态饱和度属性。
Nested Sequents for Intuitionistic Multi-Modal Logics: Cut-Elimination and Lyndon Interpolation
本文提出了一种单结论嵌套序列表演算，用于直觉多模逻辑，并证明了切消性和Lyndon插值性质。
Uniform Lyndon interpolation for intuitionistic monotone modal logic
本文证明了直觉单调模态逻辑$\mathsf{iM}$具有一致Lyndon插值性质性质（ULIP）.逻辑$\mathsf{iM}$是一种基于直觉的非正规模态逻辑，而ULIP属性是插值的加强，其中插值只依赖于蕴涵的前提或结论，并尊重命题变元的极性。我们的方法来证明ULIP产生明确的一致插值，并利用了一个终止的微积分$\mathsf{iM}$，我们已经为此目的开发。据我们所知，$\mathsf{iM}$具有ULIP和一个终止的逻辑演算的结果是第一个直觉非正规模态逻辑的结果。然而，而不是证明这些特定的结果，我们的目的是显示的建设性证明理论方法，我们用来证明ULIP的灵活性。它在过去几年中得到了发展，并已被应用于子结构，中间，经典（非）正规模态和直觉正规模态逻辑。根据这些结果，直觉非正规模态逻辑似乎是一个自然的下一类尝试应用该方法，我们在这方面迈出了第一步。
Realisability for Infinitary Intuitionistic Set Theory
我们介绍了一个基于有序图灵机（OTM）的无穷直觉集合论的可实现性语义。我们表明，我们的OTM-可实现性的概念是健全的某些系统的无穷直觉主义逻辑，并实现了所有公理的无穷Kripke-Platek集合论。最后，我们使用我们的可实现性概念的一个变体来证明（有限）直觉Kripke-Platek集合论的命题容许规则正是直觉命题逻辑的容许规则。
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公理的观点来看，它们都没有减少到另一个，尽管它们确实重叠。
Modular Models for Intuitionistic Justification Logic
我们提出的逻辑iJT 4，这是一个显式版本的直觉S4和建立健全性和完整性方面的模块化模型。
Expressing Second-order Sentences in Intuitionistic Dependence Logic
直觉依赖逻辑由Abramsky和Vaananen（2009）引入，作为Hodges（trump）团队语义的一般结构下的依赖逻辑的变体。证明了从直觉依赖逻辑句子到二阶逻辑句子的转换。本文证明了另一个方向也成立，从而直觉依赖逻辑在句子层次上等价于二阶逻辑。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。