Length of proofs depends not only on the theory but also on its axiomatization. Once an axiomatization is fixed, typical proof systems are equivalent up to a polynomial factor. But what if we care about polynomial factors and want the proof system to be quasilinear time efficient?
Thus for example, for $∀x_1 ∀x_2 ... ∀x_n \, 0=0$ we want a size $\tilde{O}(n)$ proof rather than only $\tilde{O}(n^2)$ that we get using sequent calculus (without optimizations).
For all I know, there might not be a single preferred proof system for the predicate calculus up to quasilinear size equivalence. However, ZFC and many other natural axiomatic systems have a certain closure that allows defining quasilinear time completeness as follows.
Let $P$ be a proof system for the predicate calculus whose soundness is provable in ZFC, and such that (constructibly provably in ZFC) $P$-proofs can be verified in quasilinear time. (A verification checks whether a given string is a $P$ proof of a given statement.) Let a ZFC $P$ proof of $B$ be a $P$ proof of $A⇒B$ together with the string $A⇒B$, where $A$ is a conjunction of ZFC axioms and $B$ is in the language of set theory.
Let us say that $P$ is quasilinear time complete for ZFC iff for every proof system $P'$ satisfying the above properties, there is a quasilinear time algorithm that given $B$ and a ZFC $P'$ proof of $B$ returns a ZFC $P$ proof of $B$.
Question: What are some natural examples of proof systems that are quasilinear time complete for ZFC?
To see that proof systems that are quasilinear time complete for ZFC exist, note that a ZFC $P$ proof of $B$ can be obtained as follows:
* Start with a $P'$ proof of $A⇒B$ ($A$ is a conjunction of ZFC axioms) and use soundness of $P'$ and a particular quasilinear verification of $P'$ proofs to get a ZFC $P$ proof that $A⇒B$ is provable in the predicate calculus.
* Use reflection over the predicate calculus to get a ZFC $P$ proof of $A⇒B$, and hence a ZFC $P$ proof of $B$.
For natural proof systems, I expect that the exact reasonable choice of ZFC axioms does not matter (with different axiomatizations being quasilinear time equivalent), and that the proof systems will also be quasilinear time complete for other appropriate axiomatic systems such as PA and Z2. Also, ZFC, PA, Z2 and other typical strong theories that are not finitely axiomatizable prove all instances of reflection over the predicate calculus, and I expect that with reasonable axiomatizations, the proofs of reflection instances have quasilinear size.
