problems where we knew that optimal
solutions were (NP-) hard to find, even
near-optimal solutions are hard to find.
We discuss these connections soon after we discuss the definitions of PCPs.
equivalent to this verifier. In such cases, when the set of theorems does not
change, but the “proofs” may, we call
the new system a “proof system.” So, a
proof system V would be equivalent to
V if the following conditions hold:
0
Definitions
We start by formalizing what we mean
by “theorems,” “proofs,” a “format”
for proving them, and what it means to
“change” such a format, that is, what
changes are allowed, and what qualities
should be preserved. Hopefully, in the
process we will also manage to establish
some links between the topic of this article and computer science.
To answer these questions we go to
back to the essentials of mathematical logic. A system of logic attempts
to classify “assertions” based on their
“truth value,” that is, separate true
theorems from false assertions. In particular, theorems are those assertions that
have “proofs.” In such a system, every
sentence, including theorems, assertions, and proofs, is syntactically just a
finite string of letters from a finite alphabet. (Without loss of generality the
alphabet may be binary, that is, {0, 1}.)
The system of logic prescribes some
axioms and some derivation rules.
For an assertion to be true, it must be
derivable from the axioms by applying a sequence of derivation rules. A
proof of an assertion A may thus be a
sequence of more and more complex
assertions ending in the assertion A,
with each intermediate assertion being
accompanied with an explanation of
how the assertion is derived from previous assertions, or from the axioms.
The exact set of derivation rules used
and the complexity of a single step of
reasoning may vary from one logical
system to another, but the intent is that
eventually all logical systems (based on
the same axioms) should preserve two
essentials aspects: The set of theorems
provable in any given system of logic
should be the same as in any other.
Furthermore, proofs should be “easy”
to verify in each.
This final attempt to abstract the
nature of a logical system leaves us
with the question: What is “easy?” It is
this aspect that led to the development
of Turing and Church’s work on the
Turing machine. They ascribed “
easiness” to being a mechanical process,
as formalized by the actions of some
Turing machine. Modern computational complexity is little more careful with
this concept. The task of verification of
a proof should not only be “
mechanical,” but also “efficient,” that is, should
be polynomial time computable. This
leads to the following abstract notion
of a system of logic: A system of logic Completeness: If A is a theorem (in V ),
0
is given by a polynomial time verifi- then A is a theorem in V. Furthermore,
cation algorithm (or simply verifier) there is a proof of A in V that is at most a
V ( , ), that takes two inputs, an polynomial factor longer than its proof
..
assertion A and some evidence E and in V .
0
produces a Boolean verdict “accept/ Soundness: If A is not a theorem (in V ),
0
reject.” If V (A, E) = accept then then A is not a theorem in V.
and E is a proof of A. If A is an assertion such that there exists some E
such that V (A, E) = accept, then A is
a theorem. In contrast to the notion
that a proof is easy to verify, our current state of knowledge suggests that
proofs may be hard to find, and this
is the essence of the theory of NP-completeness. Indeed the ques-
11, 25, 27
tion “is NP = P?” is equivalent to the
question “can every theorem be proved
efficiently, in time polynomial in the
length of its shortest proof?”
In what follows we will fix some
system of logic, that is, some verifier
V and consider other verifiers that are
0
By allowing different verifiers, or
proof systems, for the same system of
logic, one encounters many different
ways in which theorems can be proved.
As an example, we show how the NP-completeness of the famous problem
3SAT allows one to produce formats for
proofs that “localize” errors in erroneous proofs. Recall that an instance of
3SAT is a logical formula f = C Ù C
. . .
1m
where C is the disjunction of three lit-
j
erals (variables or their complement).
The NP-completeness of 3SAT implies
the following: Given any assertion A
and integer N, there is a 3CNF formula
f (of length bounded by a polynomial
