From Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic
本文针对直觉主义命题逻辑，论证其基扩展语义涵盖了一种基于消去规则的证明论有效性版本的陈述内容，既阐释了基扩展语义的运作原理，也证明了该版本证明论有效性的完备性。
2024-09-12 cs.LO math.LO
A Lindström theorem for intuitionistic propositional logic
证明了命题直觉主义逻辑是满足某种拓扑性质的最大（就表达能力而言）抽象逻辑，这些拓扑性质包括紧性、Tarski并性质和模拟下的保持性.
2018-10-23 math.LO
Second order intuitionistic propositional logic of the real line is decidable
已知二阶直觉命题逻辑的重言式集合$\mathrm{IPC} 2$是不可判定的。本文证明了$\mathrm{IPC} 2$的公式集在实数或有理数的开子集的代数中是可判定的。
2016-12-21 math.LO
Model-theoretic characterization of intuitionistic propositional formulas
k-asimitation和asimitation的概念被引入作为k-互模拟和互模拟的非对称对应物。证明了一个一阶公式等价于一个直觉命题公式的标准平移当且仅当它对于某个k是关于k-模拟不变的，然后证明了一个一阶公式等价于一个直觉命题公式的标准平移当且仅当它对于模拟不变.最后，证明了一阶公式与直觉命题公式的标准翻译是直觉等价的，当且仅当它对于直觉模型之间的模拟是不变的.
2012-07-18 math.LO
Maximality of bi-intuitionistic propositional logic
本文采用经典一阶逻辑的Lindström定理的形式，将命题双直觉主义逻辑刻画为满足某种形式的紧性、Tarski并性质和双模拟下的保持性的极大（就表达能力而言）抽象逻辑。由于双直觉主义逻辑通过增加向后看模态的模拟在直觉设置中引入了新的复杂性，本文构成了作者在G. Badia和G.奥尔霍维科夫直觉主义命题逻辑的林斯特龙定理。Notre Dame Journal of Formal Logic，61（1）：11-30（2020）.
2021-04-07 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
The intuitionistic fragment of computability logic at the propositional level
从可计算性逻辑的语义出发，给出命题直觉演算的可靠性和完备性证明。后者将公式解释为交互式计算问题，形式化为机器与其环境之间的游戏。直觉主义蕴涵被理解为在最弱的可能性-因此最自然-意义上的算法还原，析取和合取作为问题的确定性选择组合（析取=机器的选择，合取=环境的选择），而“荒谬”作为普遍力量的计算问题。请访问http://www.cis.upenn.edu/~giorgi/cl.html以获得关于可计算性逻辑的全面在线资源。
2006-02-11 cs.AI cs.LO math.LO
First-Order Intuitionistic Logic with Decidable Propositional Atoms
用可判定命题原子扩展的直觉主义逻辑结合了命题部分的经典性质和不含命题符号的可导公式的直觉性质。序贯演算是用来作为一个框架，调查这个扩展。削减的可接受性被保留。引入了约束Kripke结构，用于对具有可判定命题原子的直觉主义逻辑进行建模.研究了分离性和存在性的程度。关于这项研究的最新信息可以在http://sakharov.net/median.html上找到。
2005-05-08 math.GM math.LO
Uniform Definability in Propositional Dependence Logic
命题依赖逻辑和探究逻辑都是表达完备的。因此，任何具有直觉析取或直觉蕴涵的公式都可以等价地翻译成命题依赖逻辑语言中的公式，而不需要这两个连接词。我们表明，虽然这样的（非成分）翻译存在，既不是直觉析取也不是直觉蕴涵是一致定义的命题依赖逻辑。
2016-11-16 math.LO
A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised
本文为直觉主义强Löb逻辑提出新相继式演算，实现强终止的向后搜索与句法消割，并在Coq中形式化验证。
2023-09-01 cs.LO math.LO
Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents
本文利用线性嵌套框架设计了一种新的直觉模糊逻辑--一阶Gödel逻辑的无割演算LNIF。线性嵌套序列-这是嵌套序列限制线性结构-证明是一个很好的证明理论的形式主义直觉模糊逻辑。我们发现，演算LNIF具有非常理想的证明理论的性质，如可逆的所有规则，结构规则的容许性，和句法切割消除。
2020-10-04 cs.LO math.LO
Carnap's problem for intuitionistic propositional logic
我们表明，直觉命题逻辑是\emph{Carnap categorical}：唯一的解释与直觉后果关系一致的连接词是标准的解释。这相对于最著名的语义学而言是成立的，直觉主义逻辑在这些语义学中是健全的和完备的;其中包括克里普克语义学、贝斯语义学、德拉加林语义学和拓扑语义学。它也适用于代数语义，尽管在这种情况下的范畴性与相对于可能世界样式语义的范畴性在种类上不同。
2022-12-25 math.LO
Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules
本文研究了Negri和von Plato对直觉主义逻辑的一种形式化，它具有一般的引入和消去规则。阐述了该系统的哲学意义。给出了适合于该系统的“极大公式”、“段”和“极大段”的定义，并给出了相应的极大公式的约简过程和极大段的置换约简过程。还考虑了所用主要方法的替代方法。证明了系统中的演绎法可以转化为范式，范式中的演绎法具有子公式性质。
2021-10-19 cs.LO math.LO
Definite Formulae, Negation-as-Failure, and the Base-extension Semantics of Intuitionistic Propositional Logic
证明理论语义学（Proof-theoretical Semantics，P-tS）是一种语义学范式，其中逻辑中的意义基于证明（而不是真理）。直觉命题逻辑（IPL）的P-tS的一个特殊实例是它的基扩展语义（B-eS）。这种语义由一个称为支持的关系给出，解释逻辑常数的含义，它由称为基础的规则系统参数化，提供原子命题的语义。在本文中，我们解释的基础上收集的明确的公式，并使用统一的证明搜索-逻辑编程（LP）的证明理论的基础-提供后者的操作视图-建立完整的IPL的B-eS。这种观点允许否定，P-tS中的一个微妙的问题，被理解为在LP中的否定失败协议。具体地说，虽然对命题的否定在传统上被理解为对命题否定的断言，但在B-eS中，我们可以将对命题的否定理解为未能找到对命题的证明，这样，断言和否定都是P-tS中的基本概念。
2023-03-28 cs.LO math.LO
De Jongh's Theorem for Intuitionistic Zermelo-Fraenkel Set Theory
证明了直觉集合论IZF的命题逻辑是直觉命题逻辑IPC。更一般地说，我们表明，IZF有德容财产方面的每一个中间的逻辑是完整的一类有限树。对于CZF也有相同的结果。
2019-05-13 math.LO
A study of cut-elimination for a non-labelled cyclic proof system for propositional dynamic logics
Graduate School of Information Sciences, Tohoku University（东北大学信息科学研究院）
本文研究了命题动态逻辑中非标记循环证明系统的消去问题，提出了序数演算和循环证明系统，并证明了其正确性和完备性，同时展示了消去失败及限制后的消去性质。
2026-03-02 cs.LO math.LO
Fixed-point elimination in the intuitionistic propositional calculus
这是现有文献的一个结果，最小和最大的单调多项式的不动点Heyting代数，即直觉命题演算的代数模型总是存在的，即使这些代数是不完整的格。原因是这些极值不动点可由IPC的公式定义。因此，基于直觉逻辑的$μ$ -演算是平凡的，每个$μ$ -公式等价于一个不动点自由公式。本文给出了公式的最小不动点和最大不动点的公理化，以及计算等价于给定$μ$ -公式的无不动点公式的算法。最大不动点的公理化是简单的。最小不动点的公理化比较复杂，特别是每个单调公式都通过Kleene迭代在有限步内收敛到它的最小不动点，但迭代次数没有统一的上界。我们从算法中提取出这样的n的上界，这取决于公式的大小。对于某些公式，我们证明了这些上界是多项式的和最优的。
2016-01-04 cs.LO math.CT math.LO
The complexity of propositional proofs
本文研究了经典重言式和直觉重言式命题证明的复杂性。事实上，我们描述了一个不确定的多项式时间决策过程的直觉蕴涵重言式。为此，我们将直觉蕴涵重言式的判定问题归结为演绎证明图的判定问题，演绎证明图是直觉蕴涵演算中证明的一种简化形式。其次，我们将演绎证明图转换成一种特殊的形式，在这种形式中，任何证明的大小都以输入公式的长度为多项式。此外，我们证明了这个过程可以扩展到所有的经典和直觉重言式，并推出一些推论，包括复杂性类和多项式有界证明系统的结果。
2017-01-18 math.LO
An analytic calculus for intuitionistic belief
直觉主义信念已经被阿特莫夫（Artemov）和普罗托波佩斯库（Protopescu）公理化为直觉主义命题逻辑的扩展，通过分配方案K和共反射$A\rightarrow\Box A$。通过这种方式，信念被解释为验证的结果，并且它适合于具有认知模态的直觉主义命题逻辑的扩展的Brouwer-Heyting-Kolmogorov解释。本文研究了直觉信念的自然演绎系统$\mathsf{IEL}^{-}$的结构性质。重点讨论了微积分的解析性，首先证明了正规化定理和子公式性质。从这些，逻辑的可判定性和一致性遵循作为推论。最后，用纯证明论的方法建立了析取性质、$\Box$ -素性和反射规则的可容许性。
2021-06-27 cs.LO math.LO
The first-order logic of CZF is intuitionistic first-order logic
证明了CZF的一阶逻辑是直觉一阶逻辑。要做到这一点，我们引入了一个新的超限计算模型（集寄存器机），并结合由此产生的概念与贝丝语义的可实现性。同时，我们还证明了CZF的命题容许规则与直觉命题逻辑的命题容许规则完全相同。
2022-06-09 math.LO
Uniform interpolation with constructive diamond
University of Amsterdam（阿姆斯特丹大学）；University of Birmingham（伯明翰大学）；University of Melbourne（墨尔本大学）
本文通过构造性方法证明构造性K（CK）和Wijesekera的K（WK）具有均匀插值性质，填补了直觉主义模态逻辑中独立box和diamond算子均匀插值研究的空白。
2026-05-27 cs.LO math.LO
Nested Sequents for Intuitionistic Multi-Modal Logics: Cut-Elimination and Lyndon Interpolation
本文提出了一种单结论嵌套序列表演算，用于直觉多模逻辑，并证明了切消性和Lyndon插值性质。
2025-11-27 cs.LO math.LO
Intuitionistic Sahlqvist theory for deductive systems
本文将 Sahlqvist 理论扩展至包含合取连接词的直觉主义命题演算片段，引入了适用于任意原代数演绎系统的直觉主义 Sahlqvist 理论，并据此为包含蕴涵连接词的演算片段及直觉主义线性逻辑扩展导出了 Sahlqvist 定理。
2022-08-01 math.LO
Ruitenburg's Theorem via Duality and Bounded Bisimulations
对于给定的直觉命题公式A和出现在其中的命题变元x，定义公式{A\_i}的无穷序列|i $\ge$ 1}，设A1为A，A1 + 1为A（A1/x）。Ruitenburg定理[8]指出序列{Ai}（模逻辑等价）最终是周期为2的周期性的，即存在N个$\ge$ 0使得A N +2 $\leftrightarrow$ A N在直觉命题演算中是可证明的。我们给出了这个定理的语义证明，使用对偶技术和有界互模拟行列。
2018-04-17 cs.LO math.LO
Propositional Mixed Logic: Its Syntax and Semantics
在本文中，我们提出了一个命题逻辑（称为混合逻辑）包含不相交的副本的最小，直觉和经典逻辑。我们证明了这个逻辑的Kripke语义的完备性定理。建立了混合逻辑与极小逻辑、直觉逻辑和经典逻辑之间的关系。最后，我们提出了这个逻辑的微积分版本。
2009-05-04 math.LO
Failure of Higher-Order Truth within Intuitionistic Propositional Logic
University of Cambridge（剑桥大学）
本文否定回答了所有Heyting代数能否作为初等拓扑斯的次终端对象格出现的问题，证明了两生成元的自由Heyting代数无法成为该类Heyting代数，相关结果借助ChatGPT 5.6 Sol获得。
2026-09-04 math.CT math.LO
On the Jaśkowski Models for Intuitionistic Propositional Logic
在1936年，Stanislaw Jakowski给出了一个建设的一个有趣的序列，他所谓的“矩阵”，我们今天将所谓的“有限海廷代数”。然后，他给出了一个非常简短的证明，如果一个命题公式在这些代数中的每一个中成立，那么它在直觉命题逻辑（IPL）中是可证明的。这个草图只是描述了命题公式的某种范式，并给出了一个非常简洁的归纳论证的轮廓，表明范式中的一个不可证明的公式可以在一个代数中被反驳。不幸的是，如何从这个草图中恢复一个完整的证明还远不清楚。20世纪50年代初，Gene F.罗斯给出了详细的证明Jakowski的结果，仍然使用的概念矩阵，而不是Heyting代数，基于一个正常的形式，这是更严格的一个Jakowski提出。然而，玫瑰的文件是指他的论文的额外细节，特别是关于正常形式。本文用现代术语和一个更像Jakowski的正规形证明了Jakowski的结果。我们还证明了正常形式的语义属性，使我们能够提供另一种证明IPL的Heyting代数语义的完整性。我们概述了IPL的决策程序，我们的证据的基础上，并说明它在行动上的一些简单的例子。
2020-12-22 math.LO
Cut-free Deductive System for Continuous Intuitionistic Logic
本文提出了一种无割推理论系统，用于连续直觉逻辑，通过代数方法证明了其完备性和割可接受性。
2026-02-05 cs.LO math.LO
Intuitionistic Logic and Muchnik Degrees
我们证明，有一个因素的Muchnik格，捕捉直觉命题逻辑。这补充了现在经典的结果Skvortsova梅德韦杰夫格。
2010-03-23 math.LO
Cut elimination for propositional cyclic proof systems with fixed-point operators
本文研究带不动点算子或归纳定义的命题循环证明系统，证明其与无穷式系统可证明性等价，并因此具有无切割完备性。
2024-10-29 cs.LO math.LO
Simple example of weak modal logic based on intuitionistic core
在本文中，我们提出了一个简单的命题逻辑的例子，它有一个模态算子，是基于直觉的核心。这个系统在模态意义上是非常弱的-例如规则性或单调性不成立。它具有完备的语义，由具有邻域和预序关系的可能世界构成。我们讨论了对这些结构施加的某些限制。此外，我们提出的特征公理4已知的逻辑S4。
2018-06-25 cs.LO math.LO
Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
本文首次探索子结构逻辑的证明论语义，提出直觉主义乘法线性逻辑（IMLL）的基础扩展语义，其中逻辑常量定义均采用消去规则形式，并证明了其可靠性与完备性。
2024-11-12 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
Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic
本文提出共诱导证明搜索方法，扩展至偏极直觉逻辑LJP，并通过解释将该方法应用于其他直觉逻辑系统，实现了解的可判定性继承。
2025-12-04 cs.LO math.LO
From Intuitionism to Many-Valued Logics through Kripke Models
直觉命题逻辑是由Kurt Gödel（1932）证明的无限多值逻辑，它是由Stanismartaw Jaumkowski（1936）证明的可数多值逻辑。在本文中，我们使用Saul Kripke（1959）的模型为这些定理提供了另一种证明。哥德尔的证明产生了一个中间命题逻辑（介于直觉主义和经典之间），现在被称为哥德尔或哥德尔-达米特逻辑，也被模糊逻辑学家研究。我们还提供了一些结果，在此逻辑命题连接词的可定义性。
2020-08-20 cs.LO math.LO
On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems
本文展示了如何从命题直觉逻辑和一阶直觉逻辑的常量域的标记演算中导出嵌套演算，从而将标记演算的一般结果与嵌套序列的更精细形式联系起来。从标记演算中提取嵌套演算是通过消除标记推导中的结构规则来实现的。提取过程的每个方面都是有动机的和详细的，表明每个嵌套演算从其相关的标记演算继承了有利的证明理论属性。
2020-02-03 cs.LO math.LO
Undecidability of the problem of recognizing axiomatizations for implicative propositional calculi
在本文中，我们考虑命题演算，这是可公理化的直觉蕴涵命题演算的扩展连同肯定前件和替换规则。我们证明了下列问题的不可判定性：给定的有限命题公式集是否构成一个固定的命题演算的适当公理系统。此外，我们证明了同样的以下限制这个问题：是否一个给定的有限集定理的一个固定的命题演算推导出所有定理的演算。这些结果的证明是基于减少的不可判定的停机问题的标签系统介绍后。
2014-07-25 cs.LO math.LO
On the number of variables in undecidable superintuitionistic propositional calculi
本文构造了一个不可判定的3-变量超直觉命题演算，直觉命题演算的可公理化扩展，公理仅包含3个变量。由于不存在2-变量超直觉命题演算，这是变量的最小可能数量。
2015-11-06 math.LO
Modal meet-implication logic
本文扩展命题直觉主义逻辑的 meet-implication 片段，引入保持 meet 的模态，基于半格给出语义并建立对偶性，获得完备性，识别共同模态片段，并证明其为 dialgebraic 逻辑，进而获得某处可表达性。
2022-07-13 cs.LO math.LO
Proof complexity of intuitionistic implicational formulas
本文在直觉命题逻辑（IPC）证明复杂性的背景下研究蕴涵公式。一方面，我们给出了一个有效的重言式到蕴涵重言式的转换，该转换保持了直觉扩展Frege（EF）或替换Frege（SF）证明的多项式长度。另一方面，在IPC的蕴涵片段中的EF证明多项式地模拟了蕴涵重言式的完全直觉主义逻辑。在一定条件下，这些结果也适用于其他超直觉逻辑的其他片段。特别地，Hrubeeland \cite{hru:lbint}的直觉EF证明的长度的指数下界，由Jeanábek \cite{ej:sfef}推广到无界分支的超直觉逻辑中EF和SF系统之间的指数分离，可以通过蕴涵重言式实现。
2016-09-18 cs.LO math.LO
Fundamental Propositional Logic with Strict Implication
Institute of Philosophy, Chinese Academy of Sciences（中国科学院哲学研究所）；School of Humanities, University of Chinese Academy of Sciences（中国科学院大学人文学院）
本文在公理命题逻辑中引入严格蕴含，探讨其对语义蕴含关系的影响，并为两种逻辑系统提供了公理化和完备性定理。
2026-01-31 math.LO
On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains
常域逻辑是直觉主义逻辑，它用所谓的全移位公理（forall-shift axiom）进行了扩展，这是一个经典有效的命题，蕴涵了可判定公式上的排中律。令人惊讶的是，这种逻辑是建设性的，到目前为止，这已经证明了削减消除特设的结石。在这里，我们使用自然演绎和Curry-Howard对应的方法来提供一个简单的计算解释的逻辑。
2018-10-18 cs.LO math.LO
Intuitionistic Existential Graphs from a non traditional point of view
在这篇文章中，我们发展了Arnol Oostra [4]提出的直觉主义存在图的一个新版本。本文中提出的演绎规则与Yuri Poveda [5]的工作中描述的规则具有相同的含义，因为根据切割奇偶性的演绎被消除，并被递归规则的有限集所取代。这样，直觉命题逻辑的存在图系统$ Alfa_I $遵循Poveda [5]描述的系统$ Alfa_0 $的演绎规则的过程，并且等价于直觉命题演算。在这种表示中，$ Alfa_0 $系统得到了改进，引入了一系列以前没有考虑过的二次演绎规则，这些规则允许更好地管理演绎，最后，从Van Dalen [6]提出的思想出发，在演绎技术中引入了一种混合物，Gentzen系统的自然演绎与新的系统规则$ Alfa_0 $和$ Alfa_I $相结合。为$Alfa_I$表示提出的符号将图的通常拓扑的开集、闭集和准开集与直觉命题逻辑联系起来，这对于从更几何的角度来处理这种逻辑表示中的新问题是有用的。
2017-05-26 math.LO
Propositional Calculus in Coq
我正式的经典命题逻辑在证明辅助Coq的重要定理。主要证明了（1）自然演绎演算的可靠性和完备性，（2）自然演绎演算与Hilbert系统和Hilbert演算的等价性，（3）Hilbert演算的割消元。
2015-03-31 cs.LO math.LO
An Intuitionistic Formula Hierarchy Based on High-School Identities
我们通过采用公式作为指数多项式的观点来重新审视直觉等价和形式证明表示的概念。在观察到大多数的可逆证明规则的直觉（最小的）命题演算是公式（即）同构对应的高中身份，我们可以得到一个更紧凑的变体的证明系统，只包括不可逆的证明规则，其中可逆的证明规则已被替换的公式规范化过程。此外，对于某些证明系统，如Vorob'ev，Hudelmaier和Dyckhoff的G4 ip微积分，甚至可以将所有的不可逆证明规则视为指数多项式之间的严格不等式;为了建立这一事实，给出了仔细的组合处理。最后，我们扩展了指数多项式类比的一阶量词，表明它产生了一个直观的层次结构的公式，类似于经典的算术层次结构，第一个分类公式，同时保持同构。
2018-08-12 cs.LO math.LO
A cut-free sequent calculus for the bi-intuitionistic logic 2Int
本文的目的是引入一个双直觉的代数演算，并给出其结构规则的可容许性证明。我将介绍的演算，称为SC2Int，是双直觉主义逻辑2Int的一个微积分。这种逻辑的演算代表了一种双边主义的推理，因为它们不仅内化了验证或可证明性的过程，而且内化了证伪或所谓的对偶可证明性方面的对偶过程。2Int的自然演绎演算的一个范式定理已被证明，本文想证明SC 2Int的一个割消定理，即如果成功，这将推广已有的结果.
2020-09-23 cs.LO math.LO
Sequent-style tableaux for intuitionistic propositional logic
University of Calabria（卡拉布里亚大学）
本文提出用于直觉主义命题逻辑的块演算$\boldsymbol{B}_{ti}$，证明其为多后件相继式演算$\boldsymbol{G}_{ti}$的倒置形式，且相对于克里普克语义可靠完备，具有有限模型性质与析取性质的块理论证明。
2026-08-24 math.LO
How Much Propositional Logic Suffices for Rosser's Essential Undecidability Theorem?
在本文中，我们探讨了以下问题：如何弱可以是一个逻辑的Rosser的本质不可判定性的结果是可证明的弱算术理论？众所周知，Robinson的Q在直觉主义逻辑中是本质不可判定的，而P.Hajek在模糊逻辑BL中证明了它对于Q的Grzegorczyk变体，它把算术运算解释为非完全的非函数关系。我们提出了一个证明的基本不可判定性在一个弱得多的子结构逻辑和一个弱得多的算术理论，一个版本的罗宾逊的R（算术运算也被解释为纯粹的关系）。我们的结果是基于结构版本的不可判定性参数介绍了克莱因，我们表明，它远远超出了范围的布尔，直觉，或模糊逻辑。
2020-06-18 math.LO
Intuitionistic fixed point theories over Heyting arithmetic
本文证明了一个关于不动点的直觉理论对于一类公式在Heyting算法上是保守的。这部分地扩展了我的结果。证明的灵感来自于G.薄荷糖
2010-05-12 math.LO
Intuitionistic Dynamic Logic
University of Bern（伯尔尼大学）；Ghent University（根特大学）
研究直觉主义动态逻辑的数学理论，涵盖五种该逻辑。通过开发证明论工具、进行语义研究，建立相关性质与界限。主要贡献为开发演算、获有限模型性质及可判定性、给出直觉主义线性时态逻辑完备公理系统。
2026-07-16 cs.LO math.LO
Universal Proof Theory: Feasible Admissibility in Intuitionistic Modal Logics
在本文中，我们介绍了一个一般家庭的序列式演算的模态语言及其片段，以捕捉所有建设性的可接受的系统的本质。称这些演算为\emph{constructive}，我们表明，任何足够强的建设性的微积分，满足一个温和的技术条件，可行地承认所有的Visser规则，即，有一种多项式时间算法，它读取维塞尔规则的前提的证明，并为其结论提供证明。作为一个积极的应用，我们证明了Visser规则在直觉模态逻辑的几个演算中的可行容许性，这些演算包括$\mathsf{CK}$，$\mathsf{IK}$及其由模态公理$T$，$B$，$4$，$5$，有界宽度和深度的模态公理以及命题逻辑的扩展。在消极的一面，我们表明，如果一个足够强大的直觉模态逻辑（满足一个温和的技术条件）不承认至少一个Visser的规则，那么它不能有一个建设性的逻辑演算。因此，除了$\mathsf{IPC}$之外，没有中间逻辑具有构造性的构造演算。
2022-10-16 cs.LO 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
The Order-Theoretic Structure of Free Heyting Algebras
我们发现了n元直觉命题逻辑的Lindenbaum代数的序论刻画。
2007-03-28 math.LO
