2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I'm still trying to understand the actual question, but I'm wondering why a sequent calculus proof of ∀x1...∀xn 0=0 should be quadratic in the formula size. It should be n applications of ∀:r inferred from 0=0 as an instance of the reflexivity axiom of equality. $\endgroup$ – lambda.xy.x Oct 23 '18 at 23:32
  • $\begingroup$ I would also be surprised if the non-elementary speedup of a sequent calculus with cut against one without cut can be remedied by picking the right axiom system. So I'm not even sure about the "typical proof systems are equivalent up to a polynomial factor." If I remember correctly, proof systems are often incomparable when it comes to proof complexity in the sense that there are formulas F and G such that proof system A has a short proof of F and a long proof of G but a proof system B has a short proof of G and a long proof of F. $\endgroup$ – lambda.xy.x Oct 23 '18 at 23:40
  • $\begingroup$ Reading on further, I'm not even sure if you speak about proof checking or the sizes of the actual proofs :( $\endgroup$ – lambda.xy.x Oct 23 '18 at 23:45
  • $\begingroup$ @lambda.xy.x If each application of ∀:r includes a copy of the formulas used (as is standard), the number of bits is quadratic. Also, by "typical proof systems", I only meant proof systems with the cut rule or a reasonable substitute, but see Cut-free proofs in ZFC. $\endgroup$ – Dmytro Taranovsky Oct 24 '18 at 1:16
  • $\begingroup$ @lambda.xy.x The insight of the question is that for proofs in ZFC, all sufficiently powerful appropriate proof systems are in fact quasilinear-time equivalent, with the question being to give (with proof) a natural example of such a proof system. $\endgroup$ – Dmytro Taranovsky Oct 24 '18 at 1:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.