Syllabus and literature for lectures on

"Logic and complexity", Jan Krajicek

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.


The syllabus below describes the ambient space in which we shall work - not everything will be covered. What was actually covered is reflected in the Exam questions for the particular semester.

Relevant references to literature are given either by direct links in the text or are listed after each theme.


  • 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

  • Evaluating FO formulas is in Logspace. Fagin's theorem.

  • Spectra are NE sets and Asser's problem as NE vs. coNE.

  • 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 Immermann-Vardi theorem).


  • E.Graedel, Finite Model Theory and Descriptive Complexity (a book chapter)

  • Martin Otto, Finite Model Theory, lecture notes.

    Definability in arithmetic

  • The language of Peano arithmetic and the language of bounded arithmetic S_2. Bounded formulas (Smullyan 1961, Buss 1986) and hierarchies E_1,... and Sigma^b_1, ... . The class E_1 contains an NP-complete set (Adleman - Manders).

  • The language of binary words, the class of rudimentary sets RUD (Smullyan). If time permits: subclasses SRUD, RUD^+ a strRUD, rudimentary functions and Bennett's lemma.

  • Linear hierarchy LinH (Wrathall 1978) a polynomial hierarchy PH (Stockmeyer 1977). LinH = RUD (Wratthall), RUD = Delta_0 (Bennet) and PH = Sigma^b_{\infty} (Buss).

  • The graph of exponentiation in RUD (Bennett), Nepomnjascij's theorem and its corollary: Logspace is included in Delta_0.

  • Coding of sequences.


  • 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 Section 3.2 in particular.)

    Witnessing proofs - universal theories

  • Goal: A computational information from a proof of a theorem.

  • Herbrand's theorem, witnessing existential consequences of universal theories. Remark: Statman's lower bound on the size of Herbrand's disjunctions.

  • Cobham's characterization of polynomial time functions and their finite basis (Muchnik).

  • Examples of universal theories: Cook's theory PV and DeMillo-Lipton's theory PT (and its deficiencies).

  • Open induction in PV. 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 formulas. Interpretation in terms of interactive Student/Teacher computations.

  • Student/Teacher computation of a maximal clique in a graph. The unprovability of its existence in PV/PT, assuming NP is not included in P/poly.

    Additional literature (also for the next two themes:

  • 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.

    Witnessing in theories with induction axioms

  • IND and PIND (polynomial-IND) for E_1 formulas.

  • Witnessing of E_1-PIND by polynomial functions. A relation of E_1-PIND to PV: conservative for universal formulas but distinct.

  • Total NP search problems, examples: PPA and PLS. Original sources: Papadimitriou and Johnson - Papadimitriou - Yannakakis.

  • PLS (poly local search) and witnessing of E_1-IND.

    Proof complexity - basics

  • Cook-Reckhow propositional proof systems. P-simulations and p-bounded proof systems. Relation to the NP vs. coNP problem.

  • Examples of proof systems: Frege systems F, resolution R, Extended Frege systems EF and Extended resolution ER, cutting planes CP (8.9.3), polynomial calculus PC, proof systems from theories.

  • Examples of simulations: F and F^*, ER and EF.

    Additional literature, good also for all remaining themes:

  • J.K., Proof complexity, CUP, 2019.

    Proof systems and algorithms

  • DPLL SAT algorithms and tree-like resolution.

  • A lower bound for R^*.

  • Read-once branching programs and regular resolution proofs.

  • A hint on general correspondence: proofs of reflection principles and simulations (see Sec.1 or Chpt.6).

    Feasible interpolation

  • Feasible interpolation: general definition and theorem for R (see also 9.3.5 and 9.3.7 in Pudlak's survey).

  • Automatizability of proof search and its relation to feasible interpolation.

  • One-way permutations and the failure of feasible interpolation for strong proof systems (Sec.9. - general formulation and based on RSA).

    Disjoint NP - pairs

  • Disjoint NP-pairs and p-reductions among them.

  • Reflection principles as disjointness of two NP sets. Relation to feasible interpolation.

  • Optimal proof systems and complete disjoint NP-pairs.

  • Optimal proof search algorithms, information in proofs.

    Additional literature:

  • J.K., Information in propositional proofs and algorithmic proof search, JSL, to app.

    Propositional simulation of first order theories

  • Propositional translation of first order formulas. Main example: Delta_0(R) formulas.

  • Proofs in Delta_0(R)-IND and families of tautologies with short Frege proofs.

  • Other examples: PV and ER, ... .

    Possible additional topics if time permits

  • The finite axiomatizability problem of bounded arithmetic and the relation to the collapse of PH.

  • Finitistic Godel's theorem and its relation to the existence of an optimal proof system.

  • PHP and weak PHP. Provability of its instances for bounded formulas.

  • ...