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.


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


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.


  • 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.
  • 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).
  • 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.
  • 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.
  • Beame, 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.
  • 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.

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