新刊速递 | 《逻辑学研究》2023年第3期目录及摘要
逻辑学研究 2023 年第 3 期
第16卷（总第70期）2023年6月18日出版
双月刊 2008 年创刊
目 录
--英文目录--
❖Kreisel’s “Shift of Emphasis” and Contemporary Proof Mining Ulrich Kohlenbach
❖Kreisel–Lévy-type Theorems for Set Theories Michael Rathjen,Shuangshuang Shu
❖Herbrand Expansions and Extraction of Proofs from Diagrams Matthias Baaz,Norbert Preining
❖Logics for Modally Real and Modally Nonreal Events Xian Zhao,Tianqun Pan
❖Cultural Manifest Knowledge Contributing to Deep DisagreementZhixi Chen,Jiangeng Ning
--中文目录--
专栏：证明论与数学基础
主持人：程勇
❖克莱瑟的“重心转移”及当代证明挖掘
乌利齐·克伦巴赫
❖集合论中的类克莱瑟列维定理
米夏尔·拉特延，舒双爽
❖埃尔布朗扩展及来自图表的证明提取
马蒂亚斯·贝兹，诺伯特·普雷宁
❖公开宣告逻辑的一个加标矢列演算
吴昊，汉斯·范·狄马希，陈锦盛
❖模态实在与模态非实在事件的逻辑
赵贤，潘天群
❖导致深度分歧的显性文化知识
陈志喜，宁建庚
论文摘要
克莱瑟的“重心转移”及当代证明挖掘
乌利齐·克伦巴赫（达姆施塔特工业大学数学系）
摘要：当代“证明挖掘”研究的历史根源于格奥尔格·克莱瑟的“挖掘证明”研究纲领。在本文中，我们详细阐述克莱瑟这一想法对应用证明论仍在持续的巨大影响，并且讨论证明挖掘的一些逻辑方面。
集合论中的类克莱瑟列维定理
米夏尔·拉特延（利兹大学纯数学系）
舒双爽（利兹大学纯数学系）
摘要：克莱瑟与列维（1968）曾作过一个著名的表征皮亚诺算术反射原则（RFN(PA)）的定理。该定理将RFN(PA)与超限归纳原则TI()联系起来；后者即是超限归纳至序数——最小的取-幂定点。
在这篇文章中我们将此结果推广至一大部分的集合论。我们所要讨论的集合论如下所述：它们包含克里普克-普拉特克集合论（KP）；追加的公理必须被限制在一定的句法复杂度内，即存在一个固定的n使得它们皆为。比如说如果取任意n，句法复杂度，KP+幂集+-分离 +-收集就是一个典型的例子。现在假设T是在我们的考虑范围之内的一种集合论。我们对于T+RFN(T) 的表征会以超限归纳原则TI()给出，其中所表示的是所有序数的类，则是最小的取-幂定点。并非集合序数；其定义类似于证明论中的表示系统，不同之处仅在于ω被序数之类所替换。在T中从RFN(T)推导TI()的证明相当常规；其本质是根岑已证过的内容。逆命题则是更难的部分。对PA的这个方向，克莱瑟与列维使用了忒特（1965）证明算术“无反例”（no-counterexample）定理。后来克莱瑟想到使用切消法（cut elmination），而施维希滕伯格（1977）在中将其实现出来，在技术上，告诉我们无限证明的切消可以用原始递归函数实现。这些原始递归函数取值于无限证明树的某种代码（该种无限证明允许“延迟”推理，即使用-rule 使得前提与结论一致；施维希滕伯格称之为-rule的非常规应用）。如何严谨而详细地定义及操作这些代码，可称是一个挑战。在这篇文章中我们将借用构造主义策梅洛-弗兰克尔集合论（CZF）中归纳定义类的技术，从而回避先前所提到的那种代码。因此——类比布赫霍兹（1977）——本文的技术要素处于集合论语境之中，其本身也是有启发意义的。通常而言，我们对T中KP以外公理所加的复杂度限制是必要的。比如说，我们的表征不能应用于T = ZF；事实上ZF已经证明TI()。我们自然会联想到其它序数表示系统，比如费法曼和舒特曾使用来表征理论自主扩充的强度。如果考虑超限归纳至类似的序数表示系统类（即），怎样的反射原则对应于这种超限归纳原则，将是一个有趣的命题。埃尔布朗扩展及来自图表的证明提取
马蒂亚斯·贝兹（维也纳工业大学离散数学与几何研究所）
诺伯特·普雷宁（东京Mercari公司）
摘要：本文介绍射影几何中的图作为有效的证明工具。尽管图表用于支持对射影几何中证明的理解，它们本身不被视为证明。我们将表明图表可转换为无切割证明，反之亦然。这意味着，图表是种有效且完备的证明工具，然而图表可能比通常的使用切割规则的证明更复杂。作为这些分析的一个有趣结论，我们将证明，图表在逻辑意义上不是构造性的。
公开宣告逻辑的一个加标矢列演算
吴昊（中山大学逻辑与认知研究所，中山大学哲学系）
汉斯·范·狄马希（法国国家科学研究中心，图卢兹大学，图卢兹研究与信息研究所）
陈锦盛（中山大学哲学系（珠海））
摘要：公开宣告逻辑（PAL）是在认知逻辑（EL）中添加归约公理得到的拓展。本文为 PAL 提出一个无切割定理的加标矢列演算系统，该系统是在 EL 的加标矢列演算系统上添加归约公理对应的矢列规则得到的拓展，且切割可允准、支持停机搜索。
模态实在与模态非实在事件的逻辑
赵贤（河北大学哲学系）
潘天群（南京大学哲学系）
摘要：一个事件在一个世界中是模态实在的，如果它发生在这个世界或该世界的一个可能世界中；如果一个事件没有发生在一个世界或其任何一个可能世界中，则它在这个世界中是模态非实在的。我们称一个世界中所有模态非实在事件发生或存在的地方为模态黑洞。本文提出了模态实在事件和模态非实在事件的逻辑系统，并证明了系统的可靠性和完全性。
导致深度分歧的显性文化知识
陈志喜（广东外语外贸大学外国语言学及应用语言学研究中心）
宁建庚（广东外语外贸大学外国语言学及应用语言学研究中心，运城学院外语系)
摘要：目前对导致深度分歧的文化原因方面的研究存在着一种紧张关系，它存在于文化知识的集体不可区分性与高度个人特质性之间。要解决这种紧张关系，我们需要一种新的方法。本文在后格莱斯关联理论的基础上，提出文化显性知识，试图探索解决上述紧张关系的新方法。本文认为，在寻找导致深度分歧的文化因素时，我们既不应该只从集体角度关注论证参与者所持有的难以区分的文化知识，也不应该只从个体角度关注个人的特殊知识，我们应该从包含论证参与者文化能力的文化显性知识方面入手探寻导致深度分歧的文化原因。