slideshow 3

Logic seminar

usually takes place each Monday at 13:30 temporarily on Zoom starting at 15:30, normally 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
Zoom meeting 472 648 284 - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz to join
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
Zoom meeting 472 648 284 - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz to join
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
Zoom meeting 472 648 284 - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz to join
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
Zoom meeting 472 648 284 - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz to join
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^-).

Proof theoretic properties of truth predicates I
Bartosz Wcislo
Institute of Mathematics, Polish Academy of Sciences
Monday, 10. May 2021 - 15:30 to 17:00
Zoom meeting 472 648 284 - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz to join
Axiomatic theory of truth is an area of logic which studies this notion in the following way: To a fixed base theory B (which in this talk will be Peano Arithmetic, PA), we add a fresh predicate T(x) with the intended reading "x is (a Goedel code of) a true sentence" and axioms which guarantee that the predicate T has a truth-like behaviour. For instance, we can stipulate that T satisfies Tarskian compositional conditions for arithmetical sentences (obtaining a theory called CT^-) or that it satisfies various forms of induction.

It is a classical result that the theory CT^- with the full induction scheme for the formulae containing the truth predicate, called CT, is not conservative over PA. In fact, it proves so called global reflection principle which says that an arbitrary arithmetical sentence provable in PA is true (in the sense of the truth predicate). On the other hand, a theorem by Kotlarski, Krajewski, and Lachlan shows that CT^- is conservative.

In the... more

Feasible disjunction property for intuitionistic modal logics
Raheleh Jalali
Utrecht University
Monday, 26. April 2021 - 15:30 to 17:00
Zoom meeting 472 648 284 - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz to join
In this talk, we present a uniform method to prove feasible disjunction property (DP) for various intuitionistic modal logics. More specifically, we prove that if the rules in a sequent calculus for a modal intuitionistic logic have a special form, then the sequent calculus enjoys feasible DP. Our method is essentially an adaptation of the method used by Hrubes in his lower bound proof for the intuitionistic Frege system. As a consequence, we uniformly prove that the sequent calculi for intuitionistic logic, the intuitionistic version of several modal logics such as K, T, K4, S4, S5, their Fisher-Servi versions, propositional lax logic, and many others have feasible DP. Our method also provides a way to prove negative results: we show that any intermediate modal logic without DP does not have a calculus of the given form. This talk is based on a joint work with Amir Tabatabi.

Pages

  • 1
  • …