有界算术上的矩阵秩函数

《Annals of Pure and Applied Logic》：On matrix rank function over bounded arithmetics

　　摘要：在文献[14]中，Mulmuley给出了一种将矩阵秩函数的计算归约为行列式计算的算法，其正确性的证明是初等的。本文在有界算术??????中形式化这一论证；也就是说，我们证明对于具有??(??)系数的矩阵??,??，由det(????)=det(??)det(??)可推出rank(??)=dim(im??)，其中??是该理论域的全集，M是具有??系数的矩阵，而rank(??)是由Mulmuley算法计算的秩函数。此外，通过用??=?的??????2解释??????，并利用文献[18]的结果，我们看到??????2可以形式化rank(??)并证明rank(??)=dim(im??)。最后，我们给出几个在??????2中可证的组合命题的例子，这些例子使用了形式化线性代数。

引言：基于NP与????????问题的刻画[8]，命题逻辑的证明复杂性已被深入研究。在各种具体证明系统中，Frege系统在该领域一直扮演着重要角色。尽管经过数十年的深入研究，Frege系统是否具有多项式界仍是一个未解决的问题[13]。如果???? ≠ ????????，那么Frege系统不可能具有多项式界。基于这一观察，文献[5]给出了大量组合命题的例子，这些命题可以形式化为一族命题重言式，但在Frege系统中似乎难以有效证明。然而，研究表明Frege系统相当强大。已知有：
- Bondy定理的多项式规模Frege证明（[5]）
- Bollobás定理的多项式规模Frege证明（[2]）
- Frankl定理的拟多项式规模Frege证明（[1]）
- 矩阵行列式乘法性、Cayley-Hamilton定理以及其他几个困难矩阵恒等式的拟多项式规模Frege证明（[18]）。

本文属于这一研究方向。粗略地说，我们证明拟多项式Frege系统可以形式化具有?系数的方阵M的矩阵秩函数rank(??)，并证明rank(??)=dim(im??)。为了更精确地说明这一点，我们需要有界算术的概念。已知许多有界算术系统T在命题证明系统中都有对应的????，使得如果?Σ??0-定理在有界算术理论T中可证，那么在????中存在（拟）多项式规模的命题证明（[7]）。就有界算术而言，我们的工作以及上述关于组合命题可行可证性的结果都属于Cook提出的“有界逆向数学”研究计划。

就线性代数而言，与之相关的第一个且最自然的有界算术是文献[15]和[16]中引入的LA和??????，它们包含三种对象：索引类、域类和矩阵类。从模型论角度看有趣的是，它们处理一般的系数域，包括那些甚至在算术标准模型中不可定义的域。文献[15]在??????中形式化了矩阵行列式，遵循文献[4]的方法，并证明了：
1. 以下命题在??????上等价：
(a) 余子式展开的存在性，
(b) 行列式的公理化定义，
(c) Cayley-Hamilton定理。
2. 矩阵行列式的乘法性蕴含上述所有命题。

此外，他们给出了一个更强的理论???????，能够证明上述矩阵恒等式，并给出了将???????的普适句证明转换为扩展Frege系统的翻译定理。这对应于上述困难矩阵恒等式在有界算术??11中都可证的事实。然而，上述困难矩阵恒等式(1a)-(1c)和(2)是否在（看似）弱于??11的有界算术中可证，一直是一个长期未解决的问题。下一个突破是由文献[11]和[18]给出的。通过使用带除法的算术电路，通过Schur补来形式化矩阵行列式，他们证明了对于整数系数，行列式的乘法性以及上述提到的困难矩阵等式可以在有界算术??????2中证明，这对应于规模为2^??(|??|2)的Frege证明，因此相应的重言式具有拟多项式规模的Frege证明。

本文的主要贡献是给出秩性质可证性的上界。关于矩阵秩函数在并行算法背景下计算复杂性的比较已有系列研究（[9]），已知秩函数通过Mulmuley的优雅并行算法[14]归约到矩阵行列式。尽管由于Mulmuley算法不依赖于系数域，在??????中形式化矩阵秩函数是直接的，但这并不直接意味着基本的秩性质在该理论中可证。实际上，我们考虑??????的扩张??????????，它增加了关于具有??(??)系数的方阵??,??的公理det(????)=det(??)det(??)。这里??是??????的域的全集。然后我们将证明由Mulmuley算法计算的具有??系数的矩阵的秩与以下各量一致：
- 线性无关行向量的数目
- 线性无关列向量的数目
- 非零极大子式的次数

此外，我们证明??????????可以被??=?的??????2解释，因此拟多项式Frege证明可以在推理中引用和利用矩阵秩函数。

本文的组织如下：在第3节中，我们简要回顾Soltys关于线性代数的理论。我们还介绍了??????语言中的Σ??0可定义性，并证明了??????对Σ??0公式具有量词消去（定理1，推论2）。在第4节和第5节中，我们基于第3节的结果在??????中形式化一些多项式的基本处理。准确地说，我们观察到如果〈??,??,????????〉???????，则〈??,??[??],????????[??]〉????????成立。形式上，我们用???????定义????????的解释?????????，它将域解释为多项式的全集（通常记为??[??]），将矩阵解释为具有多项式系数的矩阵的全集（记为????????[??]，命题17）。在第6节中，类似于第5节，我们在??????中形式化一些有理函数的基本处理。我们引入??(??)和????????(??)，并观察到〈??,??(??),????????(??)〉???????（命题23）。在第7节中，我们引入有界算术??????????（定义28），它是??????加上????????(??)中行列式的乘法性。还给出了一个更简单的只涉及多项式的??????????的替代定义（命题30）。在第8节中，我们在符号中形式化了矩阵代入多项式。在第9节中，利用前几节中有理函数的基本性质，我们按照Mulmuley算法形式化矩阵秩函数（定义39），并证明它在??????????中与线性代数的其他几个概念一致（定理9）。在第10节中，我们证明??????2可以解释?系数的??????????（定理56），作为推论，我们获得矩阵秩在??????2中的可定义性（推论58）。这项工作包括文献[18]中的行列式定义在??????2中可证地与Berkowitz算法（[4]）兼容。（后者是文献[15]形式化的方法。）如第11节所述，这种解释也适用于具有标准素数?? ∈??的????-解释。

作为线性代数定理可证性的应用，文献[18]中实质上已经证明，通过形式化所谓的线性代数方法，组合性质也在??????2中可证。这些性质包括oddtown定理、Graham-Pollak定理、Fisher不等式以及Ray-Chaudhuri-Wilson定理的一个变体。在第11节中，我们在这个列表中添加两个更多结果，即Ray-Chaudhuri-Wilson定理的另一个版本（定理59）和Grolmusz关于Ramsey图的显式构造（定理61），作为我们秩性质形式化的应用。最后，第12节讨论开放问题。附录包含技术定义以及第3、5、6和8节中证明的细节。

主要结果与辅助命题和概念之间的关系在以下表格中给出。

章节片段

致谢：我们感谢Toshiyasu Arai和Iddo Tzameret的意见。作者衷心感谢匿名审稿人的真诚建议，这些建议极大地改进了本文的表述。本工作受JSPS KAKENHI资助号18K03400和22J22505支持。第一作者还受JSPS研究员资助和东京大学FoPM项目的支持。

预备知识：我们假设??????、??????2及相关理论的概念和结果，不再赘述。读者可参阅文献[15]和[18]等参考文献。对于自然数k，[??]表示k-集合{1,…,??}。我们用???表示给定一阶理论T的语言。此外，变量元组(??1,…,????)通常记为ˉ??。对于公式??(??1,…,????)和项??1,…,????，??[??1 ???1,…,???? ?????]或简写为??[ˉ?? ?ˉ??]表示通过同时代入得到的公式。

理论的解释：我们首先在?????中发展一些定理，然后证明多项式的基本处理可以在该理论中完成（即命题17）。为此，为了整洁地描述多项式的算术，我们利用解释的概念：

定义4：设?是k-类一阶语言，??1,…,????是它的类。类似地，设?′是??′-类一阶语言，??′1,…,??′??′是它的类。我们假设?（相应地?′）对其每个类s都包含等号=??。现在，假设我们有

??????中多项式的形式化与解释?????????：在本节中，我们讨论在??????中多项式的形式化。为了方便和可读性，我们固定??????的任意模型?=〈??,??,????????〉，其中??,??和????????分别表示域、索引和矩阵的全集。此外，对于每个??,?? ∈??，????????(??,??)是矩阵全集的可定义子集，收集使得??(??)=??和??(??)=??的元素A。此外，对于??,?? ∈??，我们定义[??,??] := {??∈??|??≤??≤??}，[??,??[ := {??∈??|??≤??
有理函数：到目前为止，我们已经证明??????可以适当地处理??[??]和????????[??]，并证明它们满足???????。也就是说，我们得到???????的新模型(??,??[??],????????[??])。现在，由于我们使用域的一些性质来形式化秩函数，我们也在??????中发展有理函数的形式化。一旦我们发展了它，我们证明有理函数和有理系数矩阵满足??????本身。然后，再次应用上述解释?????????，我们可以得到一个模型

理论??????????：在文献[16]中，考虑了??????+“det是乘法性的”，并证明了余子式展开和Cayley-Hamilton定理在该理论中可证。基于此，我们考虑以下理论（PD代表“polynomial determinant”）：

定义28：?????????? := ?????? + ?det是乘法性的???????，即，
?????????? := ?????? + ((??,??,??),(?,??,??′)∈????????(??)(??,??)→??????rat((??,??,??)???????(?,??,??′))=????????????rat(??,??,??)?????????????rat(?,??,??′))

考虑以下公理：

定义29：我们定义公式(??????)为：
(??,??),(??,??′)∈????????[??](??,??)→??????pol((??,??)???????(??,??′))=??????

矩阵代入多项式：如文献[16]所述，在???????中，我们可以将矩阵A代入??(??) ∈??[??]中的不定元（域元素的代入，即对?? ∈??的??(??)，可以类似地形式化且比下面更容易，因此我们省略其细节）；

定义33：???????中，对于??(??) ∈??[??]和?? ∈????????(??,??)，
??(??) := ??(??)?1∑??=0??????????(??,??)????。更形式地，??(??) := ∑(????)，其中
???? := ??????〈??(??)??,??,??(??,??,1)??(????????(???1,??),??????(???1,??)+1,??)〉。

固定?? ∈????????(??,??)，我们可以证明??(??) ???(??)是环同态：

引理34：???????中，对于??(??),??(??) ∈??[??]和?? ∈????????(??,??)，
??=????

秩的定义及其基本性质：现在，我们证明??????可以Σ??0-定义秩函数。首先，我们观察到??????可以计算向量中开谓词解的数量（然而，由于词汇的限制，输出适当的索引元素是不可能的，因此我们设计一个项，其唯一的非零分量对应于该数量）：

定义36：索引向量是向量?? ∈????????(??,1)，使得???≤??(????1=1∧???≤??(??≠??→????1=0))。索引矩阵是矩阵??= [??1,…,????]∈????????(??,??)，使得每个????是

由??????2解释：在本节中，我们证明在??????2中形式化的有理系数线性代数满足??????????（关于有界算术??????2的正式定义，参见[7]）。由于我们希望使用几个????2函数作为项，我们使用???????2而不是??????2。已知??????2（或???????2）相当强大，足以进行基本算术运算、由字符串类编码的整数上的矩阵运算以及算术电路的操作（这里，算术电路是

在??????2中可证的若干组合结果：在本节中，我们给出秩在??????2中可定义性的两个应用。首先，我们证明以下Ray-Chaudhuri-Wilson定理的变体，这是文献[5]中提到的可能困难的另一候选命题，也在??????2中可证：

定理59：??????2中的Ray-Chaudhuri-Wilson定理。设?? ∈?。则??????2证明以下命题：设??,??为数，?,??为字符串。假设?编码[??]的子集族{??1,…,????}，L编码数集{??1,…,????}。还假设?是L-相交的，即??? ≠?? ∈[??]. #(???? ∩????) ∈??。

然后是开放问题：正如[18]所指出的，有趣的是，目前已知的矩阵行列式和秩函数的形式化似乎仍然过于复杂。也就是说，我们有V#L（参见[6]），它对应于复杂度类#L（或AC0(#L)），能够形式化矩阵行列式，因此也能形式化秩函数，但我们只知道它们在VNC2中的基本性质证明，而VNC2对应于NC2，NC2包含#L。要确定V#L是否足够强大以完成这些证明，这是一个有趣的问题。此外，在...

未引用的参考文献
[17] 研 英人 | 黑田 悟
东京大学大学院数理科学研究科，东京都目黑区粕3-8-1，邮编153-0041，日本