slideshow 3

Logic seminar

usually takes place each Monday at 16:00 in IM, rear building, ground floor
Chair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.

LEARN-Uniform Circuit Lower Bounds and Provability in Bounded Arithmetic
Marco Carmosino
Boston University
Monday, 14. June 2021 - 15:45 to 17:15
We investigate randomized LEARN-uniformity, which captures the power of randomness and equivalence queries (EQ) in the construction of Boolean circuits for an explicit problem. This is an intermediate notion between P-uniformity and non-uniformity motivated by connections to learning, complexity, and logic. Building on a number of techniques, we establish the first unconditional lower bounds against LEARN-uniform circuits. For example:

For each k >= 1, there is a language L in NP such that circuits for L of size O(n^k) cannot be learned in deterministic polynomial time with access to n^o(1) EQs.

We employ such results to investigate the (un)provability of non-uniform circuit upper bounds (e.g., Is NP contained in SIZE[n^3]?) in theories of bounded arithmetic. Some questions of this form have been addressed in recent papers of Krajicek-Oliveira (2017), Muller-Bydzovsky (2020), and Bydzovsky-Krajicek-Oliveira (2020) via a mixture of techniques from proof theory, complexity... more

A Diagonalization-Based Approach to Proof Complexity
Iddo Tzameret
Imperial College London
Monday, 7. June 2021 - 15:45 to 17:15
We propose a diagonalization-based approach to several important questions in proof complexity. We illustrate this approach in the context of the algebraic proof system IPS and in the context of propositional proof systems more generally.

We use the approach to give an explicit sequence of CNF formulas phi_n such that VNP \neq VP iff there are no polynomial-size IPS proofs for the formulas phi_n. This provides the first natural equivalence between proof complexity lower bounds and standard algebraic complexity lower bounds. Our proof of this fact uses the implication from IPS lower bounds to algebraic complexity lower bounds due to Grochow and Pitassi together with a diagonalization argument: the formulas phi_n themselves assert the non-existence of short IPS proofs for formulas encoding VNP \neq VP at a different input length. Our result also has meta-mathematical implications: it gives evidence for the difficulty of proving strong lower bounds for IPS within IPS.

For any... more

Introduction to homotopy type theory
Valery Isaev
JetBrains research
Monday, 24. May 2021 - 15:45 to 17:15
Homotopy type theory (HoTT) is a new field of mathematics that blends logic, homotopy theory, and the theory of programming languages. In this talk, I will describe all the components of HoTT including necessary type theoretic construction. I will compare this theory with more traditional set theories like ZFC and show how homotopy theoretic constructions such as spheres and homotopy groups are defined in HoTT. I will also show how to work with such a theory in a proof assistant by providing examples of discussed concepts. Finally, I will discuss one of the open problems in the field.

Proof theoretic properties of truth predicates II
Mateusz Lelyk
Department of Philosophy, University of Warsaw
Monday, 17. May 2021 - 15:30 to 17:00
During the talk we discuss the lengths of proofs of arithmetical sentences in canonical truth theories. We focus mainly on extensions of the canonical compositional truth theory CT^-, introduced in the first talk of Bartosz Wcisło. In particular, we present a proof of the existence of a PTIME computable function f such that for every CT^- proof p of an arithmetical sentence A, f(p) is a PA-proof of A. Our proof relies on the arithmetization and uniformity of the Enayat-Visser model-theoretic construction of models with satisfaction classes. If time permits we shall comment on the speed-up phenomenon for various other truth theories, such as Kripke-Feferman (KF^-) and Friedman-Sheard (FS^-).

Pages