Intuition behind proof systems 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?
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).