Expressing vs. Proving
Antonina Kolokolova,
Memorial U. of Newfoundland
Sendai, July 22nd, 2011
Relating forms of complexity in logic
Click to edit Master text styles Second level
Third level
Fourth level Fifth level
St. John’s, Newfoundland
How hard is it ?
φ (G) = “Graph G is
connected”
T ` “Reachability is transitive”
What is the path from s to t in G?
To find ?
To prove ? To describe ?
How hard is it ?
Algorithms and complexity
To describe ? To find ?
To prove ?
Bounded arithmetic (proof systems)
Descriptive complexity (finite model theory)
The unrestricted years…
“Is it even possible ?”
Finite model theory Arithmetic
Computability
Göd el, T
urin
g Tra
khten brot
Kleene,Tarski
The restricted times…
“Everything should be
efficient !”
Descriptive complexity Bounded arithmetic
Algorithms/complexity
Complexity theory
Computation with limited
resources.
Complexity theory
Bound time by a polynomial in input length: decidable becomes polynomial-time decidable.
Bound the size of a certificate by a polynomial: r.e. (semi-decidable) becomes NP (non-deterministic polynomial-time computable).
Bound other kinds of resources (e.g., space): log-space (L), constant-depth circuits (AC0)
Complexity classes
AC0 L
NL P
NP co-NP
r.e. co-r.e.
PH
n
AC0: constant time
parallel computation
(addition).
n
NL: non-deterministic
log-space (reachability).
n
P: polynomial-time
computable (most
algorithms).
n
PH: polynomial-time
hierarchy (generalizes
NP).
Descriptive complexity
Expressing properties.
Express a property of a class of structures as a formula φ of some restricted type.
Example: 3-colourability. Graph is a structure with one binary predicate E.
φ = 9 R 9 G 9 B 8 u,v (R(u)Ç G(u) Ç B(u)) Æ
(E(u,v) → “u and v have different colour”)
Descriptive complexity
Application: database theory
Formula becomes query, structure becomes database.
Given a query Q, is there a tuple in the database S on which Q holds?
Q=“Return sets of 4 vertices that are all connected to each other.”
Descriptive complexity
Descriptive complexity
AC0 L NL
P
NP co-NP
r.e. co-r.e.
PH
n
AC0 : first-order logic.
n
NL : second-order 2CNF.
n
P : second-order Horn.
n
NP : second-order 9 logic;
all of second-order logic
gives PH.
FO
SO-2CNF SO-Horn SO
SO9 SO8
AC0 L NL
P
NP co-NP
r.e. co-r.e.
PH
n
The vocabulary has to
include arithmetic (<,+,*)
n
Proofs of equivalence are
similar to Trakhtenbrot’s
theorem.
n
Two logics are equivalent
iff the corresponding
complexity classes are.
FO
SO-2CNF SO-Horn SO
SO9 SO8
Descriptive complexity
Trakhtenbrot’s theorem
“First-order logic is
undecidable over finite
structures”
n
Take a first-order formula with free variables
Statei(t,x) and Symbolj(t,x).
n
Encode the statement “Statei and Symbolj
correspond to correct computation ending in accept”
n
Now, finding a model where this formula holds is
finding an accepting computation.
Bounded arithmetic
Reasoning about
computation.
Fragments of arithmetic where all quantifiers are bounded.
Power of a theory of arithmetic ´ how complex are functions it proves total.
Two theories are the same (=conservative) if they prove each other’s theorems. Two different theories can talk about the same class of functions.
Bounded arithmetic
Bounded reverse mathematics
(Cook, Nguyen)
What is the computational
complexity of concepts needed to
prove a given mathematical
statement?
-- Here the systems are much weaker than in Reverse Mathematics!
Power of reasoning
There are direct translations of the form “a theory proves soundness of a proof system, and each of the proofs in the theory can be done in the proof system”.
AC0 theory corresponds to Bounded Depth Frege proof system; P-theory to Extended Frege.
Systems of arithmetic are
related to propositional proof
systems.
First approach: base theories on bounded arithmetic hierarchy formulas. Does it produce the polynomial-time hierarchy? Buss’ thesis.
Result: NP-theory captures functions of P. If it proves that a function is in NP Å co-NP, the function is in P.
Fine-tuning to small feasible
complexity classes?
Bounded arithmetic
First-order: Buss’s basic theories Si2, Ti2. Have x#y = 2|x|*|y| in the language. Do not capture AC0.
Second-order: First, Buss’s theories for PSPACE and beyond (with x#y).
By Razborov-Takeuti’s RSUV isomorphism, removing x#y and adding second sort (strings) get two-sorted theory Vi1 for the same class.
Sorts are strings and numbers indexing string
positions. No operations on strings other
than length and index.
First vs. Second-order
Complexity classes
AC0
L
NL
P
NP co-NP
r.e. co-r.e.
PH
n
AC0: constant time
parallel computation.
n
NL: non-deterministic
log-space.
n
P: polynomial-time
computable.
n
PH: polynomial-time
hierarchy.
To create a theory, take basic axioms of arithmetic, and add an axiom stating “all objects definable in logic L exist”.
For levels of PH, get the same theories as before.
For non-deterministic classes, so far provably get the functions in the deterministic level of PH.
Descriptive complexity approach
Build theories from logics of known descriptive
complexity
AC0 NL L
P
NP co-NP
r.e. co-r.e.
PH
SO9
FO SO-2CNF
SO-Horn SO
SO8
Systems of bounded
arithmetic
First-order formulas give a theory for AC0. Second-order 2CNF give a theory for NL. Second-order Horn give a (minimal) theory for P.
V
0
V-
Krom
V-Horn
AC0 NL L
P
NP co-NP
r.e. co-r.e.
PH
Systems of bounded
arithmetic
The correspondences are not automatic: recall that a system based on NP formulas captured functions in P.
Need additional conditions on provability of properties.
V
0
V-
Krom
V-Horn
FO SO-2CNF
SO-Horn SO
SO9 SO8
Closure properties
We want robust definitions of complexity classes.
Closure under first-order operations: AND, OR, NOT (hardest one), bounded quantification, and function composition.
NP is not known to be closed under complementation. However, P is robust. Closure properties should be “easy” to prove.
Closure properties
Holds for AC0 from the definitions.
For P, need to formalize algorithms. [Cook, K ‘01,’03]
Surprisingly, proof that NL=coNL can be done with NL
reasoning. [Cook, K’04]
LogCFL done from its circuit (SAC1) definition (Kuroda)
Current proofs for SL (undirected graph reachability)
cannot be formalized in an SL theory. [K’05]. Work in
progress: in which theory can SL=L be formalized?
If proving that a class is closed can be done
inside the class, then the resulting system of
arithmetic captures that class.
Are there easier (non-algebraic)
proofs?
Proof idea
Translate logics from descriptive complexity setting to the language of arithmetic. Define class of theories based on the logics, and show that basic properties (e.g., induction) hold.
Introduce functions into the theory by defining their bit graphs by formulas (not the usual recursion-theoretic definitions).
Generalize Buss’ witnessing theorem to apply to this setting (complicated base case).
Other approaches
Constructing systems by adding to V0 an axiom asserting the existence of a solution to a complete problem (Nguyen/Cook).
E.g., based on versions of reachability problems
Different minimal theories for P, NL, L, etc.
Universally axiomatizable theories
Applicable to small circuit classes such as TC0
Bounded reverse math
Weak theories cannot prove much: AC0-theory does not
prove Pigeon Hole Principle, although a TC0 theory does.
PH-theory formalizes a lot of mathematics (some algebra,
probabilistic reasoning…).
Most work done for P-theory and above, or AC0 theory;
for small classes the area is wide open, although there has
been some recent work (Nguyen, etc).
Which principles does a theory prove?
More in the book
(and Phuong Nguyen’s thesis)
Jordan Curve Theorem (on grid graph) is in
V0(2)
Finite Szpilrajn theorem in VTC0
PigeonHole Principle in VTC0 and not in
V0.
Open: V0(m) ` PHP?
Open: Cayley-Hamilton Theorem (work by
Soltys for some algebra)
Breaking cryptography
with bounded arithmetic
If a P-theory proves Fermat’s
little theorem, then RSA can be
broken.
Breaking RSA
Suppose a P-theory proves
(1 · a < n) Æ (an-1 ≠ 1 (mod n)) ! 9 d (1 <d<n d | n)
All existential statements that are theorems of a P-theory can be witnessed by poly-time functions.
Then some f(a,n) computes d. If n is composite, the hypothesis holds for >half of values of a
(except Carmichael numbers, which can be factored in polynomial time).
Probabilistic polynomial-time algorithm for factoring: choose a at random, compute f(a,n). This breaks RSA.
Provability of separations
Is it independent of arithmetic altogether (like the Continuum Hypothesis) ? Diagonalization does not suffice [BGS].
Any proof that is “natural” does not work [RR] Any “algebrizing” proof does not work [AW]
Independence of PA1 implies existence of a fast algorithm for SAT[Ben-David/Halevi].
Is P vs. NP provable?
Provability of separations
[AIV] define systems with limited knowledge of polynomial-time functions (Cobham’s axioms without minimality).
Natural way to formalize oracle results as independence (both diagonalization [AIV] and algebrization [IKK]).
Conclusion: need locality of computation.
What do we need to know about P and NP to prove
separations?
Provability of separations
Ajtai showed that Parity Principle is not provable in an AC0 theory.
The proof uses heavy model-theoretic machinery: forcing, non-standard models of arithmetic.
Furst, Saxe, Sipser proved that Parity function is not computable by AC0 circuits.
Maybe it is easier to separate
theories than classes?
Conclusions
There is a natural connection between the realms of descriptive
complexity and bounded arithmetic, each of which is closely related to complexity theory. This gives a general method for constructing theories of arithmetic with predefined power.
These theories can be used for bounded reverse mathematics.
Work in progress
A theory corresponding to PPAD and related classes (with Nguyen)
Formalizing expander graphs constructions (with Koucky and Kabanets) Formalizing Reingold and Rozenman/Vadhan
Extending the “relativizing complexity theory” (with Impagliazzo and Kabanets)
Future research
Prove that the theories corresponding to different complexity classes are different. Which techniques are formalizable in weak theories?
How can bounded arithmetic results be used in the finite model theory setting? How can locality be used to prove complexity separations?
Click to edit Master text styles Second level
Third level
Fourth level Fifth level
