首页/论文/2007.14835

arXiv 2007.148352020-07-29math.LO

反思原则、命题证明系统和理论

Reflection principles, propositional proof systems, and theories

Pavel Pudlák

摘要：

反射原理是这样的陈述，即如果一个句子是可证明的，那么它就是真的。反射原理已经被研究用于一阶理论，但它们在命题证明复杂性中也起着重要作用。在本文中，我们将重新审视一些结果的反射原则的命题证明系统使用更精细的规模的反射原则。我们将使用的结果，证明下界的决议证明是困难的决议。这首先出现在最近的文章Atserias和穆勒作为一个关键引理，并推广和简化了一些衍生文件。我们也将调查一些结果有关的算术理论和证明系统与他们有关。我们将展示一个关于有限一致性陈述的证明复杂性的猜想和一个关于与理论相关的证明系统的陈述之间的联系。

英文摘要：

The reflection principle is the statement that if a sentence is provable then it is true. Reflection principles have been studied for first-order theories, but they also play an important role in propositional proof complexity. In this paper we will revisit some results about the reflection principles for propositional proofs systems using a finer scale of reflection principles. We will use the result that proving lower bounds on Resolution proofs is hard in Resolution. This appeared first in the recent article of Atserias and Müller as a key lemma and was generalized and simplified in some spin-off papers. We will also survey some results about arithmetical theories and proof systems associated with them. We will show a connection between a conjecture about proof complexity of finite consistency statements and a statement about proof systems associated with a theory.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

真正的真相

The Real truth

我们研究具有无界正负真假值的实值命题逻辑，我们称之为R值逻辑。这种逻辑稍微扩展了连续命题逻辑，而连续命题逻辑又建立在卢卡西维茨多值逻辑的基础上。在给出了R值逻辑的推理机制和语义之后，我们证明了有限理论的一个完备性定理。然后，我们定义酉和阿基米德理论，按照Riesz空间的理论。在单位设置，我们证明了一致性和可满足性的等价性和近似的完整性定理类似于一个连续命题逻辑。最后，在酉理论中，我们把阿基米德理论描述为强完备性成立的理论。我们还指出，R值逻辑提供了替代演算Lukasiewicz和命题连续逻辑。

2014-12-14math.LO

命题证明系统和快速一致性证明器

Propositional proof systems and fast consistency provers

快速一致性证明器是一个一致的多时间公理化理论，它具有任何其他多时间公理化理论的有限一致性陈述的简短证明。Kraj 'ıček和Pudlák证明了一个最优命题证明系统的存在等价于一个快速一致性证明器的存在。很容易观察到，${\sf NP}={\sf coNP}$意味着存在一个快速一致性证明器。相反的含义是一个悬而未决的问题。在本文中，我们定义了一个不太可能的快速一致性证明的概念，并证明了它的存在性等价于${\sf NP}={\sf coNP}$。接下来，它被证明，快速一致性证明不存在，如果一个考虑RE公理化理论，而不是理论与公理集是可识别的多项式时间。

2020-04-11math.LO

将同伦等价与带计算公理的依赖类型理论中的保守性联系起来

Relating homotopy equivalences to conservativity in dependent type theories with computation axioms

本文借助同伦类型理论与带属性范畴，通过上下文间典范同伦等价证明外延类型理论对带命题计算公理的依赖类型理论具有保守性。

2025-09-25cs.LOmath.CTmath.LO

序数理论的证明论III：$Π_{N}$ -反射

Proof theory for theories of ordinals III: $Π_{N}$-reflection

本文利用序数图系统给出了一个$Π_{N}$ -反射序数理论的证明论。这是前一篇（APAL 129）的续篇，其中对$Π_{3}$ -反射的理论进行了理论上的证明分析。

2010-07-06math.LO

反射代数与迭代真值理论的守恒性结果

Reflection algebras and conservation results for theories of iterated truth

我们考虑扩展的语言皮亚诺算术transmittiterated真理定义满足一致塔斯基双条件。如果没有进一步的公理，这些理论被认为是原始算术系统的保守扩展。然而，更强的系统可以通过在它们之上添加归纳公理或反射公理来获得。这类理论可以解释一些著名的二阶算术的谓词可约片段，如迭代算术理解。我们得到尖锐的结果，这些系统的证明理论的强度，使用可证明性逻辑的方法。反射原理自然地定义了作用于我们的迭代真值基本理论的可公理化扩展的半格上的一元算子。这个代数的顶元素所产生的子结构为被研究的理论类提供了一个规范的序数记号系统。使用这些符号，我们获得了对应于超算术层次的不同逻辑复杂性水平的迭代反射原理的保守性关系，即，Schmerl公式的类似物。这些关系，反过来，提供了我们的系统和一些相关的谓词可还原理论的证明理论分析。特别是，我们统一计算的序数特征的标准措施，他们的证明理论的强度，如可证明的良序，类可证明递归函数，和$Π_1^0$ -序数。

2019-10-30math.LO

直觉信念的一个分析演算

An analytic calculus for intuitionistic belief

直觉主义信念已经被阿特莫夫（Artemov）和普罗托波佩斯库（Protopescu）公理化为直觉主义命题逻辑的扩展，通过分配方案K和共反射$A\rightarrow\Box A$。通过这种方式，信念被解释为验证的结果，并且它适合于具有认知模态的直觉主义命题逻辑的扩展的Brouwer-Heyting-Kolmogorov解释。本文研究了直觉信念的自然演绎系统$\mathsf{IEL}^{-}$的结构性质。重点讨论了微积分的解析性，首先证明了正规化定理和子公式性质。从这些，逻辑的可判定性和一致性遵循作为推论。最后，用纯证明论的方法建立了析取性质、$\Box$ -素性和反射规则的可容许性。

2021-06-27cs.LOmath.LO

更多相关论文收起更多论文

基于反射原理的序数记号系统的基本理论

On Elementary Theories of Ordinal Notation Systems based on Reflection Principles

我们考虑由L.D. Beklemishev。这个系统的一些片段是小序数${ω_n}$的序数记号系统（$ω$的塔-高度$n$的幂）。该系统基于Japaridze的可证明性逻辑$\mathbf{GLP}$。它们与基于迭代反射原理的$\mathbf{PA}$序分析技术和$\mathbf{PA}$片段密切相关。我们认为这个符号系统和它的片段作为一个自然的方式选择的签名结构。证明了序数${\geω_4}$的完整记法系统及其片断具有不可判定的初等定理。我们还证明了完整系统的片段，序数${\leω_3}$，有可判定的基本理论。对于具有较弱签名的序数记号系统，我们得到了初等理论的可判定性的一些结果。

2013-12-11math.LO

与$PA$等价的理论的证明图式--论保守性反思原则的益处

Proof Schemata for Theories equivalent to $PA$: on the Benefit of Conservative Reflection Principles

归纳通常形式化为LK演算的规则或公理扩展。虽然这种对微积分的扩展简单而优雅，但证明转换和分析可能相当困难。具有归纳规则的理论，例如皮亚诺算术，没有{ \em Herbrand}定理。在这项工作中，我们扩展了现有的元理论形式主义，所谓的证明图式，递归公式的归纳特别适合于证明分析，皮亚诺算术。这种关系在\PA和另一种证明形式主义之间提供了一个有意义的保守反射原则。证明图式已被证明有一个变种的Herbrand定理的经典逻辑，可以提升到我们的新的形式主义相当于原始的递归算术的子系统。

2018-04-01math.LO

反驳语句的归结下界

Resolution Lower Bounds for Refutation Statements

对于任何不可满足的CNF公式，我们给出了一个命题陈述的归结反驳的大小的指数下界，该公式有一个归结反驳。我们描述了三个应用程序。(1)（Atserias，Müller 2019）中的一个开放性问题是，上述陈述的某种自然命题编码是否难以解决。我们给出了一个指数大小的下界。(2)我们展示了反射原理的指数分辨率大小下限，从而改进了（Atserias，Bonet 2004）中的结果。(3)我们提供了CNF的新例子，它以指数方式将Res（2）与Resolution分离（这两个证明系统的指数分离最初在（Segerlind，Buss，Impagliazzo 2004）中得到证明）。

2019-05-29cs.CCmath.LO

命题证明和算法证明搜索中的信息

Information in propositional proofs and algorithmic proof search

我们从证明复杂性的角度研究（非正式）证明搜索问题：是否有一个最佳的方法来搜索命题证明？我们注意到，对于任何固定的证明系统，存在一个时间最优的证明搜索算法。利用经典的证明复杂性的反射原理的结果，我们证明了一个时间最优的证明搜索算法存在不限制证明系统当且仅当一个p-最优证明系统存在。为了精确地描述单个公式所需的时间证明搜索算法，我们引入了一种新的基于算法信息概念的证明复杂性度量。特别地，对于证明系统$P$，我们附加{ \bf信息效率函数} $i_P(τ)$，将重言式分配给自然数，并且我们表明：- $i_P(τ)$表征任何$P$证明搜索算法必须在$τ$上使用的时间，并且对于固定的$P$，存在这样的信息最优算法，-证明系统是信息效率最优的当且仅当它是p最优的，- 对于不可自动化的系统$P$，存在具有短证明但具有大信息测度$i_P(τ)$的公式$τ$。我们隔离和激励的问题，建立无条件的超对数下限$i_P(τ)$没有超多项式大小的下限是已知的。我们还指出了新的措施与其他证明搜索的证明复杂性的一些主题的连接。

2021-09-05cs.CCmath.LO

完全反引用真理之上的迭代反射原则

Iterated reflection principles over full disquotational truth

迭代反射原则已被广泛用于揭示接受数学理论所产生的认知承诺。最近，这一点被应用于真理理论。我们的想法是从一个塔斯基双条件集开始，通过迭代反射到达强成分真理论。在经典逻辑的背景下，采用初始真值理论是不连贯的，其中A和“A是真的”是可相互推导的。在这篇文章中，我们展示了如何在一个较弱的逻辑，我们称之为基本德摩根逻辑的背景下，我们可以连贯地从这样一个完全反引用的真理理论开始，并通过有限次应用自然一致反射原理来达到一个强的合成真理理论。

2017-03-07math.LO

关于有限模代数的证明论

A Proof Theory for Profinite Modal Algebras

University of Amsterdam（阿姆斯特丹大学）；Università degli Studi di Salerno（萨莱诺大学）；Università degli Studi di Milano（米兰大学）

本文研究了有限模代数的证明论，揭示了无穷命题模演算与profinite $L$-代数的Lindbaum代数之间的联系，并探讨了演算语法性质与代数正则性之间的对应关系。

2026-10-02math.LO

反射演算的树重写系统

A tree rewriting system for the Reflection Calculus

本文提出一个针对反射演算的树重写系统，用于模拟其推导，并通过规范化提高证明搜索效率，以辅助研究该逻辑的子公式性质和规则可容许性。

2024-07-18math.LO

将$ω$ -模型反射约化为迭代句法反射

Reducing $ω$-model reflection to iterated syntactic reflection

在数理逻辑中，有两种看似不同的原则，称为“反射原则”。语义反射原理断言，如果一个公式在整个宇宙中成立，那么它在一个集合大小的模型中成立。句法反射原则断言，来自某个复杂性类的每个可证明句子都是真的。本文在二阶算术的背景下研究这两种反射原理之间的联系。我们证明，对于一个大的理论，$ω$模型反射是等价的索赔，均匀$Π^1_1$反射沿可数良序的任意迭代是$Π^1_1$ -声音。这个结果产生了强度在$\mathsf{ACA}_0$和$\mathsf{ATR}$之间的理论的一致序分析。我们分析的主要技术新颖性是引入了理论$T$的证明论扩张器的概念，它是可数序数上的算子，将$\prec$的序类型映射到$T+\mathsf{WO}(\prec)$的证明论序数。我们得到精确的结果证明理论扩张器的增长作为可证明的$ω$模型反射的函数。这种方法使我们能够同时获得不仅$Π^0_1$，$Π^0_2$，和$Π^1_1$序数，但也逆数学定理的良序原则。

2022-06-14math.LO

反射层次中的递减序列

Descending sequences in reflection hierarchies

Faculty of Philosophy, University of Warsaw（华沙大学哲学系）；Department of Philosophy, New York University（纽约大学哲学系）

研究探讨了在不同复杂度类下，n一致r.e.理论序列的编码方式对n一致性证明的影响。

2025-12-04math.LO

再论归约性质

The Reduction Property Revisited

在本文中，我们将研究一个重要的，但相当技术性的结果，这是所谓的约化性质。这个结果告诉我们两个数论之间有多少算术守恒。这两种理论本质上都是关于反思的基本原则：如果一个句子是可证明的，那么它就是真的。第一个理论是公理化使用反射公理和第二个理论使用反射规则。约化性质告诉我们，第一个理论扩展了第二个理论，但对于一大类公式是保守的。我们在不同的方向上扩展了归约性质。最值得注意的是，我们将看到各种不同类型的反射公理和规则是如何相互关联的。此外，我们扩展的减少属性超限反射原则。由于还没有令人满意的（超）算术解释，因此这种推广应该在纯粹的代数环境中进行。对于专家：经典归约性质的一个推论描述了$Π^0_{n+1}$推论的特征，并告诉我们，对于任何具有正确复杂度的理论$U$和$T$，我们有\[ U + {\sf Con}_{n+1}(T) \equiv_{Π^0_{n+1}} U \cup \{ {\sf Con}_n^k(T)\mid k<ω\}. \]。如果我们对具有$j{\leq}n$的$Π^0_j$公式感兴趣，我们将计算哪些理论可以放在右边。我们回答这个问题也在一个纯粹的代数设置$Π^0_j$ -保守将适当定义。代数转向允许对超限一致性概念的推广。

2019-03-08math.LO

证明复杂性中的H-染色二分法

H-coloring Dichotomy in Proof Complexity

无向单图的$\mathcal{H}$ -染色问题是一类约束满足问题（CSP）中的计算问题：图$\mathcal{G}$的$\mathcal{H}$ -染色是从$\mathcal{G}$到$\mathcal{H}$的同态，问题是在给定$\mathcal{G}$的情况下，判定固定的$\mathcal{H}$是否存在同态. $\mathcal{H}$ -着色问题的二分法定理由Hell和Nešetzil在1990年证明（Zhuk和Bulatov最近证明了所有CSP的类似定理），它说对于每个$\mathcal{H}$，问题要么是$p$ -时间可判定的，要么是$NP$ -完全的。由于CSP的不可满足实例的否定可以表示为命题重言式，因此研究CSP的证明复杂性似乎是很自然的。我们表明，在$p$时间的情况下的$\mathcal{H}$着色问题的决策算法可以在一个相对较弱的理论和重言式表达的负面情况下，这样的$\mathcal{H}$有简短的证明命题证明系统$R^*(log)$，一个温和的扩展决议。事实上，当公式表示为不可满足的子句集时，它们具有$p$大小的分辨率证明。为了建立这一点，我们使用一个众所周知的有界算术理论和命题证明系统之间的联系。我们补充这一结果的下界结果，持有许多弱证明系统的一个特殊的例子$NP$ -完整的情况下的$\mathcal{H}$着色问题，使用已知的结果证明复杂性的鸽子洞原则…

2020-10-05math.LO

极不稳定理论与计算复杂性

Finitely unstable theories and computational complexity

复杂性类$NP$可以通过存在二阶逻辑$SO\exists$来逻辑地表征，如Fagin所证明的，以及通过经由命题逻辑SAT的可满足性问题来模拟图灵机来逻辑地表征，如Cook所证明的。这两个定理都涉及用相应逻辑中的公式对图灵机进行编码，并声明当且仅当图灵机停止时，该公式的模型存在，即该公式是可满足的，当图灵机接受其输入。Trakhtenbrot定理在一阶逻辑$FO$中也是如此。这种不同的编码顺序是可能的，因为直到任何给定的有限时刻的任何图灵机的所有可能配置的集合可以由命题变元的有限集合定义，或者由固定有限大小的模型局部表示。在当前的文件中，我们首先编码这种时间有限的计算的确定性图灵机（DTM）在一阶逻辑。然后，我们仔细看看解决SAT的DTM。当输入字符串的长度这样一个DTM，其中包含有效编码的SAT的实例是参数化的自然数$M$，我们继续表明，相应的$FO$理论$SAT_M$有一个下界的大小，其模型几乎呈指数增长与$M$。这个模型大小的下限也转化为SAT的确定性时间复杂度的下限。

2014-10-18cs.CCcs.LOmath.LO

用于-bar-归纳（Bar Induction）的反射演算与一致性强度排序的线性性

A Reflection Calculus for Bar Induction and the Linearity of Consistency Strength Ordering

Ghent University（根特大学）；Steklov Mathematical Institute of the Russian Academy of Sciences（俄罗斯科学院斯捷克洛夫数学研究所）

本文提出反射演算的扩展RC_BI，分析ACA₀的相关扩展理论，证明其可靠性与完备性，借助模态语义确立相关理论类的预良序性，实现BI及其片段的序数分析并提出新型序数记号系统。

2026-10-14math.LO

集合论中的广义序数分析与反射原理

Generalized ordinal analysis and reflection principles in set theory

针对自然公理系统良序层级的质疑，本文基于集合论反射原理提出证明论强度概念，证明其与Pohlers广义序数分析的理论序一致，生成良序层级，并推广至其他内模型。

2023-12-20math.LO

一阶逻辑对偶

First-Order Logical Duality

从逻辑的角度来看，斯通对偶布尔代数涉及理论在经典命题逻辑和他们的收集模型。理论可以被看作是布尔代数的表示，模型的集合可以被拓扑化，这样理论就可以从它的模型空间中恢复出来。这种情况可以被看作是一种形式上的二元性，它把句法和语义两个范畴联系起来，通过归巢中介成一个共同的二元对象，在这种情况下是2。在目前的工作中，我们推广整个安排从命题的一阶逻辑。用一阶逻辑中的布尔范畴代替布尔代数，用模型的拓扑群胚及其同构代替模型空间。由此产生的句法和语义范畴之间的对偶，首先以逆变附加词的形式表达，通过归巢到一个共同的对偶对象（现在是$\Sets$）中来建立，它一度被视为布尔范畴，一度被视为配备有内在拓扑的广群。我们的研究的总体框架是由拓扑斯理论提供的。直接证明的主要结果，但专家将认识到拓扑思想的背景。事实上，语法和语义之间的对偶性实际上是代数和几何之间的对偶性在隐藏在我们形式理论后面的几何态射的两个方向上的表现。在此过程中，我们通过一个简化的相干拓扑覆盖定理，从一个可判定的相干理论的模型广群中构造了它的分类拓扑。

2013-06-28math.CTmath.LO