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

### A Lower Bound for k-DNF Resolution on Random CNF Formulas via Expansion

##### Dmitry Sokolov
EPFL
Monday, 5. June 2023 - 16:00 to 17:30
Random d-CNF formulas are one of the few candidates that are expected to be hard to refute in any proof system. One of the frontiers in the direction of proving lower bounds on these formulas is the k-DNF Resolution proof system. In this talk, we discuss known lower bounds for Res(k)-proofs of Random d-CNF formulas. We show that for lower bounds it is enough to have only expansion property of the dependency graph that implies lower bounds even in a regime with large clause density.

### Continuous combinatorics

##### Leonardo Coregliano
IAS Princeton
Monday, 22. May 2023 - 16:00 to 17:30
The field of continuous combinatorics is the study of (large, dense) combinatorial structures using tools typically associated with continuous objects, such as tools from analysis, topology or measure theory. The field started under the name of "graph limits" since the main object of study were graphons, i.e., limits of graphs. Since then, several other limits have been constructed for all sorts of combinatorial objects (e.g., digraphs, hypergraphs, permutations, etc.) and even general limits were provided through the unifying theory of flag algebras.

However, the limits constructed in the theory of flag algebras are of an algebraic/syntactic nature, due to the minimalist nature of the theory (as opposed to the more semantic/geometric nature of the previous ad hoc limits of the literature). In this talk, I will present the semantic/geometric counterpart to flag algebras: the theory of theons. I will also give a couple of examples of proofs both within continuous combinatorics and... more

### A simplified lower bound on intuitionistic implicational proofs

##### Emil Jeřábek
IM CAS
Monday, 15. May 2023 - 16:00 to 17:30
Unlike classical Frege systems, we know exponential lower bounds for some non-classical logics (modal, superintuitionistic, substructural), starting with seminal work of Hrubes (2007); they are all based on variants of the feasible disjunction property that play a similar role as monotone feasible interpolation for classical proof systems. This might suggest that disjunction is essential for these lower bounds, but Jerabek (2017) adapted them to the implicational fragment of intuitionistic logic. This results in a complex argument employing an implicational translation of intuitionistic logic on top of the proof of the lower bound proper, which in turn relies on monotone circuit lower bounds (Razborov, Alon-Boppana).

I will show how to prove the exponential lower bound directly for intuitionistic implicational logic without any translations, using a simple argument based on an efficient version of Kleene's slash. Apart from Frege, it applies directly to sequent calculus and (dag-... more

### Unearthing the Feasible World: A Proposal

##### Amirhossein Akbar Tabatabai
University of Groningen
Wednesday, 10. May 2023 - 16:00 to 17:30
The decades-long practice of complexity theory and bounded arithmetic provided some strong clues for the existence of an alternative yet rich feasible world, where for instance all the functions are feasible and the polynomially and exponentially bounded sets are the new finite and infinite, respectively. The situation is similar to the so-called computable and continuous worlds whose traces first unearthed in constructive mathematics and later realized by the forcing-style model constructions that elevated to a general and conceptual theory called the topos theory. In this talk, imitating the main ideas of topos theory, we propose a program to provide a general machinery for the feasible forcing in order to prove some independence results for weak arithmetic, on the one hand and find a conceptual understanding of the low complexity computation, on the other.

As we will see, any fulfillment of that proposal needs a certain (geometric) form of structural theory and one... more