Effect of the Choice of Connectives on the Relation between the Logic of Constant Domains and Classical Predicate Logic
不仅经典语义学可以推广，直觉Kripke语义学也可以推广，从而可以处理任意由真假值表或真假值函数表征的命题连接词。在我们以前的工作中，已经证明了Kripke有效命题序列集和经典有效命题序列集重合当且仅当所有可用的命题连接词都是单调的。本文将这一结果推广到一阶逻辑，证明了在谓词逻辑中，所有可用的命题连接词都是单调的条件是在所有常数域Kripke模型中有效的序列集，而不是Kripke有效序列集和经典有效序列集重合的充要条件.
2021-07-08 math.LO
Some abstract versions of Gödel's second incompleteness theorem based on non-classical logics
我们研究哥德尔第二不完备性定理的抽象版本，并制定了Löb的可导性条件的推广，适用于比经典逻辑弱的逻辑。我们隔离哥德尔定理中的收缩规则的作用，并给出一个基于模态逻辑的系统的（玩具）例子，没有收缩使哥德尔的论点无效。
2016-02-18 math.LO
Theories of truth for countable languages which conform to classical logic
每一个符合经典逻辑的可数语言都有一个符合经典逻辑的扩张，并有一个定义的真理论。如果客体语言的每一个句子都被它的意义评价为真或假，那么这种延伸就有一种语义学的真理论。这些理论包含真值谓词和非真值谓词。当客体语言的句子被它们的意义所评价时，理论是等价的。
2020-02-03 math.LO
Automorphisms of the Lattice of Classical Modal Logics
本文分析了最小经典模态逻辑系统E的命题扩张，它们构成一个格CExtE。我们的分析方法使用代数计算与规范形式，这是一个推广的规范形式适用于正常的模态逻辑。作为应用，我们确定了CExtE的一个自同构群，它同构于对称群S4。
2021-03-23 math.LO
On the Various Translations between Classical, Intuitionistic and Linear Logic
University of Lisbon（里斯本大学）；Queen Mary University of London（伦敦玛丽女王大学）
本文以直觉主义线性逻辑的扩张为共同基础，提出统一方法设计和简化经典、直觉主义与线性逻辑之间的证明翻译，并由此重新得到文献中多数著名翻译。
2025-11-10 math.LO
Cut elimination, identity elimination, and interpolation in super-Belnap logics
我们开发了一个根岑式的证明论的超贝尔纳普逻辑（四值邓恩-贝尔纳普逻辑的扩展），扩大了Pynko发起的方法。我们表明，正如子结构逻辑可以理解为证明理论上的逻辑放松经典逻辑的结构规则，但保持其逻辑规则以及规则的身份和切割，超贝尔纳普逻辑可以被视为逻辑放松身份和切割，但保持逻辑规则以及结构规则的经典逻辑。然后证明了经典命题逻辑的割消定理的推广，并用于建立各种超贝尔纳普逻辑的插值。特别是，我们获得了另一种改进的克雷格内插定理经典命题逻辑最近发现的米尔恩语法证明。
2018-03-10 math.LO
Recursive inseparability of classical theories of a binary predicate and non-classical logics of a unary predicate
本文通过骨牌问题提取递归不可分性，间接证明了有界语言中经典与非经典一阶逻辑各种片段的不可判定性，涵盖二元谓词经典逻辑、模态及超直觉主义谓词逻辑的单调片段。
2025-05-01 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
Truth-value semantics and functional extensions for classical logic of partial terms based on equality
我们开发了一个自下而上的方法，真假值语义的经典逻辑的部分条款的基础上平等和应用它来证明的保守性，除了部分描述和部分选择功能，独立于任何严格的假设。
2012-12-01 math.LO
Classical Logic without Bivalance
University of Southampton（南安普顿大学）；University College London（伦敦大学学院）
本文提出一种经典逻辑无二值性的语义学框架，解决了元数学中的 ω-不完全性问题，并通过普通归纳法给出了皮亚诺算术的一致性证明。
2026-03-06 math.LO
Valuation semantics for first-order logics of evidence and truth (and some related logics)
本文介绍了逻辑$QLET_{F}$，证据和真理逻辑$LET_{F}$的量化扩展，以及相应的声音和完整的一阶非确定性赋值语义。$LET_{F}$是一个次协调和次完全的逻辑，它用一个经典算子${\circ}$和一个非经典算子$\bullet$扩展了一级蕴涵逻辑（$FDE$），它们彼此对偶：当${\circ} A$要求$A$行为经典时，${\bullet} A$从$A$违反一些经典有效的推论中得出。$QLET_{F}$的语义结合了解释否定谓词的反扩展与一阶非确定性赋值的结构，并通过Henkin方法的推广获得完整性。通过为$FDE$，$K3$和$LP$的一阶扩展提供健全和完整的语义，我们展示了这些工具，我们在这里称之为“反扩展+赋值”的方法，可以自然地应用于一些非经典逻辑。
2021-06-18 math.LO
Wright's Strict Finitistic Logic in the Classical Metatheory: The Propositional Case
克里斯平·赖特在他1982年的论文中主张严格有限主义，这是一种比直觉主义更具限制性的建设性观点。在附录中，他提出了严格有限算术的模型。它们是树状结构，形成于他严格的有限元理论，数字之间的方程，具体的算术句子进行评估。作为第一步，对经典形式化的严格有限性，我们提出了一个额外的假设，在经典的元理论的同行，然后提取命题的一部分，“严格有限逻辑”，从它和调查。我们将提供一个健全和完整的Kripke风格的语义和一个演算，并与其他逻辑比较。这种逻辑缺乏排中律和前件式，弱于经典逻辑，但在定理性上强于任何真正的中介逻辑。事实上，所有其他著名的经典定理都被发现是定理。最后，我们将观察到这种语义的模型可以被看作是直觉模型的节点。
2023-01-28 math.LO
Variants into minimal logic of the Kuroda negative translation
黑田的否定翻译只把经典逻辑翻译成直觉主义逻辑，而不是最小逻辑。我们提出了八个变种的黑田否定翻译，翻译经典逻辑，甚至到最低限度的逻辑。他们的可靠性定理的证明是有趣的，因为他们说明了四种不同的证明方法。
2013-04-11 math.LO
Locality for Classical Logic
在本文中，我们将看到演绎系统的经典命题和谓词逻辑的演算结构。像随机系统一样，它们有一个可接受的截规则。此外，它们具有自顶向下的对称性和一些在微积分中不可用的导子的标准形式。同一性公理、切割、弱化和收缩都可以被简化为原子形式。这导致规则是局部的：它们不需要检查无限大小的表达式。
2003-01-27 math.LO
Projectivity meets Uniform Post-Interpolant: Classical and Intuitionistic Logic
本文研究经典与直觉主义命题逻辑中投射性与一致后插值的关系，证明经典逻辑中二者对所有公式等价，并给出直觉主义逻辑的Kripke语义刻画，进而证明某些直觉主义逻辑扩张的统一类型是有穷的。
2024-03-29 math.LO
Expressive power of basic modal intuitionistic logic as a fragment of classical FOL
本文讨论了模态直觉主义逻辑的Kripke式语义的四种不同版本所导出的一阶逻辑片断。为了捕捉这些片段，asimulation的概念进行了修改和扩展，以产生Van Benthem类型的语义表征各自的表达能力。它示出，进一步，这种特征可以很容易地进行到任意一阶可定义的子类的经典一阶模型。
2015-11-06 math.LO
Non deterministic classical logic: the $λμ^{++}$-calculus
本文给出了$λμ$ -演算的一个扩展，称为$λμ^{++}$ -演算，它具有以下性质：主题约简，强规范化，数据表示的唯一性，从而只在数据类型上融合。这种演算也允许对并行或进行编程。
2009-05-04 math.LO
Epsilon Theorems in Intermediate Logics
任何中间命题逻辑（即，包括直觉主义逻辑并包含在经典逻辑中的逻辑）可以被扩展到具有π-和τ-算子以及临界公式的微积分。对于经典逻辑，这导致希尔伯特的$\varepsilon$ -演算。经典逻辑的第一和第二$\varepsilon$ -定理建立了$\varepsilon$ -演算在其经典基本逻辑上的保守性。众所周知，第二个$\varepsilon$ -定理对于直觉的$\varepsilon$ -演算是失败的，因为预解是不可能的。本文研究了添加临界$\varepsilon$ -和$τ$ -公式以及将量词翻译成$\varepsilon$ -和$τ$ -项对中间逻辑的影响。它表明，保守性的命题基础逻辑也持有这样的中间$\varepsilonτ$ -演算。“扩展的”第一$\varepsilon$ -定理在基逻辑是有限值哥德尔-达米特逻辑时成立，否则不成立，但对无限值哥德尔逻辑中的某些可证明公式成立。第二个$\varepsilon$ -定理也适用于有限值一阶哥德尔逻辑。用于证明无限值哥德尔逻辑的扩展的$\varepsilon$ -第一定理的方法建议应用于算术理论。
2021-11-30 math.LO
Yet another proof of Goedel's completeness theorem for first-order classical logic
给出了一阶经典逻辑关于直觉序列的Genzten演绎规则的极小集合（特别是缺失的截规则）的完备性的Henkin式证明.可满足性定理坚持对推导规则的保留，认为它需要比完备性定理更弱的假设，缺少的要求恰好是规则~ p --> p，这从经典的角度暗示了直觉主义的动机。一个裸露的治疗标准，基本的一阶语法不知何故更多的代数味道比平常也给。
2009-10-11 math.LO
Propositional Mixed Logic: Its Syntax and Semantics
在本文中，我们提出了一个命题逻辑（称为混合逻辑）包含不相交的副本的最小，直觉和经典逻辑。我们证明了这个逻辑的Kripke语义的完备性定理。建立了混合逻辑与极小逻辑、直觉逻辑和经典逻辑之间的关系。最后，我们提出了这个逻辑的微积分版本。
2009-05-04 math.LO
Notion of validity for the bilateral classical logic
本文通过引入Prawitz的有效性概念，为双边经典逻辑（BCL）提供全面辩护，利用不动点构造解决RAA循环性问题，证明经典逻辑的辩护无需依赖排中律。
2023-10-20 math.LO
Classical Logic = Fibred MLL
本文将经典的命题证明表示为 * 组合证明 *，这比证明网更抽象：叠加（收缩/弱化）在数学上被建模为纤维化的松散形式，而不是语法（如在证明网中，涉及收缩和弱化节点）。一个组合证明是一个“被证明的”乘法线性证明网，因此标题中的口号。割消法保留了它来自微积分的丰富性：它的非决定性不会崩溃而成为融合。[Note：这仅仅是一个2页的概要，接受在计算机科学逻辑'05的简短介绍。
2005-04-01 math.LO
Classical propositional logic and decidability of variables in intuitionistic propositional logic
我们改进了这个问题的答案：当一个公式中的命题变元在经典命题逻辑中是可证明的时候，在直觉主义命题逻辑中，什么样的被排除的中间集足以证明这个公式。
2014-08-06 cs.LO math.LO
Negation and Implication in Partition Logic
布尔子集逻辑，通常被称为“命题逻辑”，被认为是“经典的”，而直觉主义逻辑和许多子逻辑和分支是“非经典的”。但还有另一种数理逻辑，即划分逻辑，它与布尔子集逻辑处于同一数学层次，因为子集和商集（划分或等价关系）在范畴论意义上是彼此对偶的。我们在这里的目的是探讨在其他数理逻辑的分区的否定和蕴涵的概念。
2020-07-10 math.LO
Tarskian classical relevant logic
塔斯基经典相关逻辑TR起源于塔斯基关于关系演算的基础和限制于多个变量的一阶逻辑的工作，由塔斯基和吉万特在他们的书《无变量的集合论的形式化》中提出，并在前九节中总结。TR与著名的逻辑KR密切相关。在塔斯基的二元关系扩展一阶逻辑中，关联逻辑的每一个公式都有一个对应的语句，关系符号上有运算符。公式在TR中（根据定义），或在KR中（根据定理），当且仅当其相应的句子可以在一阶逻辑中证明，使用最多四个变量，假设所有二元关系都是稠密的，并且对于TR，复合可换，或者对于KR，是对称的。TR的词汇表与Meyer和Quilley提出的经典相关逻辑CR $^*$相同，但TR适当地包含CR $^*$。TR的特征帧是CR $^*$的特征帧并且满足额外帧条件。在TR中有一些公式（但在CR $^*$中没有）与这个框架条件相对应，并为T的定理提供了一个反例。科瓦尔斯基TR或KR的特征框架是其复代数分别是交换或对称的整数稠密关系代数的框架。对于这两个类，同构类型的数量像三元关系的同构类型的数量一样增长。这两个类的渐近公式。类似的结果也适用于由相应句子的一阶证明中使用的变量数量定义的逻辑层次。
2020-09-26 math.LO
The most natural paradefinite logic relative to classical logic
University of Amsterdam（阿姆斯特丹大学）
本文提出，相对于经典逻辑，Belnap-Dunn逻辑通过添加否定和蕴含连接词来形成最自然的悖论定义逻辑。
2026-02-11 cs.LO math.LO
From translations to non-collapsing logic combinations
针对不同逻辑组合易坍缩的问题，提出基于保守翻译的通用共存组合方法，证明组合逻辑是原逻辑的保守扩展且可诱导根岑演算、满足可靠完全性条件，并通过三类逻辑组合验证其有效性。
2025-04-14 math.LO
On three-valued presentations of classical logic
本文研究了在五种单调三值后承关系下，何种三值真值表方案能使所得逻辑恰与经典逻辑一致，并给出了各情形下的完整刻画。
2023-12-26 math.LO
On Intermediate Justification Logics
我们研究抽象的中间证明逻辑，即任意的中间命题逻辑扩展的（经典）证明逻辑的特定公理的子集。对于这些，我们介绍了各种语义相结合，无论是海廷代数或Kripke框架与通常的语义机器所使用的Mkrtychev的，拟合的或莱曼的和Studer的模型为经典的理由逻辑。我们证明了统一的完整性定理，所有中间的理由逻辑和相应的语义使用相应的命题完整性定理的基础中间逻辑。进一步，通过对Fitting方法的改进，我们证明了一大类中间证明逻辑和伴随的中间模态逻辑的统一实现定理。
2020-08-16 math.LO
Preservation under Reduced Products in Continuous Logic
本文提出连续逻辑中一种在缩减积下保持的片段，扩展了经典理论在保持性和稳定性方面的结果，并通过保持性质表征了相关片段。
2026-01-15 math.LO
Logic of paradoxes in classical set theories
集合论的悖论有一个共同的根源--缺乏对为什么某些集合不是集合的理解。为什么大量的思维对象本身不能成为思维对象？此外，这是一个合乎逻辑的真理，这样的群众确实存在。然而，我们对这个逻辑真理的理解并不像我们对逻辑真理$\forall x \ x=x$的理解那样透彻。在本文中，我们阐述了一个逻辑真理，我们称之为生产力原理。Bertrand Rusell是第一个提出这一原则的人，但形式有限，目的不同。这一原则阐明了一种逻辑机制，这种机制隐藏在矛盾的群体背后，并且与任何简单的逻辑真理一样可以理解。但是，它没有解释集合的概念。它只在经典的二值$\in$语言的框架内设置概念的逻辑边界。这一原则的行为就像是我们用来解释和描述集合的任何理论的逻辑调节器。它提供了识别理论内部矛盾类的工具。我们展示了如何从生产力原理已知的悖论类，以及如何原则给我们一个统一的方式来产生新的悖论类。在$ZFC$集合论的情况下，生产力原理表明，大小原理的局限性具有限制性的性质，它们不能解释哪些类是集合。生产力原理作为一种逻辑调节器，在发展相容的集合论的过程中可以起到一定的启发作用。我们勾勒出这样一个理论--集合的累积基数理论。
2021-05-28 math.LO
Isomorphic Formulae in Classical Propositional Logic
公式之间的同构是相对于在经典命题逻辑和经典线性命题逻辑的乘法片段捕获的证明网的形式化相等的演绎的范畴来定义的。这种平等是由演绎的一般性所驱动的。刻画给出了对同构公式，从而导致决策程序，这种同构。
2010-10-04 math.CT math.LO
A classical-logic view on a paraconsistent logic
本文研究次协调一阶逻辑 LPQ$^{\supset,\mathsf{F}}$，提出其自然演绎证明系统，通过嵌入一阶经典逻辑提供模型论与逻辑论证，并探讨其可判定性及逻辑性质，揭示其与经典逻辑的紧密联系。
2025-09-16 cs.LO math.LO
Mixed Logic and Storage Operators
1990年，J-L. Krivine引入了存储操作符的概念。它们是$λ$ -模拟按名称调用策略中的按值调用的术语，并且它们可以用于对赋值指令进行建模。J-L Krivine利用经典逻辑到直觉主义逻辑的哥德尔转换证明了在AF 2型系统中存在一个非常简单的二序型的存储算子。为了使控制算子模型化，J-L. Krivine将系统AF 2扩展到经典逻辑。在他的系统的财产的唯一性的整数表示是失去了，但他表明，存储运营商类型的系统AF 2可以用来找到价值的经典整数。在本文中，我们提出了一个新的经典类型系统的基础上的逻辑系统称为混合逻辑。我们证明，在这个系统中，我们可以表征，由类型，存储运营商和控制运营商。在M. Parigot的$λμ$ -微积分。
2009-05-06 math.LO
Regular non-normal modal classicalities
本文提出了一种基于一致性算子的四值布尔逻辑B_4^∘，并扩展其到模态逻辑中，揭示了非正常全局推理关系及新的可及性类型。
2026-02-23 math.LO
Kripke Models for Classical Logic
我们引入了经典逻辑的Kripke模型的概念，并构造性地证明了它的可靠性和无割完备性。我们讨论的概念和它的潜在应用的新颖性。
2010-06-07 cs.LO math.LO
Classical Logic as Intuitionistic Logic with Duality
University of Southampton（南安普顿大学）；University College London（伦敦大学学院）
本文通过将原子命题替换为字面量并引入原始对偶性，提出一种基于证明论语义的经典逻辑替代方案，表明经典逻辑可视为直觉主义逻辑加上对偶性原则。
2026-10-06 cs.LO math.LO
Interpolation in Non-Classical Logics
Institute of Computer Science of the Czech Academy of Sciences（捷克科学院计算机科学研究所）
本文探讨了非经典逻辑中插值性质的差异，分析了多种逻辑系统中的插值特性及重要实例。
2025-12-01 cs.LO math.LO
Homotopies in Classical and Paraconsistent Modal Logics
模态逻辑的拓扑语义最近在逻辑的许多不同分支中获得了新的动力。在本文中，我们将考虑经典和次协调模态逻辑的拓扑语义。本文的工作是从几何和拓扑的角度研究次协调系统的一个新的进展。在这里，我们讨论了在次协调和经典模态情况下的函数变换：如何将一个经典或次协调拓扑模型变换为另一个模型，如何以保持有效性的方式将一个变换变换为另一个变换。此外，我们还建议采取措施来跟踪这种变化。
2011-07-25 cs.LO math.LO
Embedding and Automating Conditional Logics in Classical Higher-Order Logic
University of Torino（都灵大学）；Freie Universität Berlin（柏林自由大学）；King’s College London（伦敦国王学院）；University of Luxembourg（卢森堡大学）
提出了一种将条件逻辑完全嵌入到经典高阶逻辑中的方法。这种嵌入使得现成的高阶自动定理证明器和模型查找器能够应用于条件逻辑中的推理和关于条件逻辑的推理。
2011-08-17 cs.AI cs.LO math.LO
A modal logic amalgam of classical and intuitionistic propositional logic
由哥德尔在1932年提出并由麦肯锡和塔斯基在1948年证明的一个著名的结果是：$φ$是直觉命题逻辑IPC的一个定理当且仅当它的哥德尔翻译$φ'$是模态逻辑S4的一个定理。在本文中，我们扩展了在我们的前一篇文章（S. Lewitzka，Algebraic Semantics for a Modal Logic Close to S1，J. Logic and Comp.，doi：10.1093/logcom/exu 067），并证明了：命题公式$φ$是IPC的一个定理当且仅当$\squareφ$是L的一个定理（实际上，我们证明了：$Φ\vdash_{IPC}φ$当且仅当$\squareΦ\vdash_L\squareφ$，对于命题$Φ,φ$）.因此，映射$φ\mapsto\squareφ$是IPC到L中的嵌入，即L包含IPC的副本。此外，L是经典命题逻辑CPC的保守扩展。在这个意义上，L是CPC和IPC的混合物。证明了L是完备的。一类具有（非正规）模态算子的特殊Heyting代数。
2015-06-03 cs.LO math.LO
Relevant Reasoners in a Classical World
我们开发了一个框架，认知逻辑相结合的相关模态逻辑与经典命题逻辑。在我们的框架中，代理建模为推理根据相关的模态逻辑，而我们的逻辑的命题片段是经典的。为了实现这一功能，我们修改了相关模态逻辑的关系语义，使模型的有效性被定义为满足整个一组指定的状态，就命题连接词而言，表现得像经典的可能世界。本文的主要技术成果是一个模块完整性定理参数化的相关模态逻辑形式化代理的推理。
2022-06-07 cs.LO math.LO
On an ordinary expansion of first-order Belnap-Dunn logic
Informatics Institute, Faculty of Science, University of Amsterdam（阿姆斯特丹大学科学学院信息学研究所）
本文提出了一种第一阶Belnap-Dunn逻辑的扩展，通过经典逻辑等价律区分其与其他逻辑，并探讨其在处理归纳机器学习中的不一致和不完整性方面的潜力。
2026-03-03 cs.LO math.LO
Quantum Logic as Classical Logic
我们提出了一个语义表示的标准量子逻辑QL在一个经典的，正常的模态逻辑，这通过一个格嵌入正交模格到布尔代数与一个模态算子。因此，我们的经典逻辑是量子逻辑QL的一个完善。换句话说，我们驳斥了伯克霍夫和冯·诺依曼的经典论点，即量子力学的逻辑（形式特征）将是非经典的，以及普特南的论点，即量子逻辑（他的同类）将是一般命题推理的正确逻辑。量子力学的命题逻辑是模态的，但却是经典的，命题推理的正确逻辑不需要具有外向的量子特征。一个正常的必然模态足以捕捉量子实验中观察的主观性，这要归功于它未能在经典析取上分布。我们结果的关键是把量子否定转化为可观测性的经典否定。
2017-02-07 cs.LO math-ph math.LO
Merging fragments of classical logic
我们调查的可能性扩展的非功能完整的逻辑的布尔连接词的集合，通过添加进一步的布尔连接词，使所得到的连接词功能完整。更确切地说，我们将有兴趣检验经典命题逻辑的公理化是否可以通过将希尔伯特式演算合并为两个不相交的不完整片段而产生，我们将证明这个问题的答案是否定的，除非其中一个组件只包括类顶连接词。
2017-06-27 cs.LO math.LO
Wijesekera-style constructive modal logics
我们定义了一个命题构造性模态逻辑族，每个模态逻辑对应于一个不同的经典模态系统。逻辑定义在风格的Wijesekera的建设性模态逻辑，并证明理论和语义动机。一方面，它们对应于经典模态逻辑的标准演算的单一后继限制。另一方面，它们是通过将直觉Kripke模型的遗传性纳入模态公式的经典满足子句而获得的。我们表明，对于所考虑的经典逻辑，证明理论和语义方法返回相同的建设性系统。
2022-10-18 cs.LO math.LO
Non-Orthomodular Models for Both Quantum Logic and Standard Classical Logic: Repercussions for Quantum Computers
结果表明，量子逻辑和经典逻辑的命题演算都是非范畴的。我们发现，量子逻辑是除了正交模格也建模的弱正交模格和经典逻辑是除了布尔代数也建模的弱分配格。这两个新模型都是非正交模的。我们证明了模型演算的可靠性和完备性。我们还证明了正交模格中的所有运算都是五重定义的。最后，我们讨论了我们的结果可能对量子计算和量子计算机的影响。
1999-09-12 math.LO math.QA quant-ph
Questions and dependency in intuitionistic logic
近年来，疑问句逻辑和依赖逻辑在探究逻辑和依赖逻辑两个密切相关的框架中得到了研究。这些研究假设经典逻辑作为陈述的背景逻辑，并在这个经典核心中加入了表达问题和依赖关系的公式。在本文中，我们通过在直觉主义逻辑的背景下研究问题和依赖关系来拓宽这些研究的范围。我们提出了一个直观的团队语义，团队嵌入在直观的Kripke模型。伴随逻辑是直觉主义逻辑的一个保守的扩展，带有问题和依赖公式。我们建立了一些关于这个逻辑的结果，包括一个范式的结果，一个完整性的结果，并翻译到经典的查询逻辑和模态依赖逻辑。
2017-04-06 cs.LO math.LO
A Proof-Theoretic Approach to the Semantics of Classical Linear Logic
University College London（伦敦大学学院）
本文提出通过基础扩展语义（BeS）和基础支持的概念，从证明论角度研究经典线性逻辑的乘法-加法片段（MALL）语义学。
2026-02-27 cs.LO math.LO
The interdefinability of expansions of Belnap-Dunn logic
本文研究Belnap-Dunn逻辑的非经典连接词扩张是否与仅含经典连接词的扩张相互可定义，基于被遗忘的连接词可定义性一般概念，并探讨其与经典逻辑版本的关联。
2025-09-16 cs.LO math.LO
Computational interpretation of classical logic with explicit structural rules
我们提出了一个演算提供了一个Curry-Howard对应的经典逻辑中所表示的显式的结构规则，即弱化和收缩演算。这些结构规则分别引入了明确的删除和重复的条款。我们提出了一个类型系统，我们证明了类型保持下减少。详细研究了它与经典微积分之间的一种相互关系，这种关系具有隐含的结构规则。从这个分析中，我们得到强归一化性质。
2012-03-21 cs.DC cs.LO math.LO
On the strongest three-valued paraconsistent logic contained in classical logic and its dual
LP $^{\supset,\mathsf{F}}$是一个三值次协调命题逻辑，本质上与J3相同。它的大多数属性都被认为是合理的次协调命题逻辑的理想属性。然而，从已经发表的结果可以很容易地得出，正好有8192个不同的三值次协调命题逻辑具有相关的性质。本文利用逻辑等价关系的性质来区分LP $^{\supset,\mathsf{F}}$与其它逻辑。作为专注于逻辑等价关系的奖金之一，它被发现，只有32的8192逻辑有一个逻辑等价关系，满足的单位，湮灭，幂等，和交换法律的合取和析取。LP $^{\supset,\mathsf{F}}$的大多数性质都被认为是合理的次协调命题逻辑的理想性质，而它的仿完全类似物也具有类似的性质。本文还利用逻辑等价关系的有关性质，将LP $^{\supset,\mathsf{F}}$的仿完全模拟与具有类似性质的其它三值仿完全命题逻辑区分开来。
2020-12-01 cs.LO math.LO
Semantical Investigations on Non-classical Logics with Recovery Operators: Negation
本研究以拓扑布尔代数为基础，采用高阶逻辑元语言与Isabelle/HOL证明助手，为带恢复算子的非经典否定逻辑提供语义，构建拓扑对立立方并实现多阶量化的统一刻画，推动非经典逻辑的计算机辅助研究。
2023-07-21 cs.LO math.LO
Logic of Combinatory Logic
我们开发了一个经典的命题逻辑推理组合逻辑。我们定义了它的语法、公理系统和语义。以经典命题逻辑为基础，以类型化组合项为基本命题，给出了其语法和公理系统，并给出了其语义，该语义基于扩展了与原始组合子相对应的特殊元素的应用结构。无类型组合逻辑的方程理论和所提出的公理系统都被证明是正确和完整的。给出的语义。此外，我们证明了组合逻辑是可靠的和完备的w.r.t.给出的语义。
2022-12-13 cs.LO math.LO
