Define a finitary combinatorial principle to be a first-order sentence which is valid in the finite but falsifiable in the infinite. We aim to compare the strength of such principles over bounded arithmetics. We distinguish “weak” and “strong” principles based on their behaviour with respect to finite structures that are only partially defined. We show that over relativized T^1_2 “weak” principles do not imply “strong” ones. The proof applies a general forcing method to produce models of relativized T^1_2.
Logic seminar
usually takes place each Monday at 16:00 in IM, rear building, ground floorChair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.
Forcing with partial structures
Moritz Müller
Universitat Politècnica de Catalunya
Wednesday, 13. November 2019 - 14:00 to 15:30
The symmetric calculus and monotone interpolation, Part 2
Pavel Pudlák
Institute of Mathematics
Monday, 11. November 2019 - 13:30 to 15:00
In this talk I will say a little bit more about the topic that I presented this spring. First I will ask and explain the problem whether the symmetric calculus simulates Frege systems. Then I show how one can strengthen the characterization of the canonical and interpolation pairs. The result can be viewed as monotone interpolation by certain generalizations of monotone Boolean circuits, called bounded depth game schemas. I will also show simulations of point-line game schemas by depth-2 games and vice versa.
The symmetric calculus and monotone interpolation
Pavel Pudlák
Institute of Mathematics
Monday, 4. November 2019 - 13:30 to 15:00
In this talk I will say a little bit more about the topic that I presented this spring. First I will ask and explain the problem whether the symmetric calculus simulates Frege systems. Then I show how one can strengthen the characterization of the canonical and interpolation pairs. The result can be viewed as monotone interpolation by certain generalizations of monotone Boolean circuits, called bounded depth game schemas. I will also show simulations of point-line game schemas by depth-2 games and vice versa.
Why are Proof Complexity Lower Bounds Hard?
Ján Pich
Institute of Mathematics
Monday, 21. October 2019 - 13:30 to 15:00
We formalize and study the question of whether there are inherent difficulties to showing lower bounds on propositional proof complexity. We establish the following unconditional result: Propositional proof systems cannot efficiently show that truth tables of random Boolean functions lack polynomial size non-uniform proofs of hardness. Assuming a conjecture of Rudich, propositional proof systems also cannot efficiently show that random k-CNFs of linear density lack polynomial size non-uniform proofs of unsatisfiability. Since the statements in question assert the average-case hardness of standard NP problems (MCSP and 3-SAT respectively) against co-nondeterministic circuits for natural distributions, one interpretation of our result is that propositional proof systems are inherently incapable of efficiently proving strong complexity lower bounds in our formalization. Another interpretation is that an analogue of the Razborov-Rudich 'natural proofs' barrier holds in proof complexity:... more