Intuition behind proof systems

Question

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?

Answer 1

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).

Answer 2

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.