两个模糊逻辑规划模型隐含连续统假设=“假”和选择公理=“假”隐含ZFC不一致

模糊饮酒悖论与模糊选择公理：向下洛文海姆-斯科伦定理的构造性反反数学

Blurred Drinker Paradoxes and Blurred Choice Axioms: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem

本文探讨了构造性反反数学中向下洛文海姆-斯科伦定理的逻辑分解，揭示了模糊饮酒悖论与模糊选择公理在不同公理体系下的等价关系。

Zermelo-Fraenkel集合论与选择公理的不一致性及其对计算复杂性的影响

Inconsistency of the Zermelo-Fraenkel set theory with the axiom of choice and its effects on the computational complexity

本文揭示了Zermelo-Fraenkel集合论与选择公理（ZFC）的矛盾。虽然哥德尔的不完备性定理指出，一个相容的系统不能证明它的相容性，但它们并没有排除使用更强的系统或系统范围之外的方法进行证明。本文证明了无穷集的基数是不可控的和矛盾的。然后，本文指出，皮亚诺算术，或一阶算术，是不一致的，如果所有的公理和公理模式假设在ZFC系统是真的，表明ZFC是不一致的。然后，本文揭示了一些后果，是在计算复杂性理论的范围内。

一种真正无类型的认知者悖论解决方案

A genuinely untyped solution to the knower paradoxes

本文提出一个一致的真正无类型一阶知识理论，通过知识谓词与真谓词形式化真实性原则以解决认知者悖论，并借助自指和Löb定理支持公共知识推理。

Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis

In 1964, Paul Erdős published a paper settling a question about function spaces that he had seen in a problem book. Erdős proved that the answer was yes if and only if the continuum hypothesis was false: an innocent-looking question turned out to be undecidable in the axioms of ZFC. The formalisation of these proofs in Isabelle/HOL demonstrate the combined use of complex analysis and set theory, and in particular how the Isabelle/HOL library for ZFC integrates set theory with higher-order logic.

四个悖论与一个证明助手：coq-paradoxes 库中的 Burali-Forti、Diaconescu、Reynolds 和 Hurkens

Four Paradoxes and a Proof Assistant: Burali-Forti, Diaconescu, Reynolds, and Hurkens in the coq-paradoxes library

本文通过 coq-paradoxes 包中机械化的四个悖论（Burali-Forti、Diaconescu、Reynolds 和 Hurkens），展示了归纳构造演算（CIC）的边界条件，并论证这些悖论是 Rocq 内核设计拒绝某些构造的负面规范。

证立逻辑中的不可能义务与冲突义务

Impossible and Conflicting Obligations in Justification Logic

该研究针对标准道义逻辑中义务一致性概念等价的问题，在证立逻辑框架下提出多种一致性原则并比较其逻辑强度，构建了使带jd公理的证立逻辑对任意常项规范完全的新语义，还探讨了相关道义悖论的哲学意义。