Bounded arithmetic AID for Frege system

The Strength of Abstraction with Predicative Comprehension

Frege's theorem says that second-order Peano arithmetic is interpretable in Hume's Principle and full impredicative comprehension. Hume's Principle is one example of an abstraction principle, while another paradigmatic example is Basic Law V from Frege's Grundgesetze. In this paper we study the strength of abstraction principles in the presence of predicative restrictions on the comprehension schema, and in particular we study a predicative Fregean theory which contains all the abstraction principles whose underlying equivalence relations can be proven to be equivalence relations in a weak bac…

Characterizing Propositional Proofs as Non-Commutative Formulas

Does every Boolean tautology have a short propositional-calculus proof? Here, a propositional calculus (i.e. Frege) proof is a proof starting from a set of axioms and deriving new Boolean formulas using a set of fixed sound derivation rules. Establishing any super-polynomial size lower bound on Frege proofs (in terms of the size of the formula proved) is a major open problem in proof complexity, and among a handful of fundamental hardness questions in complexity theory by and large. Non-commutative arithmetic formulas, on the other hand, constitute a quite weak computational model, for which e…

等价于 Feferman 系统 $\mathsf{T}_0$ 的 Frege 结构理论

Theories of Frege structure equivalent to Feferman's system $\mathsf{T}_0$

本文提出了几个与 Feferman 系统 $\mathsf{T}_0$ 具有相同证明论强度的 Frege 结构系统，通过扩展 Kripke--Feferman 理论和 Aczel 的 Frege 结构，并为 Cantini 的超赋值式理论引入宇宙概念，解决了一个开放问题。

从扩展弗雷格下界出发证明P≠NP

Towards P$\ne$NP from Extended Frege lower bounds

本研究基于有界算术理论$S^1_2$与扩展弗雷格证明系统EF的性质，提出多组可推出$P\ne NP$的条件假设，将计算复杂性下界与证明复杂性建立关联，且结果可推广到更强理论与证明系统。

逆细胞自动机的下界 via 证明复杂性

Lower Bounds on Inverse Cellular Automata via Proof Complexity

研究有限大小配置上逆细胞自动机的复杂性，通过将UNSAT归约到该问题简化证明其co-NP完全性，并展示其在弱算术理论V^0中可形式化，利用已知的受限深度Frege系统下界和Paris-Wilkie翻译，得出逆细胞自动机大小的下界。