Skip to content

The Proof Theory Blog

PA ⊢ ∀x ∃y A(x,y) ⇒ ∃t . T ⊢ ∀x A(x,t(x))

Menu
  • Home
  • About
  • Contribute
  • Resources
Menu

Checking proofs with very low complexity

Posted on June 12, 2020June 12, 2020 by Anupam Das

The very notion of mathematical proof is founded upon the idea that a proof is ‘routine’ to check. While it may be difficult to actually prove a mathematical theorem, a proof should allow us to verify its truth without question or significant effortIt goes without saying that this is only an ideal.. But exactly how much effort is required to check a proof, in terms of computational complexity?

Abstract proof systems and the Cook-Reckhow criterion

In proof complexity there is a well-known formalisation of this idea: the Cook-Reckhow criterion. This criterion says that, to qualify as a ‘proof system’, proofs must be polynomial-time checkable. It is this that gives rise to the famous Cook-Reckhow theorem [BIBCITE%%3%]:

Theorem (Cook-Reckhow ’74). There is a proof system for classical propositional logic with polynomial size proofs of each tautology if and only if \mathbf{coNP} = \mathbf{NP}.

But this polynomial time criterion for checkability seems overkill in practice. We can usually verify proofs in commonly used systems in some ‘local manner’ leading to log-space algorithms or simpler.

So what is the general complexity of checking proofs? Well, naturally, the answer to that question depends on the proof system at hand. However, perhaps a lower bound can be derived from the following intuitionI recall this intuition being used to argue for a lower bound in several discussions with collaborators!: to know that a proof is correct, we have to at least check that the conclusion is a syntactically correct formulaThis problem is a special case of recognising Dyck languages, asking whether an expression is well-bracketed.. This is known to not be possible in \mathbf{AC}^0 but is possible in \mathbf{TC}^0 (an apparently folklore result).

The log-time hierarchy (aka  \mathbf{AC}^0)

Low-level classesNB: Here I am only speaking about the uniform version of AC0, aka the Logtime Hierarchy. 'AC0' is often used to refer to the non-uniform class of polynomial-size bounded-depth circuits. such as \mathbf{AC}^0 are defined using the model of random-access Turing machines. These machines are able to ‘jump’ to any cellThe nomenclature 'random-access' is really not good, since there is nothing 'random' about it. on the input tape by simply writing down the address of that cell in binary. In this way it makes sense to speak of ‘logarithmic-time computation’.

The class \mathbf{AC}^0, in this setting, is now just the languages accepted on a logarithmic-time random access Turing machine which allows alternation, i.e. the machine may have both non-deterministic and co-nondeterministic states. From a descriptive complexity point of view, this means that we can compute predicates that use quantifiers over indices of the input (or other logarithmic-size objects) . Indeed there is a famous characterisation to this effect by Immerman [BIBCITE%%4%], that may be informally stated as follows:

Theorem (Immerman ’87). \mathbf{AC}^0 is just the class of languages recognised by first-order logic on finite structures.

More formally, the first-order signature here consists of basic manipulation of indices, e.g. +, \leq and \max, and predicates for accessing the symbol at each index.

Example. Let us consider the modus ponens rule of Hilbert-Frege systems:

    \[\dfrac{A \quad (A \to B)}{B}\]


We can verify that a triple of strings (\sigma,\tau,\pi ) forms an instance of this rule with the following \mathbf{AC}^0 predicate: there is an index i<|\tau| such that,

  • \tau(0)=``("  \ \wedge \ \tau(i)= ``\to" \ \wedge \ \tau(|\tau|-1)= ``)" ; and,
  • \forall j<i . \ \sigma(j)=\tau(j+1); and,
  • \forall j<|\pi|. \ \pi(j)=\tau(i+j).

Here I am writing, say, \sigma(i) to denote the symbol at position i of the string \sigma. As convention, indices start from the left at 0 and finish on the right at |\sigma|-1.

Log-time hierarchy with counting (aka \mathbf{TC}^0)

Now the class \mathbf{TC}^0 is obtained from \mathbf{AC}^0 by adding an oracle for counting. More precisely, we may query at any point the number of symbols satisfying an already defined property. It might not seem like much of a change, but it is enough to stump complexity theorists: we have no nontrivial lower bounds for \mathbf{TC}^0. In fact, as far as we know, \mathbf{TC}^0 could equal \mathbf{NP}!

Example (Buss ’87). Buss gave a \mathbf{TC}^0 algorithm for formula verification in his seminal paper on the complexity of the Boolean Formula Value problem [BIBCITE%%5%], which we sketch a variation of here. Let us consider formulas generated by the following grammar:

    \[A \quad ::= \quad p \quad | \quad \neg A \quad | \quad (A \vee A) \quad | \quad (A \wedge A)\]

We can check that a string \sigma is formula as follows: for every index i<|\sigma| we have that:

  • \sigma(i)\sigma(i+1) is not a forbidden adjacent pair of symbols for formulas, e.g. pp,p\neg ,(),\vee(,\wedge\vee; and,
  • if \sigma(i)=``\vee" or \sigma(i)=``\wedge" then \exists j,k with j<i<k such that \sigma(j)=``(" and \sigma(k)=``)" and the number of “(” and “)” in \sigma(i,j) is identical.

The point is that if \sigma is not a formula, then there must be some minimal substring \sigma' that occurs in a correct context (i.e. \sigma becomes a formula if we replace \sigma' with a propositional variable) but is not a formula.

Note that there is a subtlety here about how propositional variables are coded, since there are infinitely many of them. A common and natural implementation, that suffices for our purposes, is that propositional variables are simply coded as strings with symbols distinct from the rest of the signature.

Further details on low-level complexity classes.
Hide details on low-level complexity classes.

Proofs as parsing certificates

However, one could imagine that a proof, as well as verifying the truth of a formula, also acts as a parsing certificate, at the same time verifying the syntactic correctness of the conclusion. Seen this way, the problem of checking syntactic correctness actually lies at the other end of a proof: the axioms. To check that an expression is an ‘instance’ of an axiom involves, in particular, checking that the expression is a formula. This yields a \mathbf{TC}^0 lower boundNB: I know we can always 'pad out' the representation of an object to make its syntactic verification easier, but I am not interested in that here. I am only consider 'natural' representations of proofs, a notion that itself I accept is contentious. on checking, say, Hilbert-Frege style axiomatic proofs.

But what about systems where the axioms are atomic? Gentzen style sequent systems are the natural point of call. Indeed, taking a cedents-as-lists implementation seems rather promising, and indeed is the variant originally proposed by Gentzen. However, we hit another problem, namely the weakening and additive rules:

    \[\dfrac{\Gamma \to \Delta}{\Gamma, B \to \Delta}\qquad\dfrac{\Gamma \to \Delta}{\Gamma \to \Delta,B}\qquad\dfrac{\Gamma,A\to\Delta}{\Gamma,(A\wedge B)\to \Delta}\qquad\dfrac{\Gamma\to \Delta,A}{\Gamma \to \Delta, (B\vee A)}\]

The problem with the rules above is that, in each case, the expression B could be arbitrary and we only know that the conclusion is syntactically correct if we know that B is a syntactically correct formula. A complete sequent calculus typically contains either the first two rules (and multiplicative \wedge–l and \vee–r) or the second two rules (and contraction). Some calculi absorb weakening into the identity, but this gives us the same problem as for Hilbert-Frege systems since axioms are no longer atomicIn fact, the calculus remains complete if we insist on atomic axioms, since weakened formulas can always be decomposed. However this does not seem natural, proof theoretically, and, moreover, comes at an exponential cost in proof size. (see [BIBCITE%%6%] for a selection of such calculi).

Other classical proof formalisms exhibit the same problem of ‘new formulas’ occurring, top-down. For instance in natural deduction it is the elimination rules that are problematic. So I am left with the following curiosity:

Question. Is there a ‘natural’ proof system for which proof checking is in \mathbf{AC}^0?

One point of call could be deep inferenceDeep inference is a proof methodology that allows rules to operate arbitrarily deep inside a formula, as opposed to just on the main connective. proof theory, where all structural rules can be made atomic. (Note that this is impossible in sequent style systems, cf. [BIBCITE%%7%]). Such systems, in a sense, enjoy ‘local’ proof checking, though it does not seem that this has been formalised in the setting of computational complexity. For now this is beyond the scope of this post, but I aim to cover the complexity of checking deep inference proofs at some point in a future post.

Some special cases of efficient checkability

Notice that logics without ‘weakening behaviour’ do admit proof systems with \mathbf {AC}^0-checkability. The simplest such example is that of Multiplicative Linear Logic, whose rules in a one-sidedA 'one-sided' calculus usually refers to a sequent calculus where the LHS is always empty. The adequacy of such a calculus is an immediate consequence of De Morgan's laws. system are as follows:

    \[\dfrac{}{1}\qquad\dfrac{}{p,\bar p} \qquad \dfrac{\Gamma,A,B,\Delta}{\Gamma,B,A,\Delta}\qquad\dfrac{\Gamma}{\Gamma,\bot}\qquad\dfrac{\Gamma,A \quad \Gamma, B}{\Gamma,A\otimes B}\qquad\dfrac{\Gamma,A,B}{\Gamma,A\parr B}\]


The weakening issue described above becomes present as soon as the additive connectives or exponential modalities are included.

There are also many systems that operate with a restricted syntax of formulas, such as clausesA clause is a disjunction of literals., e.g. Resolution. The problem of proof checking here is much simpler since we do not need to determine scoping. In particular, \mathbf{AC}^0 proof checking is possible with an appropriate implementation of the rules. For example the following conventions will suffice:

  • Clauses are implemented as lists, so that clause-identity is in \mathbf{AC}^0.
  • The cut rule insists that the resolved literals occur in some fixed position in a clause, e.g. at the beginning or the end.
  • The structural rules exchange and contraction are explicit, due to the previous two points.

From the point of view of \mathbf{AC}^0, it does not matter if the proof is tree-likeI.e. each premiss is used only once. or dag-likeI.e. a proof is a sequence of clauses, each of which is inferred from previously occurring clauses.. This difference does, however, affect the amount of time taken in traversing the proof deterministically without random access.

References

Leave a Reply Cancel reply

Your email address will not be published. Required fields are marked *

Meta

  • Register
  • Log in
  • Entries RSS
  • Privacy Policy

Search

© 2023 The Proof Theory Blog | Powered by Minimalist Blog WordPress Theme
The Proof Theory Blog uses cookies, but you can opt-out if you wish. For further information see our privacy policy. Cookie settingsAccept
Privacy & Cookies Policy

Privacy Overview

This website uses cookies to improve your experience while you navigate through the website. Out of these cookies, the cookies that are categorized as necessary are stored on your browser as they are essential for the working of basic functionalities of the website. We also use third-party cookies that help us analyze and understand how you use this website. These cookies will be stored in your browser only with your consent. You also have the option to opt-out of these cookies. But opting out of some of these cookies may have an effect on your browsing experience.
Necessary
Always Enabled
Necessary cookies are absolutely essential for the website to function properly. This category only includes cookies that ensures basic functionalities and security features of the website. These cookies do not store any personal information.
Non-necessary
Any cookies that may not be particularly necessary for the website to function and is used specifically to collect user personal data via analytics, ads, other embedded contents are termed as non-necessary cookies. It is mandatory to procure user consent prior to running these cookies on your website.
SAVE & ACCEPT