<p>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$.</p>

<p>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.</p>

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

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

CC BY-SA 3.0
2012-10-25T14:48:59.443Z
2012-10-25T15:07:23.673Z
2012-10-25T15:07:23.673Z
Andrej Bauer
<p>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.</p>

<p>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 <em>lines</em>, 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$.</p>

<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.</p>

CC BY-SA 3.0
2012-10-25T14:48:50.327Z
2012-10-25T14:48:50.327Z
Yuval Filmus
<p>I'm trying to under stand the paper <a href="http://eccc.hpi-web.de/report/2010/008/download/">On p-Optimal Proof Systems and Logic for PTIME</a>. There is a notion called <em>proof systems</em> in the paper and I do not get the intution:</p>

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

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

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

<p>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 ...</p>

<p>Any ideas?</p>

<lo.logic><descriptive-complexity><proof-complexity>
Intuition behind proof systems
Joachim
# Intuition behind proof systems

(Asked by: username_0 on 2012-10-25)

I'm trying to under stand the paper [On p-Optimal Proof Systems and Logic for PTIME](http://eccc.hpi-web.de/report/2010/008/download/). 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?

**Tags:** lo.logic, descriptive-complexity, proof-complexity

---

## 2 answers

### Answer by username_1 on 2012-10-25. Score: 8 | Accepted answer

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 by username_2 on 2012-10-25. Score: 5

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.


---

