[Proof Complexity] Prague seminar on Monday - Iddo Tzameret

[thapen]

Iddo Tzameret will give a proof complexity talk in our online logic 
seminar on Monday, at 15:45 Prague time - see the announcement below.

To join go to
https://cesnet.zoom.us/j/472648284?pwd=ZTlxeHhqWlltR1AzZC9CTHgzZ2tRZz09
Passcode: 017107 (if required)

-------------------------------------------------------------------------

Iddo Tzameret, Imperial College London
A Diagonalization-Based Approach to Proof Complexity

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 strong enough propositional proof system R, we define the 
*iterated R-lower bound formulas*, which inductively assert the 
non-existence of short R proofs for formulas encoding the same statement 
at a different input length, and propose them as explicit hard 
candidates for the proof system R. We observe that this hypothesis holds 
for Resolution following recent results of Atserias and Muller and of 
Garlik, and give evidence in favour of it for other proof systems.

Joint work with Rahul Santhanam