Syllabus and literature for lectures on
Course code: NMAG446
Exam questions.
Student logic seminar.
Mathematical logic, and the problems studied in connections
with foundations of mathematics in the first half of the 20th
century in particular, was one
of key sources of ideas for computational complexity
theory and theoretical informatics at large.
A number of fundamental problems of complexity theory
were formulated first in mathematical logic, and a variety of
concepts and methods of complexity theory have a source in
mathematical logic. The approach of mathematical logic
is an alternative to the combinatorial approach which dominates
complexity theory today, and in some topics yields a
deeper understanding of the underlying issues.
This course will outline several key areas where complexity
theory and mathematical logic meet.
Prerequisites
You ought to be familiar with basic first-order logic
(as, for example, covered in the first three chapters
of van den Dries's lecture notes)
and with basic complexity theory (Turing machines and their
time and space complexity, Halting problem, classes P and NP,
etc: see M.Sipser's book,
Chapters 3,4 and 7, in particular).
Syllabus
The syllabus below describes the ambient space in which
we shall work - not everything will be covered.
What
was actually covered during the particular semester
will be reflected in the exam questions.
Relevant references to literature are given either
by direct links in the text or are listed after
each theme.
Introduction
Entscheidungsproblem, the problem
of the consistency of mathematics, axiom of choice,
...
(Hilbert, Godel, Church, Turing, Kleene,
... ).
"Finitary versions" of these problems and
connections with the
P/NP and NP/coNP problems and with one-way
functions.
The spectrum problem (Scholz 1952 / Asser 1953),
Godel's letter to von Neumann 1956
(a related
paper of S.Buss).
Cook 1971 (the paper formulating
the P/NP problem).
Descriptive complexity
and finite model theory
Examples of properties in (graph of a function, perfect pairing)
and outside of (the odd size of the universe, transitive closure of
a binary relation) FO-definability.
Evaluating FO formulas is in Logspace and Ptime.
Sigma^1_1 and Pi^1_1 formulas and examples (3-colorability,unsolvability of
a set of constraints).
Fagin's theorem.
Spectra are NE sets and Asser's problem as NE vs. coNE.
NE \neq coNE (i.e. spectra are not closed under complementation)
implies that coNP \neq NP \neq P.
Propositional translations of FO formulas and
the NP-completeness of SAT as a corollary to Fagin's
theorem.
The idea of the characterization of
- polynomial time by FO logic augmented by the
least fixed-point operator (the Immerman-Vardi theorem),
- logspace by FO with the transitive closure operator
and the Szelepcsenyi-Immerman theorem: NL = coNL.
Literature:
E.Graedel,
Finite Model Theory and Descriptive
Complexity (a book chapter)
Martin Otto,
Finite Model Theory, lecture notes.
See also lectures of Anuj Dawar at my
2011 Fall school.
Definability in arithmetic
The language of Peano arithmetic, bounded (= Delta_0) formulas
and rudimentary sets
(Smullyan 1961).
The hierarchy E_1, U_1, ...
and an NP-complete set in E_1 (Adleman - Manders).
Coding sequences, Delta_0-definition of the graph of
exponentiation, the Numones function.
The language of binary words, the class of rudimentary sets
RUD (Smullyan'61).
[If time permits: classes
SRUD, RUD^+ (positive rudimentary) a strRUD (strongly rudimentary).
Rudimentary functions and
Bennett's lemma (closure under bounded recursion on notation).
RUD = Delta_0 (Bennett'62), the graph of Exp
in RUD.]
Nepomnjascij's theorem (1970) and its corollary:
Logspace is included in Delta_0.
Linear hierarchy LinH (Wrathall 1978) a polynomial hierarchy
PH (Stockmeyer 1977). LinH = RUD (Wratthall'78): a proof via
Delta_0 = LinH using Nepomnjascij's thm.
The language of Buss's bounded arithmetic (1986) and
PH = Sigma^b_{\infty} (Buss'86).
Literature:
P.Hajek a P.Pudlak:
"Metamathematics of First-Order Arithmetic",
Perspectives in Mathematical Logic, Volume 3
Springer-Verlag, 1998.
(Sections V.2 and V.3 in particular.)
J.Krajicek,
Bounded arithmetic, propositional logic, and
complexity theory, Cambridge University Press, (1995).
Preliminaries
and sections 3.2 (languages) and
5.4 (coding of sequences) in particular.
Witnessing proofs - universal theories
Goal: A computational information from a proof of a theorem.
Herbrand's theorem and witnessing existential consequences
of universal theories.
Model-theoretic proofs: simple for FO statement and a more
subtle one about propositional
provability.
Remark: Statman's lower bound on the
size of Herbrand's disjunctions.
Examples of universal theories related to complexity theory:
Cobham's characterization of
p-time functions and (the idea of)
Cook's theory PV.
Remark: finite basis of p-time functions (Muchnik).
The true universal
theory T_{PV} in the language of PV.
If time permits:
DeMillo-Lipton's theory PT (and its deficiencies).
Some corollaries:
- A set PV-provably in NP \cap coNP is
already in P.
- Unprovability in PV/PT (assuming various
computational complexity hypotheses) of the completeness of
propositional calculus, of the surjectivity of a one-way
permutation, of a collision in a hash-function.
- From an NP witness for primality to p-time algorithm
for it.
The KPT theorem
and witnessing of AEA (and AEAE) formulas. An interpretation
in terms of
interactive
Student/Teacher computations.
Student/Teacher computation of a maximal clique in a graph.
Remarks (if time permits):
- the
unprovability of the existence in PV/PT (assuming
NP is not included in P/poly) and its provability from bounded
induction,
- the finite axiomatizability problem of bounded
arithmetic
and the relation to the collapse of PH.
Literature:
J.Krajicek,
From feasible proofs to feasible computations,
in: Computer Science Logic 2010, A. Dawar and H. Veith (Eds.),
LNCS 6247, Springer, Heidelberg (2010), pp.22-31.
J.Krajicek, Proof complexity, CUP, (2019).
Sec.12.2, in particular (
final draft freely available).
Witnessing in theories with induction axioms
IND and PIND (polynomial-IND) for E_1 formulas.
Open IND in T_{PV}.
Witnessing of E_1-PIND by
polynomial functions.
If time permits: E_1-PIND is
conservative over PV for universal formulas but distinct.
Total NP search problems, examples: PPA, PLS
and PPP.
[Original sources: Papadimitriou
and Johnson -
Papadimitriou - Yannakakis.]
PLS (poly local search)
and witnessing of E_1-IND.
Literature:
Beame et.al.,
The relative complexity of NP search problems,
DOI.
(a logical set-up for relativised problems)
Samuel R. Buss and Alan Johnson,
Propositional Proofs and Reductions between NP Search Problems,
Annals of Pure and Applied Logic 163, 9 (2012) 1163-1182.
(first 10 pages are a good introduction
into logical view of NP search problems)
M. Chiari and J.K.,
Witnessing functions in bounded arithmetic and search problems,
J. of Symbolic Logic, 63(3), (1998), pp. 1095-1115.
Quantitative Godel's theorem
Godel's incompleteness theorems (and Lob's conditions and
Godel's diagonal lemma).
Length-bounded provability predicate and revised Lob's conditions.
Quantitative version of the Second theorem (H.Friedman, P.Pudlak)
and an idea of upper bound.
Connections to P/NP and NP/coNP problems.
Literature:
my notes (rather brief, note
the yellow correction on p.8)
H.Friedman,
On the consistency, completeness and correctness problems,
unpublished manuscript,
Ohio State Univ., 1979.
P. Pudlak:
On the length of proofs of finitistic consistency
statements in first order theories, in: Logic Colloquium 84,
North Holland P.C., 1986 pp.165-196.
an informal discussion is also in Section 6.4 of
P.Pudlak, Logical foundations of mathematics and computational complexity,
Springer, 2013
Godel's theorems:
Smorynski's paper (first 8 pages)
further literature about topic around Godel's theorems
is at 2011 Babylogic page
Proof complexity
Proof complexity connects logic and complexity theory in a number
of ways. For example,
there are several correspondences between natural proof systems
and SAT algorithms based on logic, geometry or algebra,
or there is the general paradigm of
feasible interpolation (and related
automatizability of proof search) relating proof systems
to cryptography, communication complexity, and circuit complexity.
However, proof complexity is the subject of a separate course:
Proof complexity and the P vs. NP problem.
Hence in this course we concentrate (after some necessary basics)
one one particular advanced topic for which there is usually not time in
the above course but which is - in my view - important.
In Spring 2022 this topic is:
The Optimality problem.
This is a fundamental proof complexity problem asking whether
there exists an optimal propositional proof systems (and, in a related
version, an optimal proof search algorithm). It has connections
with a surprising number of areas of logic, complexity theory
or combinatorics.
Ex's of propositional proof systems (pps)
based on
logic: Frege systems F and resolution R
and their "extended" versions EF and ER,
algebra: polynomial calculus PC and Nullstellensatz proof system,
geometry:
cutting planes CP and the SOS system.
SAT algorithms as proof systems: general interpretation and
a specific example of tree-like resolution as DPLL algorithms.
The Cook-Reckhow definition.
NP =? coNP: the fundamental problem.
Simulations and p-simulations between proof systems, examples.
The Optimality problem.
From first-order theories to pps and back: propositional translations:
- theory S^1_2, Sigma^b_1-formulas, feasible Sigma^b_1-completeness,
- definability of satisfiability and provability relations,
- propositional translation of Pi^b_1-formulas,
- reflection principles and simulations,
- corresponding pairs of theories and propositional proof systems.
A relation between the Optimality problem
and the quantitative Godel's theorem, and to NE vs. coNE.
The existence of complete NP search problems, of complete
disjoint NP pairs, ... .
Optimality of proof search.
Literature:
The 1979 Cook-Reckhow paper.
J.Krajicek, Bounded arithmetic, propositional logic and complexity
theory, CUP, 1995.
Secs. 9.2, 9.3 and 14.1, in particular.
J.Krajicek, Proof complexity,
CUP, 2019.
Chpt. 21 is about the Optimality problem.
J.K.,
Information in propositional proofs and
algorithmic proof search, JSL, to app.
J.Krajicek and P.Pudlak:
"Propositional Proof Systems, the
Consistency of First Order Theories and the Complexity of
Computations",
J. Symbolic Logic, 54(3), (1989), pp. 1063-1079.