I'm trying to under stand the paper On p-Optimal Proof Systems and Logic for PTIME. There is a notion called proof systems in the paper and I do not get the intution:

$\Sigma = \{0,1\}$ ... We identify problems with subsets of $Q$ in $\Sigma^*$.

I think the intution is that we encode a certain structure in $\Sigma^*$ (e.g. undirected graphs) and subsets of these structures are problems (e.g. planar graphs).

A proof system for a problem $Q \subset \Sigma^*$ is a surjective function $P:\Sigma^* \to Q$ computable in polynomial time.

Now one possibilty is to say $\Sigma^*$ is the set of all possible models in a certain structure (e.g. all the undirected graphs). But that does not make sense because why should a undirected graphs be mapped on a subset? It could be encoded turing machines but this does not make sense either ...

Any ideas?


2 Answers 2


Think of $\Sigma^{*}$ encoding some sort of objects, and $Q$ as the set of all objects satisfying some property. Think of $P$ as a function which accepts (the encoding of) a pair $(x, p)$ where $x$ is an object and $p$ is alleged "evidence" of $x \in Q$. The function $P$ is a "proof checker": it verifies that $p$ actually represents valid evidence that $x \in Q$. If so, it returns $x$, otherwise it returns a default element of $Q$.

As an example, suppose $\Sigma^{*}$ encodes graphs and let $Q$ be the set (of encodings) of Hamiltonian graphs. A possible $P$ is this: decode input as $(G, \ell)$ where $G$ is a graph and $\ell$ is a list of vertices of $G$; verify that $\ell$ is a Hamiltonian cycle in $G$; if so then return $G$ otherwise return the graph on one point.

You considered the case of planar graphs. To get a suitable $P$ we need a notion of poly-time checkable evidence of planarity.

In general the input to $P$ need not encode a pair $(x, p)$. The important thing is that $P$ can extract two pieces of information from its input: the object in question and the alleged evidence that the object belongs to $Q$. For example, let us take as $Q$ the set of all sentences provable in some first-order theory. Now $P$ decodes its input as a formal proof. If the encoding is invalid, it returns $\top$. If the encoding represents a valid proof, it returns the statement that was proved by the proof (which is likely to be the root of proof tree, or the last formula in a sequence of statements, depending on how you formalize proofs).


You should think of the input of the proof system $P$ as the text of a proof $\pi$ of an element $q \in Q$. If the text is valid that $P(\pi) = q$, otherwise $P(\pi)$ is some fixed $q_0 \in Q$. We want $P$ to be polytime since that means that the proof is easy to verify.

As an example, suppose $Q$ is the set of propositional tautologies, and $P$ is any Hilbert-style proof system, which consists of a set of lines, each of which is either an axiom or follows from previous lines via a derivation rule (usually Modus Ponens). If the proof is valid, that $P$ should output the last line in the proof. Otherwise, output some fixed tautology like $p \lor \lnot p$.

Back to your first question, $Q$ is an encoding of all structures of a certain type satisfying some property. One example is tautologies. Another example is the set of all non-3-colorable graphs, which have a proof system known as the Hajós calculus.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.