Skip to main content
Loading Explore guides…
Lower Bounds · Acedra
Home
Explore
Computer Science
Lower Bounds
Sign in to save
Chat
If YouTube asks you to sign in, open the video on YouTube.
Watch on YouTube
Reload player
Transcript
431 segments
Copy
Hide video
0:00
[ANTONINA KOLOKOLOVA] --for a whole minute. So shall we start? [MOSHE VARDI] Yeah, let's get started.
0:08
[ANTONINA KOLOKOLOVA] So welcome everybody to the session today, and we have a fantastic cast of speakers. I'm really looking forward to that.
0:17
So just couple of housekeeping things. If you are an attendee and you want to ask questions raise your hand. If you are a panelist and you want to ask questions you can unmute yourself, you, I think all the speakers are okay with this and/or you could post things in the chat.
0:45
And what else?
0:49
We'll gather down after that.
0:52
Uh, so let me, without my-- much more housekeeping, you remind me if I forgot something, introduce our first speaker today, and I'm really, really, really happy to have Sasha
1:06
Razborov gives the first talk today.
1:11
I've heard it before and it's beautiful. So you--
1:16
Speakers today hardly need any introduction, but just to mention one of the main thing that Razborov was famous for being one of the few people who proved lower bounds, original lower bounds for monotone circuits.
1:38
He had done beautiful work in bounded arithmetic and
1:44
proof complexity in bounded arithmetic. Last last Wednesday we talked about RSUV
1:54
isomorphisms, for example.
1:57
And he's also well known for probably the most important barrier result in circuit complexity and also bounded arithmetic, is a natural proof barrier. And hopefully you might hear a bit about it today. In addition to that done some quantum
2:24
complexity, communication complexity, some other complexity and some deep mathematics.
2:31
Mm-hmm. Algebra stuff. Um he
2:36
unsurprisingly got numerous prizes for that just to mention the Gödel prize for the barrier results for natural proofs, and I think an Ivan Lienas' prize for circuit lower bounds. There is way too much to say, but I'd rather let him speak for himself, so please, the floor is y--
2:59
[ALEXANDER RAZBOROV] All right. Thank you very much, Tonya, for the nice introduction. Again if you want to ask questions, please unmute yourself and ask, highly preferred method. So, and first of all this talk today will be highly speculative, and it is, I apologize that it's about some-- somewhat old stuff. Uh, I will talk here at Simon's, I mean virtual talk somewhere in my-- in May on more modern things. And
3:35
another apology I already made is that some of you or many of you have seen this talk before, a longer version of it, but I still hope I made a few changes. All right. So we start with our favorite program, P versus NP. I think at this point in the game everyone here knows what it is, but we are going to tweak this equation a bit. So the first version we may ask, and that's how it was attacked, people tried to attack it it's-- in this form. It's a slightly stronger version,
4:18
and it's asking whether languages in NP have polynomial size circuits. Let me remind you that P/poly is anything is non-uniform P, which means everything you can compute with its polynomial size circuits. So then we can further relax this question and ask, are there any explicit Boolean functions not in P/poly, which explicit being in good old sense, in mathematical sense, not necessarily in P or something which you would recognize as explicit.
4:56
And so then we may ask this question,
5:00
which looks ridiculous, but as we will see, it is not, at least for the purposes of my talk today. And this question is
5:14
this question is actually even more relaxed version, are there any Boolean functions that cannot be computed by polynomial size circuits? Well, of course I have put here a question mark, but of course, we all know that it is the case, it's classical result by Shenam
5:40
uh, somewhat verified by Lupanov later, and it says that it is indeed the case, and we have functions and actually almost all functions are hard. So here is some notation, C of FN is the circuit size of my function F in some standard basis, so almost all of them are exponential. Almost all functions are exponential and that's basically the on the whole proof. It's simple application of the Pidgon-Hale principle, but let's look closer at this proof. So what's really going on is that if you want
6:22
to run these arguments, then you want to be able to count really well. Uh, and by really well, I mean you are going to be able to count really large numbers, so you want to count up to double exponential sign-- uh, double ex-- uh, double exponent in the number of variables because it's the overall number of your Boolean functions, or at least up to this number, but still you have to count really a lot. And that's that will be the main theme in my talk today
6:58
is that actually, right, the main principle is what you can do depends on how well you can count. Right. So maybe you should use it in K-12 education in our classes on arithmetic, but that's really that will be the dividing line. Everything will depend on what is the maximal number you can see in your arguments, and you can count up to that number.
7:30
So, let me now revisit this question.
7:34
Are there any Boolean functions not in P slash poly? And for the purposes of my talk, first of all, we are going to be interested in proof theory. So we are going to study whether this equation is provable somewhere or not or using some class of methods. And if there are any logicians here or proof theorists, then we will understand for the purposes of this talk we will understand proof theory slightly more broadly. It's not necessarily a first order theory or prepositional theory.
8:13
It's something that some class of methods that you can rigorously define it that work you don't compromise on.
8:26
It must be rigorously defined, but other than that, it can be described by various means and natural proofs that we will see is one of the examples. So, and let me now put here my favorite, one of my favorite sentences because well, you do algorithms, you do whatever, you prove theorems, and when you cannot do something, then you start to explain others why you are so stupid. And as you see, this principle was not invented by complexity theorists, but still,
9:00
that's basically what we are going to do in this talk. As I said, it's highly speculative, so let me-- And yes, I forgot to say that we will be, it will be one of our guiding principles is that we will be interested in our proof systems, again, broadly understood, for which even that statement is supposed to be hard. So
9:31
only in those proof systems in which you can, first, formulate the statement, and second this blue word, "any", does not make your life any simpler. [AUDIENCE MEMBER] So [ALEXANDER RAZBOROV] Proving that NP is not in P slash poly is supposed to be more, or at least as hard as proving it for any Boolean functions. Let me briefly state a few motivations.
10:00
Right.
10:03
So, first of all, because mathematicians do it. We know great independence result in mathematical logic term of choice, continuum hypothesis, or Gödel's incompleteness theorem, and it's self-explanatory that it is interesting.
10:20
Uh, the second motivation it actually started in the book by Gary Johnson '79 o-- '79, and as many of you know, in the first chapters, they carefully laid down this principle that the theory of NP-completeness is good for many reasons, but one of them is that you can explain to your boss why you cannot do the job. So that's the second reason. The third reason it is of course because since these problems so far mathematics never gave up on its problems.
11:04
It kept solving them if necessary, for centuries, and as we know, eventually they get solved. So we have to continue around, so like in complexity theory, computational complexity theory, I mean, it is the same hope. We are going to focus
11:24
our research in the right direction by just saying what and why does not work. So it's the ideology that we used in our paper on natural proofs. Of course well as we-- uh, as Steven and me had expected, everyone misused that sentence and took the paper like "Don't do circuit lower bounds, do something else." Well, we cannot do anything about it. It was not our intention. Our intention was just that we showed what does not work, and let's take it from there.
12:02
And the third but also impor-- fourth, I'm sorry, but also very important motivation is of course about byproducts. So again, that's what complexity theory is about. You prove something totally useless and then something comes out of it that makes a difference in the real world, even if you're or just saying sort of happens in this business as well. All right, so what's next? So Diagonalization it was the first operator, was the first barrier. Let me go over this slide very quickly.
12:48
So it's a proof system in my sense, right? So if you have a complexity result, then the proof system, it simply says that it should be true in all Oracle worlds. It's well-defined. It's not, of course, like the usual proof system.
13:03
Uh, but still it is rigorously defined and we all know this classical theorem by Baker, Gill, and Solovay, is that this proof system is not capable of doing, of proving either P is equal to NP or it's complete. That's probably the first manifestation that was probably the first manifestation of this idea that the proof system is not necessarily rules and axioms in first order logic. It might be something else, but something reasonable.
13:37
So what does it mean to be reasonable? Again, let me try-- So four will be a magic number for some reasons throughout my talk. Let me formulate four constraints and wish list that I would like to have in a framework that barrier or proof system, whatever you like to study these kind of things, I mean. So the first, of course is that your proof system should not be able to solve this equation in the obvious way by counting. And it rules out strong proof systems like those.
14:22
Well Shai probably will disagree with this, but we will we will listen to what he can say in an hour about stronger proof systems.
14:35
So what's for, for the purpose of my talk, I really don't want to be I really don't want Shannon arguments to be formalisable in my proof system, er, because it's it's not an interesting proof. I want it to be out.
14:56
So the second which is very important very important is that if you take your favorite result in circuit complexity, and we do have a few results as you know, and so by the way, it is an excellent book, one of the best books I've ever seen.
15:15
So if you take any result from this book, then you really don't want to work hard on
15:23
proving it in your system.
15:28
You don't want to write papers, you don't want to introduce something some new concepts. You just take it and it should be doable in your system in a straightforward way.
15:41
So hence, returning to my counting theme, turns out that now all those results are, well, exact, of course, from the book. Exact, of course for the chapter that talks about Shannon counting arguments, that Lupanus improvements all other results, they use only counting up to polynomial in the number of instances. So little n, of course, stays everywhere for the number of variables, so it is just polynomial in the number of your instances. So all those proofs, they use counting only up
16:20
to this number, which is single exponential in n.
16:27
Right, so this sort is self-explaining. We really want proof systems that people care about. And it is probably the weakest point of natural proofs, because somehow that's what we cooked up. I will show you what we did in several slides.
16:56
Still we have some motivations, but other than that, usually it should be natural. The proof system should be somehow of interest. I cannot quantify it. And, of course the first thing is that we really want to hope to make progress. So, and in logic, you make progress if
17:24
usually if metamathematics of your proof system, so what you can extract from rules basically, it somehow matches mathematics. So Gödel's incompatibility theorem, it is metamathematics is formulas that you prove. You encode them And then it is the same mathematics about integers your proof system is arguing about. And if it looks very if it looks abstract to you, then let me point out this recent breakthrough r-- result by Albert and Müller, Albert Atzeres and Müller.
18:00
They proved something extremely concrete in proof complexity, not only extremely concrete automatability of resolution, but it-- But what has been open for decades, and they really use this self-referring argument. So it's not, if you are interested in concrete things, then you are still, you still want to hear it, right? Here, Shai again probably disagrees with this, uh--We are going to listen to it later.
18:35
All right, so let me remind you what are natural proofs. And I will be very quick because you know, this talk is about something really relevant but still something else. So these are two pieces of common wisdom. So the first one is that if you want to prove lower bounds for Boolean functions, then you should look at how it looks like, study its properties, and then move it to lower bounds. And the second piece of wisdom, it says that if you want to analyze your proofs, then you should carefully
19:13
look into them do a proof system, and blah, blah, blah. So the starting point of natural proofs is that we dismiss both of them. So namely, instead of even trying to understand what our proof looks like, so we are going to think about it, sometimes creatively. It's sometimes it's not straightforward. And then we are going to conclude that the same argument can be applied not only to your function of interest, but to a great deal of other functions, which
19:54
which gives rise to the set of Boolean functions, P_n, to which your arguments can be applied in a sense and so that's the only thing we need in our we need in our model. So we only look at this set P_n, and then we formula-- formalize, so sorry, it should be P_n. So in-- wait sorry, P_n and C_n on this slide are the same, so, and then we simply write the properties of this set of functions. First of all, of course, we want it to make sense,
20:39
and the second two properties they are debatable but still that's what happens in our all or almost all known proofs. And
20:52
you really want to understand what you are doing,
20:57
so which means that our set P_n must be co-- computable in polynomial time in this quantity, and it must have large density. So once you have a good method, then you really are going to be able to apply it to sufficiently many functions. Usually, it is even better than that, usually, it is just almost all functions, but so to be on the safe side.
21:28
So let us check against our four items from the wishlist
21:40
there is no obvious counting solution you cannot count, so that's why we have here constructiveness,
21:44
right? So if you count up to larger than that number, then it will not be in polynomial time,
21:57
so that is what we called naturalization. So there are some technicalities where it's monotone formulas basically because it is not so easy to define a good distribution over monotone formulas, but more rarely you can do it.
22:25
So as I said this is the weak point of natural proofs, so you can prove, but here is at least one justification for it which is also well-known that it's written here. If you prove that A is hard and your proof system is closed under X_4, then you somehow, and you understand what you are doing, then you should be able to tell which one of these two is hard and it gives you largeness because you have then half of all functions-- And
23:01
here
23:05
on the first r-- item about mathematics versus meta-mathematics it looks it is almost here because our, one of our axioms, it has polynomial i-- inside of it, and we study right, short circuits, small circuits. But the pitch here, of course, is it really a problem that now we have changed our measure, that it's not small and that it is too big. Is it really a problem? Well turns out it is the main and actually the only problem about natural proofs is that you really can prove
23:46
things even in this form. So, that's the main theorem of natural proofs, so modular standards or cryptographic assumptions, there is no natural proof against general circuits. Self-defeating arguments in its.
24:04
Good. So as I said there is lots of work on natural proofs, and people disagree with many of these points. Some people agree. Some people both agree and disagree at the same time
24:22
and let me stop it here. So, and this is one very important byproduct. So it is it will be the same throughout my whole talk that we actually are interested in our inputs. We are measuring our main size measure is this capital M. It will always be the same, which is the number of instances in that problem, which means that your Boolean functions are given as through stable. And one byproduct is that this work with Steiner which had highlighted the importance
25:09
of this problem, which these days is called minimum circuit size problem, which is here. It is obvious. It is the set of all those tables that corresponds to simple functions. And let me just say that there has been a lot of very interesting and wonderful and important research on this problem, and somehow our paper helped to understand its importance and that it is a really good thing for study. So in complexity terms, if we forget about all our motivations, then in complexity terms,
25:50
natural proofs can be easily formulated in terms of this problem as is written here.
26:03
Right, so that's it with natural proofs. Let's move on, and
26:09
so these are the two points. I repeat here, the two points that natural proofs dismiss. Today in the remaining of my time today, we are going to now to still dismiss the first point. As I said, we are interested in proof systems that actually do not distinguish between explicit functions and any functions, but we want to replace the second point with its opposite. So we really want good proof systems in the good old sense of formal theories. And, of course, as Antonina already said, there
26:55
is lots of work about it, so here I
26:58
really want to say just just a bit. So bounded arithmetic is just Peano arithmetic where you focus on bounded quantifiers, bounded bi-terms, so you also have sharply bounded quantifiers. And it is important that it is just a normal first-order theory.
27:22
It's no catches axioms, inference rules. So again, as almost all of you or all of you know as to one is the most important theory in the whole family. There is a hierarchy. There is a family hierarchy. It closely models complexity hierarchy, but I don't have much time today, so I will talk only about S21. And the fourth item in my wishlist, it is answered by this fundamental theorem by Sam Bass.
28:00
It's from his book about bounded arithmetic that basically started this whole subject, is that if you prove something existential in this area, and A is simple, it's a predicate number, you have But, you know, then it can be witnessed by polynomial time function. So we see here polynomial time that corresponds to meta-mathematics, a powerful system, and it's the same concept we are going to study. Therefore it's good news for us.
28:36
Mm-hmm. So, sorry, it should be S21, S21 reversed. So now again it's a shorter version of the talk. I have to skip many details that I gave before, but you can formalize the equation we are interested in. So here I put sub-exponential function to avoid certain trivialities, and this is the equation, whether we can prove the existence of a Boolean function fn--So
29:15
Right there is no obvious counting solution because we don't know the answer to this equation. We don't know whether it is probable or not. Therefore, there are no counting solutions, obvious counting solutions.
29:32
Right.
29:35
The second part is also very easy and very natural. So if you look at the same statement, but for restricted circuit models you can really do it in the system. It is extremely straightforward. So I did it once, and mostly I focused on the creation are there weaker systems than this where you can prove all that stuff from Stasi's book. And yeah, And so each is very natural, very simple.
30:17
So of course, bounded arithmetic, that what we love for many good reasons. It's not only because we are able to do this stuff.
30:27
And now comes an interesting part. So that I will show on the next slide, and it's good that I was able to get to that slide. So but one clarification is that we cannot hope to get to all the way up to this bounded arithmetic unconditionally. So I like in natural proofs, I do allow you arbitrary reasonable complexity cryptographic assumptions that are short of NP is not equal to co-NP because that makes the whole game trivial. So again it's a short version.
31:09
Let me just mention a competing framework which was
31:17
uh, which is promoted by Jan Krajčík. So in this framework you allow even more restricted counting. You can literally count up to capital M. But
31:32
on the other hand, it's no longer simple existential formulas. You allow lots of quantifiers.
31:39
It's very interesting framework connected in many respects to what I am talking about here, but I don't have time to talk about it. So and now, again, it should be S to 1. So and now we can reformulate our equations. We are interested in terms of prepositional proof complexity because again, there is a catch here. Our beautiful sharply bounded quantifiers, but morally, Szembat's theorem almost implies that if you prove this in S to 1, then should be, there should be some explicit
32:21
sequence of functions for which you can prove the same thing. And once you have a quantifier-free statements or only with sharply bounded quantifier, then quantifiers, then you can translate it through prepositional proof complexity, prepositional logic. You can express it as prepositional formula. The fact that the function FN is hard, and the size of this formula, again, we use our convention or our main principle that we don't care how we encode it. It's simply given by its truth table.
33:02
We have enough memory or enough time to just encode it as a truth table and measure everything as a polynomial in terms of the lengths of these truths. And now comes the main slide. So we have now we have this square, namely, we have proofs in bounded arithmetic.
33:31
And it shares very popular topic connections between bounded arithmetic and uniform complexity classes given by various witnessing theorems. Szembat's theorem was the first theorem from this family. If you have something in bounded arithmetic, a proof in bounded arithmetic S to 1, then you get something polynomial time computable. So if you have Sigma if you have Delta zero be a quantifier-free formulas, then you can translate them through prepositional proof systems.
34:13
And this will give you, you will just work in now in more, much more convenient and more elegant prepositional world. For example, S to 1, again, S to 1 is different. S to 1 gets translated to extended variety.
34:32
So this is also, this connection is very standard in computational complexity. So every uniform complexity class, or essentially every uniform complexity class, you have associated non-uniform class. So what we really need is the fourth arrow,
34:56
right? So you would really expect a fourth arrow on this picture. I give you a prepositional proof it argues about computational concepts, and you want to extract some computation, something computational out of it, and then apply your knowledge like we did in natural proofs or in this implication, apply our knowledge to get conditional results. And it's embarrassing that we almost came up with, and I don't understand why. All right. So let me give you a few definitions for regular
35:36
systems, resolution, extended regular system role. I believe that everyone knows what it is, so I have only less than 10 minutes left, so I don't want to spend time here. All right, so the success story here, and it is precisely a model case of what we would like to have. Ideally, it's called feasible interpolation. That's precisely what we would love to have. So I give you special topology, and it all is applied here. And then you ask, and then you extract
36:22
from it something computational, which is called feasible interpolation. So you can apply it to several systems of interests, but then turns out that you cannot go very far along these lines because simply feasible interpolation fails for more
36:48
for, for stronger systems, for systems that we are really interested. Well I mean, we are interested in all those systems as well as everyone at this workshop already knows why this time, but for different reasons.
37:09
So here is a byproduct of this, one byproduct of this. It is simply because it is simply one quite amazing thing about the complexity is that really
37:25
it is the same phenomenon. Unlike circuit complexity, we really don't know if there are any hard tautologies for Frege or extended Frege proof systems. There is no accounting argument here. So in this paper they tried to come up with some e-- Uh, with so-- some examples, but I guess they indicated themselves that it was not very conclusive and most of those results were solved, I mean short proofs in Frege or X in Frege were found later on. The principle is that these systems are really hard.
38:03
So we really want some arguments that we don't understand ourselves. And at the moment I have only two, and I think everyone has only two reasonably convincing examples of what might be hard for Frege or extended Frege. The first is randomCNFs. It's just because we really don't understand why if you pick a random CNF, why is it unsatisfiable, you'll have to count for that answer. It's beyond the reach of our system and it is-- The second example is coming from this business
38:43
or proving that NPA is not equal-- is not NP/poly. It is the second candidate hard topology, and it is again, it is we don't understand it to the extent that we don't even know if it is true or not, which makes it a perfect candidate. So I have only a few minutes left, so let me very briefly say that we have some ad hoc results for-- So that's now what we are going to study. We are going to try to understand why this thing is difficult for various pre-conditional proof systems.
39:31
We have a few unconditional results, and it also does not go quite far.
39:38
So when-- so that's basically the last thing I want to show and Punia, do we have five minutes? [ANTONINA KOLOKOLOVA] First prover right now. [ALEXANDER RAZBOROV] When? [ANTONINA KOLOKOLOVA] Please. Yes. [ALEXANDER RAZBOROV] Okay, good. So I will try to finish in five minutes. So, and so that's one suggestion that is still it, which made it anywhere. So, improve all this, all the stuff to stronger proof systems. So let me start with reminding you about natural proofs.
40:15
And the way you prove it is that you construct pseudorandom function generator. If you have an ordinary one-way function, then you get an ordinary pseudorandom bit generator out of it, and you can either construct it using general construction by Micali, Goldwasser, and Rackoff, or you can take, for example, Nisan-Wigderson that immediately gives you a conjectural
40:42
function generator. And so this is basically the whole proof. You have to supply few details.
40:50
So the idea is to try to understand what it looks or what it might look like in the propositional world. So again, I have a mapping, I have a proof system P. So our idea was that if I give you a Nisan-Wigderson generator or any other generator, any other reasonable generator, and I give you identically zero string--- Right? And I ask you, is it true or not that this string is not in the image of your generator, is not generated by any seed, then it's really impossible to know.
41:33
So if your generator is reasonable, then you cannot answer this basic question. You cannot really pinpoint any particular string in the image of the generator that is not in the co-domain of your generator, that is not in the image. And that's what we take as a definition of our hardness. So the idea is of course that we can use-- So if I give you any string B, then your proof system does not prove that B is not in the image of the seed.
42:11
So answer, the proposal is simply to try to somehow write a pseudorandom generator to something that is well-studied in computational complexity. And so the proposal is, of course, to search for this missing fourth arrow, using maybe at least as our inspirations what is known in the computational world. So in a sense, good news is that it's-- or it extends feasible interpolation. So if you have feasible interpolation for your systems, then you basically can do it with the slight
42:58
twist of your generator. And this is the main conjecture, is that if you take any Nisan-Wittestein generator just for simplicity and for concreteness, and you base it on any function, then it becomes hard for extinct regular systems. So that was made almost 20 years ago. There has been some work, but not much on it, and it is still wide open. And basically, that was the main purpo-- one of the main purposes of my talk is to draw attention to this conjecture. So here is what we know.
43:38
We don't know very much. So we know this conjecture for reads, Resolution reads, for Polynomial Calculus, for even for resolution it is frustrating because we don't know yet for exponentially what many output bits on the M squared.
44:01
And it is ve-- very important work by Jan Krajicek. So which is again the same principle. You can iterate this generator so-- as you do
44:13
in circuit complexity and for example, for Resolution, you can get slightly better. You can get 2 cube. And so that's probably the best you can do at the moment. It is the proof system where you can lift this stuff. So our pseudorandom generator for this system, well, I hope you know what it is, which is the strongest system for which we know these statements.
44:41
So and as I mentioned several times, there are many other suggestions. So often that the-- the obvious open problem, so it-- it should stay as to one, it is just the same Y, R, S, U, V isomorphism Tonia mentioned before. So it is the main conjecture. Again it is connected to model theory somehow. So now we have had several breakthrough results in cutting planes in several last years. But as far as I know, they formally don't imply unconditional hardness of this statement.
45:21
It would be a great program, accessible problems, or accessible problem, I mean. Well, unless I missed something and there is a simple reduction, which I don't see. So probably it's hardness for cutting planes or sum of squares, as far as I know, it is open. Unconditionally conditional, you can apply feasible interpolation. And the same equation for bounded depth Schradin. We missed some techniques basically, or randomizations were not suited very well for the task.
45:56
But these people, they explained to us that it is much more versatile method than we had thought about it. So again, even for resolution, we have also apply other methods. We don't have pseudorandom generator for resolutions. That is really in the range we are interested in, and it's variables because, Yeah, It's variables creation. Right.
46:24
[ANTONINA KOLOKOLOVA] Thank you so much. This is fantastic. This is such an inspiring talk. Applause for everybody. Questions comments please.
46:36
[MOSHE VARDI] I have a question. [ANTONINA KOLOKOLOVA] Mm-hmm. Mm-hmm. [MOSHE VARDI] So you motivated the search for natural proof by you didn't want to have counting up to W exponential.
46:49
But that can be then, you could have said that the proof should be of exponential length, so the proof should be in P space.
46:57
Why not take a similar definition of natural? [ALEXANDER RAZBOROV] Uh, no it's, uh-- Uh-huh.
47:08
So, no it is, it is not what we want to achieve. It's, I view it as a test for what we're-- what we are doing is right. It's sanity check. I view it only as a sanity check. Right. It's not like I really-- it's not my purpose. But simply if your system be it natural proofs or anything else, if it does not pass this check, then it means that, again it's not what you're interested in. Okay. It's not the purpose, but it's excellent comment. Thank [MOSHE VARDI] You. Okay thanks.
47:59
[ANTONINA KOLOKOLOVA] More questions?
48:01
[AUDIENCE MEMBER] I can ask a question? [ALEXANDER RAZBOROV] Mm-hmm. Mm-hmm. [AUDIENCE MEMBER] You ended with the comment about lifting versus natural proofs, so I was wondering if you think there's any connection between the two and the techniques or the [ALEXANDER RAZBOROV] Approaches? Oh no no no no no. Let me, uh-- Or I think it's more, again, I had to revise, which mean randomize my large talk we did here, right?
48:35
So in the long version, it refers only to this result. [AUDIENCE MEMBER] Okay. [ALEXANDER RAZBOROV] So natural proofs are, so it comes, it comes here in this business where if you have a system with feasible interpolation, right? And you want a pseudo-random, natural pseudo-random generator, then you will do very primitive lifting, extremely primitive. But still, you do it.
49:10
Is there anything like that for natural proofs or for other systems?
49:16
It's very limited creation.
49:20
Okay. Such as in
49:25
[PAVEL PUDLAK] This diagram that you have on the slides so you were asking about the arrow on the bottom. Mm-hmm. So your proposal is to, to use this what Jan Krejcik calls tau formulas?
49:39
What formulas? Tau formulas.
49:43
This formula saying that something is not in the image of a pseudo-random generator. Yeah yeah.
49:49
This should be the arrow down. [ALEXANDER RAZBOROV] It's multi-faceted. So and it's main-- Is [PAVEL PUDLAK] It, is it your conjecture or, or that this is the right arrow, or you suggest it as one possibility, [ALEXANDER RAZBOROV] Or? Yeah yeah. No, this conjecture is made in my annals paper.
50:09
It's quite official. Mm-hmm. Or are you asking in the reverse direction? So, if you just-- No, I'm [PAVEL PUDLAK] Asking wh-- whether th-- this-- You propose this as the solution of what the arrow should be. So I know that you proposed this conjecture, but Yeah. --do You [SHAI BEN DAVID] Propose [PAVEL PUDLAK] This as a, as the-- Yeah. The only solution of this arrow, or-- Well, [ALEXANDER RAZBOROV] Well-- Just one of the solutions? Well, this solution has extremely well maybe a bit
50:43
dirty, but extremely powerful, something extremely powerful behind. It might be bad, it might be totally incorrect, but we don't have anything else. [SHAI BEN DAVID] Mm-hmm. [ALEXANDER RAZBOROV] At least I am not aware of anything that I would recognize as a project, as a plan to get it. I tried, I had to try lots of things. [PAVEL PUDLAK] Mm-hmm. [ALEXANDER RAZBOROV] And it's very frustrating. You have an object, right? Which is essentially a sequence of circuits, polynomial-sized circuits.
51:17
Every one computes, Each one of these circuits computes one, because it's a tautology,
51:24
and you want to get some computational content out of it, and you fail.
51:32
I don't understand why. Even in 30 years, I guess, I still don't understand why we fail.
51:40
So it is a, it is simply, it's like democracy. I would compare this to random generators with democracy. It may be a bad system, it may be a lousy system, but it's better than anything else. [ANTONINA KOLOKOLOVA] Mm-hmm.
51:59
I have a quick question. So you were talking about S12 as kind of the right system, the right power to talk about complexity. But in recent years, people have been working with systems that formalize probabilistic reasoning, APC1 and friends. What do you think about that? [ALEXANDER RAZBOROV] Hmm. First of all, it is definitely a very interesting line of research. And I certainly don't want to say anything negative about it. But somehow, I feel that--
52:44
You mean this one, Yeah?
52:48
Okay. [AUDIENCE MEMBER] Um. [ALEXANDER RAZBOROV] Somehow I-- Mm-hmm. --don't feel quite strongly in terms of this thing.
53:03
It looks like the systems, they in many cases, they were somehow to formalize or capture particular things. It's not the case with bound arithmetics, right? [SHAI BEN DAVID] Mm-hmm. [ALEXANDER RAZBOROV] Bound arithmetic was not invented to prove something or analyze proofs. It was invented to capture polynomial time. It's not with Peano arithmetic, not the case with Peano arithmetic. It was-- Mm-hmm. --meant to capture all finite arguments. Somehow these systems I'm not sure that they-- Yeah.
53:45
[ANTONINA KOLOKOLOVA] Thank you. Thank you so much. So more questions, comments? [SHAI BEN DAVID] Can you go back to the slide where you have this generator that you talk about?
53:59
[ALEXANDER RAZBOROV] From what--I'm sorry. The [SHAI BEN DAVID] Nisan-wigderson generator the first time that you talked about it. [ALEXANDER RAZBOROV] No, no, it's not back.
54:07
It's forwards.
54:13
[SHAI BEN DAVID] Yes. Yeah, yeah, this one. All right.
54:19
So can you go back one slide?
54:24
The one where you have the mapping from functions. Yeah, this one. What exactly--
54:31
[ALEXANDER RAZBOROV] Mm-hmm. [SHAI BEN DAVID] What exactly are you saying here? So I'm just trying to understand this. So [ALEXANDER RAZBOROV] I'm saying, I'm saying that if if you take any reasonable generator, for example, Nisan-Wigderson, right? [SHAI BEN DAVID] Mm-hmm. [ALEXANDER RAZBOROV] And I ask you a question like I give you identically zero or almost all strings here are not in the image of this generator. [SHAI BEN DAVID] Mm-hmm. [ALEXANDER RAZBOROV] Yes? [SHAI BEN DAVID] Yeah.
54:55
[ALEXANDER RAZBOROV] If I am asking whether identically zero string is in the image of this generator or not, you will not be able to answer this question. [AUDIENCE MEMBER] Mm-hmm. [ALEXANDER RAZBOROV] Regardless of any complexity.
55:11
Just fix it in any reasonable way. Of course, you can hold this manually. You can manually ensure that it is not there, but if you don't play any tricks, then you will not be answer, you will not be able to answer this question about identically zero string.
55:27
[SHAI BEN DAVID] Okay, thanks.
55:31
[ALEXANDER RAZBOROV] Mm-hmm. And we simply analyze it for all other strings.
55:38
[ANTONINA KOLOKOLOVA] Great.
55:40
Well, thank you so much. This is fantastic. [ALEXANDER RAZBOROV] Thank you, Tonia. So, and I'm now giving floor to Pavel. Let me see how do I stop sharing?
55:56
[ANTONINA KOLOKOLOVA] Thank you. Oh, this is great. So, Pavel, would you like to share your talk and unmute yourself? [PAVEL PUDLAK] Yes. [ANTONINA KOLOKOLOVA] Yeah. [PAVEL PUDLAK] So do you want to make a short break before I start?
56:18
[ANTONINA KOLOKOLOVA] Um, do people want a break now? Do people want a break in, after your talk? Any-- I [SHAI BEN DAVID] Think a five-minute break might be good because we have been at this one hour now. So maybe Tonia? Okay. Yeah. [ANTONINA KOLOKOLOVA] Let's take maybe three, four minutes break. [SHAI BEN DAVID] Yeah. [ANTONINA KOLOKOLOVA] And actually people can use this to ask more questions if you like. And we'll start in four minutes. [PAVEL PUDLAK] Okay.
56:48
I just try sharing my screen so that-- [ANTONINA KOLOKOLOVA] Yeah, yeah, [PAVEL PUDLAK] Please. [ANTONINA KOLOKOLOVA] Yeah. Mm-hmm.
57:09
[PAVEL PUDLAK] So how does it look like?
57:12
[ANTONINA KOLOKOLOVA] It's not full screen, but it's visible.
57:16
[PAVEL PUDLAK] Okay, let me do it, Presentation.
57:33
[ANTONINA KOLOKOLOVA] Oh, yeah, that looks great. [PAVEL PUDLAK] We should be okay. [ANTONINA KOLOKOLOVA] I can see the slides, can see your mouse. That's great. [PAVEL PUDLAK] Mm-hmm.
57:44
So how do I exit this? Okay.
57:53
Yeah, just stretch my legs
58:56
(indistinct conversation)
59:31
[THOMAS F KOCHMANN] Alexander? [ALEXANDER RAZBOROV] Yeah. [THOMAS F KOCHMANN] May I ask an intermediate break question? [ALEXANDER RAZBOROV] Absolutely. [THOMAS F KOCHMANN] Yes. That was very, very amazing talk to me. Um, I-- I'm wondering two questions. First, do you think, what is your personal belief, does a proof system, propositional proof system exist that is strictly stronger than extended Frege?
1:00:12
And second, what might it look like then?
1:00:16
I don't have [ALEXANDER RAZBOROV] Any idea. Also, it's it's actually, Pavel, I think it's a correction for you, right?
1:00:23
[PAVEL PUDLAK] Uh, well, of course Sasha knows very well these things, but-- No no no no no [ALEXANDER RAZBOROV] Not, not about extended Frege. [PAVEL PUDLAK] Not about-- So, so we are uh, already said a long time ago, and I'm going to also in my talk is our quantified propositional calculi or calculee. So where you have the usual sequent calculus formalization, but you use quantified propositions, and they seem to be stronger. So this is just one next step after Frege or extended Frege.
1:01:07
But uh, there are other things like, like
1:01:12
Jan Krejčík's implicit proofs. [SHAI BEN DAVID] Mm-hmm. So you [PAVEL PUDLAK] Can take basically any proof system and make a so-called implicit proof system from it. And this is a kind of jump that we cannot prove that it's strictly stronger, but potentially it could be a kind of jump like a recursion theory that produces a stronger system from one proof system.
1:01:37
And there are other things like taking first-order theories as proof systems for prepositional calculus, and then you get the extremely strong proof systems.
1:01:49
So yes, where to read about it? In the, in Jan's book, of course. Mm-hmm.
1:02:03
[ANTONINA KOLOKOLOVA] Thank you.
1:02:06
[PAVEL PUDLAK] But of course, there are different opinions, so Yeah, can I check things that it's quite possible that these proof systems are not stronger than they are.
1:02:19
[ALEXANDER RAZBOROV] Theoretically, you can believe that NP is equal to coNP, right? [PAVEL PUDLAK] Yes. [ALEXANDER RAZBOROV] Which immediately closes all discretions. [PAVEL PUDLAK] Yeah.
1:02:31
So should I, [ANTONINA KOLOKOLOVA] Uh, so-- Start now? --shall we start? Yeah, if you don't mind putting up the slides. [PAVEL PUDLAK] Okay.
1:02:50
[ANTONINA KOLOKOLOVA] And meantime
1:02:56
-- speakers today need no introduction, but let me still introduce Pavel Pudlak. And if you did anything with proof complexity, you always SAT circuit, you've seen Pavel's name over and over and over again. And from lower bounds, from feasible, I think your name is on most lower bounds in proof complexity that I can think of. Cutting planes the seminal result has lower bounds for cutting planes. Um, from the point of view of metamathematic
1:03:36
Pavel has a great book called Metamathematics of First-Order Arithmetic, and a more recent book, which is a gentle introduction to Logical Foundation of Mathematics and Complexity.
1:03:51
It's gentle, but it still talks about a lot of really advanced concept that Sasha mentioned. Also, if you do algorithm for SAT probably the most well-known algorithm for SAT exponential algorithm is PPAZ. And again this is Pavel's work. So many things that I can't even mention all of them. Circuit complexity as a connections. So I'd rather let Pavel talk about this and the beautiful connection between different areas of complexity in SAT. Please.
1:04:31
[PAVEL PUDLAK] Thank you, Antonina, for a very flattering introduction.
1:04:37
So my talk will be hopefully short and definitely very elementary.
1:04:45
I will not talk about new stuff. I will actually talk about that I have already spoken a couple of times. But each time I still find some details that I can present in a better way or complement things in it. So
1:05:14
I'll start with some background from the foundations of mathematics. We use various theories to formalize arithmetic or set theory.
1:05:27
These theories are of increasing strength.
1:05:32
Here on the slide we have T2 which is bounded arithmetic. So I should have also included S12 that was mentioned before, which is a fragment of T2. Then we have a fragment of Peano arithmetic called I sigma 1, which is induction for sigma 1 formulas. Uh, a stronger theory than that is than Peano arithmetic, is uh, the so-called second order arithmetic, which is not arithmetic formalized in, in this, in the second order
1:06:08
proof calculus because there, there is now any, but it's it's an extension of Peano arithmetic by sets.
1:06:16
Subsets of interpreted as subsets of integers plus non-negative integers. Then Zermelo-Fraenkel theory, and we can go on by adding new axioms such as strongly inaccessible cardinal or the existence of measurable cardinals and obtain stronger and stronger theories. And these theories are stronger, we can prove that they are stronger because of Godel theorem.
1:06:50
And they in fact prove more true pi 1 sentences assuming that these theories are true, that they describe the true sentences of arithmetic. But the question that is interesting for us is whether they prove more sentences relevant to computational complexity. This is what we would like to know.
1:07:20
So this is one thing that we can ask. And another thing is, if you take some theories that differ in a way like P differs from NP and NP differs from Sigma 2P and so on then we can ask whether these theories form an increasing hierarchy. And this is open and probably very difficult problem because here we cannot apply Godel theorem. Of course we cannot prove that we cannot apply the theorem, but we know one thing that the consistency of these theories is, so strong that none of
1:08:11
these theories prove the consistency of the weakest one. So we cannot use the consistency to separate these theories.
1:08:24
Here's an example of what I am very much interested in.
1:08:30
Given a problem and an algorithm that solves P,
1:08:33
what is the weakest theory that proves the soundness of A? By the soundness of A, I mean that the algorithm solves the problem. Or
1:08:45
given a problem and a time bound T, you can ask what is the weakest theory
1:08:51
such that for some algorithm T proves that A solves P in time T?
1:09:04
Here is an example that appears in, you know, paper long time ago. Uh, if factoring is hard, then the theory denoted by S12, which Sasa mentioned briefly, does not prove the soundness of any polynomial-time algorithm for primality.
1:09:22
So we are in the situation that we do know that there is a polynomial-time algorithm for primality but assuming a reasonable conjecture, S12 doesn't prove the soundness of this algorithm. So it's conceivable that there are algorithms that are so complex or tricky or that use deep mathematics that they are not provable in weak systems of arithmetic or set theory.
1:10:02
So for instance, here, we are not able to prove the soundness of AKS algorithm in any fragment of T2. But at the same time, we don't have a reason to believe that it is not provable in T2 except that we don't know how to do it. But there may be ways to argue that it's not possible by placing these things into a hierarchy of total function and P problems. But I am digressing.
1:10:40
So here is what I mean by soundness of an algorithm.
1:10:48
So we have to be careful how we formalize these questions. We can always formalize an algorithm so that ZFC or any fixed theory does not prove the soundness. We can just embed the consistency statements of this theory into the algorithm and then we are not able to prove that it is sound.
1:11:14
But we can ask the opposite question or something formally opposite.
1:11:23
Is it possible to formalize every algorithm that its soundness is provable in peon arithmetic or some other fixed theory?
1:11:34
Now th-- this question is vague and unfortunately, I'm not able to formalize it any way so that it doesn't have a trivial answer. But this is what I would be very much interested. So instead I will show today some related things that are not exactly this question but of the same nature.
1:12:05
Uh, what I, I'm going to present is something that can be uh, presented a-- As a syntactic classes versus semantic classes. Syntactic classes do have complete problems while semantic classes usually do not. And we usually are not able to prove that there is no complete problem but we can argue that there are some good reasons to believe that there are no complete problems. And what I'm going to talk about i-- is three
1:12:49
conjectures or several conjectures that are on the form that saying that there are no complete problems in certain classes.
1:12:59
Uh Russell Impatz doesn't like the word conjecture because he suggests to call things hypothesis. But in this case, it's something that I very much believe that they are true, that we should eventually be able to prove it like we believe that P is not equal NP. So we don't see the-- What is-- P equal NP is a hypothesis. [MOSHE VARDI] Pavel, Pavel? Yes? What is a semantic? Can you define semantic class? [PAVEL PUDLAK] Okay.
1:13:35
So semantic class is a class that is defined in such a way that we have to prove the defining condition [AUDIENCE MEMBER] That the [PAVEL PUDLAK] Problem belongs to the class. So for instance P is a syntactic class because we can present every polynomial algorithm in such a way that we know from the code that you write down that it runs in polynomial time.
1:14:12
This is not, uh-Uh the definition is not a syntactic, but if we uh, if you put into the code of the algorithm a clock that will stop the algorithm after polynomial number of steps, then we know for sure that it will stop after polynomial time. And the dog makes noise here. I will have to do something. Uh, but other classes uh, typically uh, randomized classes are not of this form. We write down an algorithm and you accept this as a definition
1:15:03
of the set in this class if you prove that it accepts the input with certain probability or not. Sorry, I have to make [ALEXANDER RAZBOROV] Sure to see what's going [MOSHE VARDI] On. The dog doesn't have a mute button? [PAVEL PUDLAK] No.
1:15:26
Okay, so he's now quiet. Okay, so let's go on. [MOSHE VARDI] No, my question is, when we use semantic class, we're actually very loose about it because I can always ask when you say all the algorithms in some time, I say, "In what set theoretic universe are you talking about?" [PAVEL PUDLAK] Mm-hmm. [MOSHE VARDI] So my claim is that when we use semantic classes, we are really very loose and if we try to be precise, we will have to be better
1:15:53
defining to say in what class of models are we talking about.
1:15:59
[PAVEL PUDLAK] Well I don't understand this. So I think that the semantic class is defined precisely a lot like RPPPP because they are, they may be for the P And then they are not semantic anymore because they can be defined syntactically. But otherwise they are semantic. So uh-- Excuse
1:16:32
me.
1:17:07
Sorry. So this dog is very clever. He can open the doors, so it's difficult to contain him somewhere.
1:17:16
So anyway this is not a precise definition but we will see examples and maybe it will be better to look at the examples that I will present. Is it okay Roshka?
1:17:38
[MOSHE VARDI] Yeah. Sasha just gave a good answer. Uh, I'm happy with his answer. [PAVEL PUDLAK] Okay.
1:17:46
Yes maybe--
1:17:49
[ANTONINA KOLOKOLOVA] So yo-- you have to say uh, Sasha said in the chat, "In semantic, there is no recursive enumeration of machines computing languages from this class." [PAVEL PUDLAK] Say it again.
1:18:00
[ANTONINA KOLOKOLOVA] Semantic, there is no recursive enumeration of machines computing languages from this class. [PAVEL PUDLAK] Yes. Yes. The reason why we do have complete problems in syntactic classes is because we can enumerate the algorithms. Of course it may not work always because the enumeration may be not so effective but this is just a rule of thumb. It's not a precise statement.
1:18:35
So let's get to examples. So the first item on my list or in the title is the set of tautologies. So let's restrict to DNF tautologies, but this is not important, just to be more concrete. We have proof systems and a proof system is something that is complete that there is a proof for every tautology, and sound, that it doesn't prove non-tautologies. The completeness is easy to ensure by embedding some well-known proof system into it and then say it,
1:19:24
if we believe that the resolution is complete, then we can add to each proof system resolution and then we know that it is complete based on the assumption that resolution is complete and we don't have to prove essentially anything.
1:19:49
But the soundness is a problem. So if you have a very strong proof system, then you have to prove that it is sound. It's not, it may be a non-trivial thing.
1:20:04
So this is how they are defined. And then we have polynomial simulations. I'll not define them because we know this very well that you can, if you want proof system and the other proof systems simulate this proof system means that you can simulate the proofs of one system in the other. So there is polynomial time function that translates proof systems from one into the other.
1:20:36
And the conjecture is that this condition of soundness is indeed syntactic that we cannot prove it easily, which means that there is now a consistent theory that proves the soundness of all proof systems.
1:20:59
So this may be one possible statement of this conjecture and which is not maybe completely obvious but easy, that this is equivalent to the condition that there is no proof system that simulates all other proof systems. I will call this optimal proof systems. An optimal proof system is that simulates all proof systems. And also, I am omitting the specification polynomial, so simulates mean polynomially simulates, effectively that you have polynomial time computable functions.
1:21:38
I will not talk about the length of proofs. [ALBERT ATSERIA] Your red "syntactic" should be "semantic", right?
1:21:48
What did you say? Syntactic? [PAVEL PUDLAK] Oh, yes.
1:21:52
This should be "semantic". Thank you. Thank you. Yes. I have
1:22:00
a kind of selective blindness. I cannot proofread my slides very well.
1:22:07
In this [MOSHE VARDI] Conjecture-- Your slides are semantic, not syntactic.
1:22:14
[PAVEL PUDLAK] So okay. And this conjecture is a fairly strong, strong conjecture because in particular, it implies that exponential time is not equal to non-deterministic exponential time.
1:22:30
And this is probably stronger than P is not equal to NP.
1:22:39
There is a related class, which is the class of disjoint NP sets. So this class consists of pairs of sets, A, B, which are in NP, and they are disjoint.
1:22:54
Again, we can define polynomial reductions between two elements of this class.
1:23:01
This is quite natural. Uh, we can use either Turing reductions or many-one, which means that if you have two pairs, then the first set should be mapped into
1:23:15
the first set of the other, and the second should be mapped into the, to the other. So this is something that you can easily imagine.
1:23:23
And now, the condition that these two sets are disjoint is a semantic condition. I have to be careful not to confuse the two things. Semantic because if you write down the definitions of these sets, you don't know whether they are disjoint. Unless you write down some trivial thing like all of the sets in A start with bit zero or all the sets in B start with bit one. So these are easily recognizable but it's easily recognizable that they are disjoint. But in general, it may be hard to prove
1:24:10
that they are disjoint.
1:24:14
So we can state the conjecture that there is no complete disjoint NP pair.
1:24:21
And this conjecture, again, is equivalent to the statement that there is no consistent theory that proves the disjointness of all the disjoint NP pairs.
1:24:33
Now, I am stating this conjecture, at least the second part is stated a bit not quite precisely because what does it mean that the theory doesn't prove that a pair is not disjoint?
1:24:54
Whether the theory proves that the pair is disjoint
1:24:58
definitely depends on how you formalize these pairs. So you need to write down a formula if you want to talk about its probability.
1:25:10
So to state this precisely, what I would need to say that it does not prove the disjointness of all NP pairs. However, you formalize the pair. So you take the best formalization for which it should be the easiest way to prove that they are disjoint and for this you are still not able to prove it in some theory. I mean, you are still not able to prove it in the theory.
1:25:45
All right. So how these conjectures are connected. To show that they are connected one can use the very important concept of canonical pairs of proof systems. If we have a proof system P, then uh,
1:26:18
the canonical pair of the proof system as defined by Sasha is consists of a set of basically you can view it as, uh, formulas that are, that have short proofs but to be more precise, what we use we are using the padding that uh, limits the, the, the length of proof. So it's a pair of formula and a number represented in unary, such that the phi doesn't have phi has a refutation of length at most end. And the second set is basically sad, but we need something that looks similar to AP
1:27:11
So we also use padding but it is just a padding that does nothing.
1:27:20
So this pair somehow captures the strength of the proof system because if P simulates Q, then the pair corresponding to Q is polynomial reducible to pair corresponding to P.
1:27:44
This is very easy to prove.
1:27:46
And the corollary of this is that the conjecture about disjoint NP pairs implies the conjecture about proof systems for propositional tautologies.
1:28:05
Now let's get to total function NP.
1:28:13
So TFNP means total function NP which I define in the following way.
1:28:23
A problem in total function NP is given by a binary relation that is computable in polynomial time and a polynomial bound such that
1:28:36
the relation defines a multi-valued but total function. That is, for every A, there it is B, which is at most polynomially longer than A such that it satisfies the relation. So this polynomial bound is given just to be quite precise, but typically the polynomial bound is already implicit in the relation R so I will often omit this polynomial bound and talk only about the relation.
1:29:16
The problem associated with this relation which has this property is to find for a given A, to find B such that it satisfies the relation.
1:29:33
So now, again, this condition is semantical.
1:29:44
That you, if you have the definition, if you have a formula for R or a polynomial time algorithm computing this binary relation, you never know for sure that this defines a total function. So you have to prove in some theory. Now again, we have reductions between these problems. Now I will just use R and R prime for these problems. And, and these relations, this reduction are defined in the obvious way, we have either many-one relations or Turing relations and it makes no difference for,
1:30:29
for the conjecture that I'm going to state. Okay, so this many-one reduction is given by two polynomial time computable functions, F and G.
1:30:42
So you want to compute
1:30:46
a witness for A in the relation R and you can do it in such a way that you first compute FA and find a witness for R prime. And from this witness B and A, you get the witness for A in relation R. But it may be more complicated to just using oracle for the solution of R prime.
1:31:16
Anyway, so we have class and we have reductions, and then we can ask whether there is a complete problem.
1:31:28
But let's just take an example so that we are sure that this concept is not empty that there are probably total function NP that are not solvable in polynomial time. Because if everything is solvable in polynomial time, then everything will be reducible to everything. So then there will be a complete problem.
1:31:57
So factoring is an easy example of a problem that is not solvable in polynomial time. But it's based on the assumption that it is hard.
1:32:13
So the hardness of factoring simply means that this total function NP problem is not believed to be computable in polynomial time. So we have at least two different types of total function NP problems, those that are solvable in polynomial time and those that are not. The conjecture about total function NP is, however, much stronger than that than just saying that there are problems that are not solvable in polynomial time. The conjecture is that there is no complete total function NP problem.
1:32:55
So this far more stronger than saying that there is one problem that is not solvable in polynomial time.
1:33:06
And again, this can be stated in logic that there is no consistent theory that proves totality of all total function NP problems.
1:33:24
These are, of course, hopeless conjectures because they imply P and QNP.
1:33:30
So do we have any reasons to believe that they are true? One reason why I believe is this is true is that it's very much like the like computable functions in provably total computable functions in theories. If you have increasing theories with increasing strength,
1:34:04
then you can show that also the class of provably total computable functions increases in the strength of the theories. It does not have to increase, always increase, but at least in the examples that I showed at the beginning this is the case. So the only difference here is that in total function NP, everything is polynomial, while here it is computable. So this formal similarity is one reason to believe that they may be true.
1:34:42
The other reason is that we already have characterizations of provably total functions provably total NP-functions in fragments of bounded arithmetic.
1:35:00
And these characterizations are of increasing complexity. We cannot show that they are of increasing complexity indeed, but at least formally they are of increasing complexity. Unfortunately, we are still not able to prove that at least in relativized work they are of increasing complexity. So this is one of the big open problems in,
1:35:29
in proof complexity to show that uh, that this hierarchy of total function and P-problems is increasing. This is something that is not hopeless.
1:35:41
I believe that it only requires proving some very complicated switching lemmas but so far nobody was able to do this.
1:35:54
Like with the set of tautologies we also have a similar connection which are disjoint coNP, pairs of disjoint coNP sets.
1:36:11
Again polynomial reductions and during or many-one are defined in the same way.
1:36:19
And we can state the conjecture that there is no complete disjoint coNP pair. Again, it's a syntactic class so this is equivalent to, if true then there is no fixed here that proves disjointness of all coNP pairs.
1:36:49
And we have a similar connection as before, namely that the conjecture about addition grand P pairs implies the conjectures about total function in P problems.
1:37:09
So the situation so far is that we have two branches of conjectures. One is about tautologies and addition in P pairs and another is about total function in P and addition grand P pairs.
1:37:34
But SAT is still missing and you can now guess where SAT is.
1:37:43
It's not obvious, so we will look at what, at SAT. So I want to spend a, a bit more time with SAT because this is uh, a program in SA-- uh, at Simons, Simons which is focused on SAT.
1:38:03
So SAT is of course very much different from OAT. But we also can consider proof system for SAT.
1:38:15
And a proof system, what is a proof system for SAT? It's just any evidence that proves that a formula is satisfiable.
1:38:26
What are polynomial simulations? They are exactly same as for OAT that you transform proof in one proof system into a proof in another proof system in polynomial time.
1:38:45
But the difference is that there is a, the standard proof system, one very special proof system, and this is just satisfying assignments. If you want to show that a formula is satisfiable, then the best you can do is to provide a satisfying assignment.
1:39:10
And this is, this proof system is polynomial bounded.
1:39:14
While we believe that there is no polynomial bounded proofs for tautologies, we have trivially polynomially bounded proof [ANTONINA KOLOKOLOVA] System [PAVEL PUDLAK] For [ANTONINA KOLOKOLOVA] Sat. Uh well, I'm sorry for interrupting if we're really running over time, but, uh-- Oh, sorry. If you can take couple more minutes. [PAVEL PUDLAK] Oh, sorry. I thought I was, -- [ANTONINA KOLOKOLOVA] Uh uh, I, I'm sorry. We've been quite relaxed, but just realized, sorry. [PAVEL PUDLAK] Okay.
1:39:47
I don't have many slides and I skipped something, so I will finish. Five minutes or it's okay, [ANTONINA KOLOKOLOVA] Or? Oh no. Sorry for that. I just looked at the clock. Oh. [PAVEL PUDLAK] Yes. So mm.
1:40:05
Okay. So we so the situation is different.
1:40:13
But still there may be proof system that are not polynomially bounded.
1:40:21
Now an example of a proof system for SAT that is probably not polynomially simulatable by the standard proof system is the following one. You take the standard proof system and you add basically factoring into it, which means that you take as a proof any satisfying assignment or if the formula expresses that N is not a prime, then N will be just the proof of this. And it
1:41:01
is not difficult to see that if factoring is hard, then the standard proof system does not simp-- polynomially simulate this system because if it did, then we would need to, we would get a satisfying assignment for, for formula Phi, and this is what what we believe is not possible. All right.
1:41:24
So let me quickly go over this natural proof system for SAT. Uh, you can get natural proof system for SAT if you realize that uh, Phi is in SAT if the existential, existentially quantified formula has a quantified tautology, is quantified tautology. And then you can use proof system for quantified tautologies.
1:41:57
And you have to go faster.
1:42:00
Uh, what is interesting that the standard proof system polynomially simulates the G star 1, and I'll tell you the details about it.
1:42:09
And the point is that
1:42:14
is the, the witnessing theorem of, of Cook. So the bottom line is that if you have a witnessing theorem in a proof system, then it essentially means that the standard proof system polynomially simulates it.
1:42:35
Okay.
1:42:38
If there is an optimal proof system for SAT, then there exists a complete problem in total function NP. I wanted to prove this, but we don't have time. So it's a pity because it's a simple proof.
1:42:57
So let me finish by saying that we can state the conjecture that SAT doesn't have an optimal proof system. And what and the proof that we skipped gives us that total function NP conjectures implies the SAT conjecture. So we can place SAT into the diagram, and it is between
1:43:21
P unequal NP and total function NP conjecture. Now in these things have been rectified,
1:43:31
so we know that many things are different.
1:43:36
In particular, these two branches are really distinct branches. But unlike showing these implications which are usually easy and more or less straightforward, relativizations are pretty technical and complicated. So we still don't know whether these two are different and these two are different. Okay.
1:44:06
[ANTONINA KOLOKOLOVA] Thank you. Thank you so much, Pavel. This is really, really interesting. Okay. We are running a bit over time, but maybe
1:44:21
--Moshe has a question.
1:44:23
Okay. Just [MOSHE VARDI] A quick question. [ANTONINA KOLOKOLOVA] Yep. [MOSHE VARDI] So, so Harvey Freedman has this program showing that this stronger set theories end up proving kind of a, you need strong set theory to prove very mathematically looking statement about kind of numbers, just statement about number theory and things like that. Mm-hmm. And I wonder whether you can use his program to show that these stronger sets theory like axiom cardinal,
1:44:52
strong cardinal axioms, prove things that actually they have computational meaning.
1:45:01
[PAVEL PUDLAK] I wish I could But I cannot. Yeah. So the problem is that essentially what we would-- we are able to do is just somehow to rephrase the consistency in some combinatorial way But it's not anything that can be interpreted as a statement about computational complexity.
1:45:35
But but this is well, I would like to do it and I'm thinking about it, but I don't know how to do it.
1:45:46
[MOSHE VARDI] Thank you. [ANTONINA KOLOKOLOVA] I think, yes, thank you so much. And maybe while Shai is setting up, if anybody has any more questions for Pavel? And thank you so much, Pavel. This is fantastic. This is really interesting. Uh, [PHOKION KOLAITIS] Antonina, may I ask a question? Mm-hmm. Uh, Pavel, thank you for the talk, first of all. My question is the following, consider the conjecture that NP intersect coNP, which is a semantic class,
1:46:16
he has no complete problem, where would this conjecture fit in your diagram of connections between the conjectures? [PAVEL PUDLAK] This doesn't fit into any of the branches so it's in the middle. It's, it's stronger than, of course BIANCO and P But it's in the middle, so we are-- uh, I-- I'm not sure that we can
1:46:47
show by relativization that it is not in any of the branches, maybe if Hanneke de Lief is connected, he can tell you more but it seems that this is in between. [PHOKION KOLAITIS] Thank you. Mm-hmm. [ANTONINA KOLOKOLOVA] Thank you so much. [PAVEL PUDLAK] And it's possible that there is a third branch which is based on this But I don't know other than this problem in this direction. So sorry for being a bit longer than expected. [ANTONINA KOLOKOLOVA] Oh I'm sorry for kind of making it
1:47:26
more long than it needs to be. Thank you so much, Pavel. It's been beautiful. So if you don't mind, let's postpone question till later and give up with the talk and go to town and start our grand finale of today's. Uh, which is the talk by Shai Ben-David about as you could see if P versus NP can be independent of the axioms of reasoning. And so just a couple of words to introduce Shai Ben-David, his work spans a really vast range from kind of,
1:48:07
from set theory of se-- kind of, really deep set theory to really practical machine learning with algorithm and complexity and logic and all sorts of things in between. And Shai can connect all those disparate things and show the relations where you know, it's hard to imagine that there could even be relations. For example independent result of a machine learning problem this is one of your NeurIPS best paper awards, right? [SHAI BEN DAVID] No, not this [ANTONINA KOLOKOLOVA] One. Oh, this one?
1:48:49
Not this one? Okay, so you have other papers which got NeurIPS best paper awards and such. Anyway, so Shai's work spans huge area and it's really beautiful and today he is going to tell us about the really cool result about SAT and P versus NP and independence. Please. [SHAI BEN DAVID] Okay. Yeah. So I'll try to be more technical. I know what we're running behind time So Yeah. So I-- I want to look at this question of whether P versus NP can be independent of set theory and here, I mean,
1:49:21
as in contrast to-- to what Sasha was saying when you look at negative results, the stronger the system you can show that cannot prove something, the more, the stronger the result is. So I'm talking, I'm really e-- interested in much stronger systems So I'm not going to talk about SAT or anything, how to solve SAT but, uh-- so what was the talk about? So when you're faced with some hard mathematical problem, there is always the temptation to think that maybe this problem
1:49:53
is inherently irresolvable, maybe the reason that we fail to find answers is not our lack of wisdom but rather than no answer, no proof exists. I mean that's following Gödel. We know that this is always a possibility when we're facing an open problem. So the goal of this research was to see, try to ask why do we fail to resolve some basic computational complexity questions? Could it be that P versus NP or other computational open problems are unresolvable in set theory which means
1:50:29
we have no tools of proving that the answer? And more concretely, is it likely that, right? That the tools that we have in mathematics are inherently too weak to determine relationship between complexity classes?
1:50:48
So, I mean, if we believe in such a direction then we should direct our efforts to answering these logical oriented questions rather than strangle with directly computational complexity issues because maybe it's hopeless. Maybe by showing that-- I mean and that's, you know, the-- the kind of, the line of research as Sasha was taking and-- and others in, in this community that don't try this direction because it's, it's a futile. So
1:51:19
what do we know about independence proof? Just to remind everybody of it. Independence proof of set theory. So Hilbert's program was to-- the hope to develop a form of method that will resolve all mathematical questions. And of course, Godel's incompleteness result show that this plan is bound to fail. Every reasonable mathematical framework
1:51:41
has irresolvable question. And we will call a problem independent of a theory T if we cannot-- T cannot prove neither the statement S nor its negation. And Godel show that s-- the consistency of a theory T is always such an independent statement with respect to T. But of course, what we are interested in is, are there relevant real mathematical questions that fall in this category of being unresolvable by set theory, which means unresolvable by what we call mathematical proof.
1:52:21
Okay, so what do we know about that? So what is the set theory that we look at? So a formal theory that defines, kind of commonly define what mathematical proof is about is the set theory ZFC. Uh, there is a slightly weaker theory which talks about arithmetic, Peano arithmetic, we all know it. And just to mention that Peano arithmetic is equivalent to set theory if we just delete the statement there exist an infinite set. So
1:52:59
and since there's, ZFC can prove the consistency of Peano arithmetic, we can build in ZFC a model for number theory, then we know that it's strictly stronger than PA even with respect to statements about natural numbers because the statement "Peano arithmetic is consistent" is, can be phrased as a statement about natural numbers. So here is a statement about natural numbers that you can prove with ZF-- with ZFC, with the assumption, with the extra axiom, there exists an infinite set.
1:53:31
And you cannot prove this statement in Peano arithmetic although it is a finitary statement about natural numbers. Okay, so that's kind of the background, and Paul Cohen showed that there are really questions that are independent of set theory. The continuum hypothesis and is a kind of a sounding example of this. And since then, there have been many, many independence results in set theory. It started with cardinal arithmetic and infinite combinatorics group theory topology,
1:54:06
functional analysis algebra, and recently we had as Antonina mentioned, we had an independence results of set theory in prov-- very, very basic question machine learning.
1:54:20
So, can-- what can we say about independence results for computational complexity? Do all of this kind of machinery of being able to show the things that are independent of a strong theory, does it apply to complexity, computational complexity statements? So the there is an old result of Hopcroft and Hartmanis that says that for any theory T, we can find a Turing machine such that-- as an-- the oracle complexity with respect to this Turing machine cannot be decided in, in T.
1:55:00
This is kind of a diagonalization trick and talks about the oracle P versus NP with respect to some specially crafted oracle. So that was kind of the first result, and then there were several results of independence of weaker fragments of arithmetic. We also already mentioned here first there were artificial fragments that were kind of meant to be weak enough so that you will not be able to prove much with those weak fragments. Then there was a bounded arithmetic independence like
1:55:39
the famous independent results of Sasha, and all kind of
1:55:46
limiting the proof techniques. So relativize the proofs that was the, the oracle result of Becker, Gil and Solovay and then Razborov and Rudich showed that if you limit the proofs in another way, it's exactly what Sasha was talking about, then there are statements you will not be able to prove. And then later there's the algebroth proofs of Aaronson-Wingazur. But can we prove the independence of P versus NP from set theory? Could this be the case? So there are inherent limitations.
1:56:24
Uh, the, the point is that to realize that since Paul Cohen in 1960, Paul Cohen introduced the technique of forcing and in some sense, we do not have any new techniques for showing independence of set theory.
1:56:39
In a high level, they all follow the same pattern. I will not get into describing this pattern, but important to notice about it that all the proof techniques that we have for showing independence from set theory, they cannot show independence of any statements that involves only natural numbers, only finite sets. So we do not have any technique that has a hope of showing independence of statement like P versus NP because those are finitary statements, there exists a
1:57:11
Turing machine such that, and there exists a case such that for all formulas and so on, everything is finitary.
1:57:19
The tools that we have for showing independence from full set theory can be shown not to be able to show such independence. So we have to go to a, a r-- so that's wh-- I'm trying to explain why it's a finitary statement. It's for every code P, there is a Turing machine N to the K and s-- and so on.
1:57:41
We know that P versus NP can be written as a finitary statement in in, in the language of number theory.
1:57:49
So what can we hope to prove? So I'm saying we cannot-- we don't have any tools that will be able to show independence of P versus NP of full set theory, but what about non-provability from Peano arithmetic? That's kind of the next best thing that we could hope for.
1:58:10
So
1:58:12
this is a weaker theory and a weaker theory it would be easier to show statements that it fails to prove naturally. And it will be a v-- a very interesting result because independence with respect to Peano arithmetic
1:58:29
would be quite satisfactory. It will tell you that without assuming-- without using a statement, there exist infinite sets, we'll not be able to resolve our complexity questions. So showing independence of Peano arithmetic I think will be a, a kind of, could, could be something to hope for as a mathematician because it really tells you that we cannot resolve P versus NP. I mean, the possibility that for having to resolve it, we have to assume the existence of infinite sets or even stronger
1:59:07
infinite cardinals does not, we have no way of incorporating or even imagining how it could be relevant. So this could be an interesting goal. So I can go back to my first slide. What I'm saying is rather than trying to solve P versus NP, maybe what we should do is try to show that it is independent of Peano arithmetic.
1:59:31
If it's independent in Peano arithmetic, in some sense, our efforts to show it to prove it are bound to fail.
1:59:39
Okay, so do we know of any independence from Peano arithmetic of real mathematical statements? So as I mentioned before, we do have results about independence from ZFC and of course there are independents from Peano arithmetic, but these are all about statements which involve infinite sets. So do we have any statements about in-- the independence from Peano arithmetic of real mathematical statements? Of course, the consistency of Peano arithmetic is independent
2:00:12
of Peano arithmetic, but we want to talk about inherently mathematical statements. So the first such result was Paris and Harrington, and that was a, a very, a big breakthrough at the time. They talk, uh-- they took a, a natural version of Ramsey theorem that we can prove in ZFC that this is a true theorem.
2:00:34
It's just the usual Ramsey theorem, but just as sh-- I mean, I'll not repeat it, but just mention to those that are familiar with Ramsey that the only addition here is that the homogeneous set that the existence of this set is guaranteed by Ramsey theorem should be larger than the first natural number in this set, which seems like a small
2:00:59
minor addition to Ramsey's theorem and it really indeed provable that it's true, but they showed you cannot prove it in Peano Arithmetic. So that was kind of giving hope that there are mathematical statements about finite sets that are independent of Peano Arithmetic, although they're provable in, in ZFC. The question we are aiming for is to ask, is it likely to be the case for P versus NP or other computational complexity problems?
2:01:31
So there are similar results later statements about natural numbers. Uh, i-- it's fun to read these things, the Hercules and the Hydra. I don't know if you heard about this. It's kind of a puzzle that you have a tree and you, you have leaves from the tree which are heads of the Hydra and you are Hercules and you ha-- have a sword and you are cutting heads, but each time you're cutting heads, it grows more heads and it grows more heads in a scary way, the f-- the formula.
2:02:03
And still one can prove that no matter how bad is the Hercules, as Hercules you are, you will eventually kill the Hydra. But this eventually is very long and to prove such a system-- so to prove such a statement we can do it in ZFC, but we cannot do it in Peano arithmetic. And again, it's a finitary statement. You're playing a game against a finite tree, which is the Hydra. The interesting relevance to us is that the structure of P not equal NP is syntactically it looks the same as the
2:02:42
Paris-Harrington because the Paris-Harrington is a Ramsey theorem. It says for every arity and size and number of colors, there exist a homogeneous set of such size. And here the P not equal NP have a very natural-- a very similar syntactic structure. It says for every X, there exists a Y such that phi X, Y, which is just, like the Ramsey, for every parameters you have and, and size, you have a homogeneous set. And the statement, this set is homogeneous and
2:03:18
of this size does not contain any unbounded quantifiers. And it's the same with P versus NP, just you want to show that for every program and every bound or the polynomial of the runtime of the program, there exists instance of such, such that this program will give you the wrong answer. So the statement syntactically looks like the Paris-Harrington. So we, we could hope that maybe we could show a similar result independent of Peano arithmetic for P not equal NP.
2:03:55
Okay, so that's what I'm-- I was set to try to understand.
2:03:59
And the conclusion of this work, if we jump right to the end is that,
2:04:12
If on one hand, if SAT can be solved in almost polynomial time, so say P is not equivalent P but SAT can be solved in time which is very, very close to the polynomial and then elaborate on it later. If SAT can be solved in almost polynomial time, then you cannot prove that P is not equivalent P. And now the concrete notion of almost polynomial depends on the theory in which you want to prove it. So for every theory there is a notion of close to
2:04:44
polynomial such that if NP, if SAT can be solved in such close to polynomial time, then that theory will not be able to prove the separation between P and NP because the SAT has a solution that looks almost like polynomial and the theory, the almost will be so fine that the theory will not be able to distinguish between the two. So let's not s-- so not so much of a surprising result but it's something that's worthwhile to bear in mind and I'll get back to it a bit later.
2:05:18
But the surprise here is that we also can show the other direction. So if the theory is sufficiently strong then the reverse statement also holds. Namely the only possible reason for failure of the theory to prove that P is not equivalent P is that SAT can be solved by an algorithm which is almost polynomial time.
2:05:42
So in some sense it says loosely stated that if you can prove that a strong mathematical theory cannot show that P is not equivalent P, you will imply that SAT has a solution which is almost polynomial time.
2:06:01
So solving the logical statement, the higher level logical statement P versus NPs independent of SAT theory will be as hard as coming up with a polynomial, almost polynomial time for SAT. So in some sense that's the main conclusion of this talk that there's no point you don't get much advantage by struggling with logic and trying to show that P versus NP is independent of SAT theory because this will be as hard as showing that you have a polynomial, algorithm almost polynomial algorithm for SAT.
2:06:42
Okay So at this point I said the most important things of the talk and now I want to go a little bit into the technical details and kind of convey the intuition which is not so complex at all of why this is indeed the case.
2:07:00
So
2:07:03
we would consider what do we mean by almost polynomial? I'm talking now about SAT has a solution which is almost polynomial time. So what do we mean by almost polynomial?
2:07:14
So we look at running time which is N to the FN where the exponent FN grows very, very slowly. So it means that the running time has a constant exponent for huge stretches of input lengths.
2:07:33
So the function FN I want it to grow very, very slowly, the exponent of N all the time and if the function grows very, very slowly we can view it as the inverse of a fast growing function. So in some sense it's easier to talk about how fast a function grows rather than talking about how slow it does. So I'll-- we'll talk about the inverse of the function which is the exponent of the runtime.
2:08:06
So wha-- here are some fast growing functions, the Weiner hierarchy. So this is a way of constructing very fast growing functions so if one of N is 2N and now for every ordinal countable ordinal lambda F lambda plus 1 of N is just you apply F of F of F You compose N time F lambda and apply it to N and if you take a limit ordinal then you also have to define it for a limit ordinal. For a limit ordinal you just at the end step you apply-- you take a sequence delta N that converges to delta
2:08:50
to your ordinal and that ends for, to compute F of N you apply the function composed delta of N times. So this is a very-- a way of defining a very fast growing functions, the Ackermann function is just F omega is the first eh, infinite ordinal in the sequence is only the Ackermann function But then as we see here we can keep going. We can applying it further and further and further and get faster and faster growing function. That's the kind of the functions that we will
2:09:27
talk about whose inverses will be the exponents of the runtime if indeed you could prove independence of P versus
2:09:40
NP. So just to demonstrate here I know-- I mean this is a sophisticated audience I don't have to convince you but like F, F2 of 3 is already, a crazy number somehow something hides it for me But yeah anyway anybody can do these calculations. It's crazy fast going even F3 if omega is Ackermann's function and we go beyond it. Okay now how far beyond that we go when we want our functions to grow very very very fast? It's common to denote by epsilon zero, the first ordinal such that omega to the
2:10:21
power alpha equals alpha. We-- The powers here are ordinal powers but, and I will not get into the definition but this is the limit of omega, omega to the power, omega, omega to the power, omega to omega and we take the comfortable limit this.
2:10:40
So this is epsilon zero and we will be interested in the function F epsilon zero. So we take this when we have a key and we push it and push it and push it. We go through function is just here at omega and then we keep going and going and going and going and we get to this stationary point.
2:11:07
Fixed point of this function and we take this crazy growing function. Why do we care about this function? So we care about such a function because I mean the next step is the way I connect fast-growing functions and complexity conjectures. I mean this is fun to talk about fast-growing functions and midlines and so on, but it does relate to computational complexity. So how do we make the connection?
2:11:38
So given a complexity class which has a-- Which you can enumerate as a countable set of algorithms, a sum canonical enumeration of the class. I guess this is what Pavel was calling a x-- a syntactic class, and given the language, I can define a function. And the function, it measures how well can this class approximate the language L.
2:12:13
So this function at the point I, it is the maximum So I go over M1, M2, M3 and so on up to MI And I see which of them can compute L correctly on longer initial segments.
2:12:33
So again, I go over all functions and here is my class, M1 and 2 and so on. I'm going o-- at point I, I'm going over all the I, first I machines or first I programs and then for each of them, I look at the minimum point where it fails to compute my language L And I take the maximum. So this tells me how many machines do I have to consider in order to correctly. Compute the language L on the first
2:13:10
I. So how far can any of the first machines compute my language. This is what we are doing here. So we define a function that measures how well can a class of functions approximate a given language?
2:13:32
And it is easy to realize that this function is total if and only if L is not in the class because if L is in the class, there will be some I such that there will never be a failure. This machine, MI, will compute the class form correctly and we are just looking at the first time that all the first I machines fail. So this is a total function for every I, there is a number R of I if and only if the function is not in the class. And furthermore, the faster this
2:14:11
function grows, the closer is L to the class because it means that fewer machines, right? F of I tells me how far could any of the first I machines compute L correctly So if it grows fast, it means that I need few machines to compute big stretches, L on big stretches of Xs.
2:14:35
So
2:14:39
the faster this function grows, the closer is the class--the function, the language L to the class C. So here we kind of measure how far-- it's not just P naught equal NP, but I'm trying to measure how far is SAT from the class of polynomial time functions. So it gives quantitative measure and this is the function that will apply our knowledge about our discussion of fast-growing functions, so we enumerate all P time machines and we assume that we have some kind of a easy mapping,
2:15:18
computable mapping from index I to the code of the IS machine and we can, without loss of generality, assume that the IS machine is bounded by N to the log I. I mean they're all, we're just enumerating for another kind of machines and then we can get this nice connection between this function, R, and the computational complexity of computing SAT.
2:15:45
So if we-- R is this approximation function of SAT by P, then SAT is in deterministic time D to the log G of N for every function G that bounds R minus one. So now let's stop and see what it means. R is how easy I can-- How far I can approximate SAT. R is a function that grows very fast. So R minus one is a very slow growing function and I --So G is just the computable function that up abouts our minus one and it means that if such can be approximated
2:16:32
well by this procedure, by enumerating all polynomial time machines then such is a deterministic time which this is a very close to constant, very slow growing function because
2:16:48
R min-- R is fast growing, R minus one is very slow growing. I take the log of it And so I have this in the exponent. The exponent is almost a constant. So we're using fast growing functions, we're looking at the inverses as a way of measuring how close that is to P.
2:17:05
And the corollary is that the approximation rate of P by SAT gives us a notion of almost polynomial time algorithm for SAT. So if the approximation rate is fast, is a fast growing function then SAT is really almost polynomial. The exponent is almost a constant.
2:17:32
Okay, so at this point we have the ingredients for our reasoning. We have the notion of fast growing function and the relation to SAT and the class P but of course what we want to do is relate it to a provability. So what's the connection between this and provability? Or in particular to the probability of P versus NP. So a function is called pro-- provably recursive, I guess you all know it, if you can prove in your theory that it holds th-- I have an algorithm that computes this function and
2:18:08
holds on every input and provably recursive functions with respect to PA and PA1, I haven't yet defined PA1, I'll define it in a second, it's the Pi 1 closure of, of PA, it's the same so we can talk about being provably recursive without making this distinction and there is the Wiener theorem. And the Wiener, the Wiener was the, is from this hierarchy and the function is every F alpha for alpha less than Epsilon zero is provably recursive and this is if, in some sense it's if and only if.
2:18:43
If a function is provably recursive then it is dominated by some F alpha. So this, the Wiener hierarchy, what it gives us is a way to determine how fast can a function grow and still be provably recursive.
2:19:03
Still we could prove that for every X there is F of X and the answer is that roughly the bound is this F epsilon zero in the Wiener hierarchy.
2:19:16
So the corollary is that if a function grows very fast, it's not dominated by any of those functions then Peano arithmetic and its closure by Pi 1 functions, by, by pi 1 statements cannot prove that the function is total. I guess I don't have time to explain the result, it's a classical result, it's a beautiful result but if a function grows too fast you cannot prove that this function is total. Eh, and the Paris-Harrington actually the proof that Peano arithmetic cannot resolve this
2:19:57
Ramsey type theorem is that, is exactly by showing that the Ramsey number that you take parameters and you want to ask how fast should your graph be in order to get such homogeneous set is such a fast growing function that it's beyond the scope of what Peano arithmetic can prove it is complete and if Peano arithmetic cannot prove that it's complete, it cannot prove that for every input parameters there is indeed a large enough graph that will give you homogeneous set for these parameters.
2:20:30
So this is exactly the, the tool, the machinery behind the Paris-Harrington independence result and
2:20:41
most of the proofs of independent from Peano arithmetics of statements that we can prove in ZFC, in set theory have this kind of nature. They generate a very fast growing function and show that this fast growing function is beyond the limit that is stated by Wiener's theorem.
2:21:01
Eh, so this repeats in other independence proof respect to Peano arithmetic. So what we can conclude here that if the approximation rate of SAT by P is very fast growing function, then Peano arithmetic cannot prove that P is not equal in P
2:21:19
And so if SAT can be solved by an almost polynomial time algorithm then Peano arithmetic will not be able to prove that they are different. Okay, so that's one direction of our theorem the, maybe the more interesting direction is the other direction so, the inverses of fast growing functions are functions that are very, very, almost constant with their own big stretches. They're constant, I'm trying to rush because I see the clock and we're getting too
2:21:57
close to two o'clock here and the end of the recording.
2:22:02
So what I'm saying is that if a function grows very fast, eh, if the, this function R, the approximation grows very fast then there are long stretches on which SAT can be solved in a fixed polynomial.
2:22:20
So the next step is showing that this is the only reason for non-probability of P versus NP.
2:22:26
And I show it with respect to the theory PA1. Pa1 is a add to Peano arithmetic all the pi 1 true statements. Now PA1 so it's Peano arithmetic plus all the pi 1 formulas that are true in standard models of arithmetic. And what do we know about this property of P1? It's not a recursive theory. That's a big negative but there is some notion of some sense of representative representation independence. Uh, I mean it, it has the-- it exactly the theory that
2:23:05
we need in order to be able to show that if you have two Turing machine to prove that two Turing machines that compute the same function are indeed computing the same function. So in order to show representation independence of Turing machines we need the theory PA1, and so it's in some sense it's a natural theory to consider when we want to talk about independence of runtime on, on Turing machines.
2:23:37
And we can also nice properties if P equals NP, then PA1 can prove it because you can have this polynomial time algorithm and PA1 can prove the statement for every input it computes SAT correctly.
2:23:55
Okay, so we switch to the theory PA1 which is much stronger, and now we have the theorem that PA1 proves P equals-- are not equal NP if and only if
2:24:12
the approximation rate of P is low. Or in other way-- in other words, so, I mean before I talk about the proof idea, what we care about here is to show that PA1 will be able to sh-- if SAT is far from P, PA1 will be able to show it. And the only reason that it cannot show it could be that SAT is very, very close to P.
2:24:41
And the proof idea, I guess we don't have much time for proofs now, but we can write this as a Pi 1 statement.
2:24:51
So, the conclusion is that if PA1 fails to prove P not equal NP then SAT has almost polynomial time algorithms.
2:25:02
And more on the significance, so I want to show that if PA1 cannot prove that there are different-- I mean then in some s-- in some sense we cannot distinguish an independence proof between PA1 and PA because the generic way in which we show that a theory does not prove some statement, the, the, the Poincare forcing style is to start with a model. We assume that the theory is consistent, so we have a model M. We construct a submodel in which you get the opposite
2:25:39
of the statement and such a submodel will also satisfy the PI 1 theory of the first model. So what I'm saying, any tool that we have with the hope of showing that something is independent of Peano Arithmetic will also show us independence of PA1,
2:25:58
and therefore if it could show independence of SAT, of P versus NP, it will mean that SAT is very close to P.
2:26:07
So this is the bottom line. So if it is provable that P versus NP is independent of PA then SAT can be solved in a deterministic time T to the g of n where g is a very, very slow growing function of g minus 1, is a very fast growing function which will mean that SAT is almost in P and that's if and only If statement. I think I have just, we have similar results for system complexity. We can show that, for example, I-- if Peano arithmetic cannot show is, if P versus NP is independent of Peano
2:26:49
arithmetic then there are no one-way functions and all kind of results in this nature But I, I'm out of time So I will stop here and take some questions if we can still take questions.
2:27:02
[ANTONINA KOLOKOLOVA] Thank you so much.
2:27:05
Yeah please ask questions and sorry for running overtime but please do ask questions.
2:27:21
If nobody ask, may I ask a really naive question? I-- I have a [JAN JOHANNSEN] Question. [ANTONINA KOLOKOLOVA] Oh, you have a question? Okay. Go ahead. [JAN JOHANNSEN] Okay. Does this the proof technique also allow you to go further down in the strength of the theory, for instance, to replace Peano arithmetic by I Sigma 1 and M F Epsilon naught by Ackermann?
2:27:46
[SHAI BEN DAVID] That's an interesting direc-- It seems that-- I mean, it's an interesting direction. I haven't thought about it. I haven't thought about weaker theories. I mean, as Sasha was saying right at the start, I come from working on ZFC But yeah, I think it's a very interesting uh, question. It's not inconsiderable. Yeah.
2:28:05
[JAN JOHANNSEN] Okay.
2:28:12
[ANTONINA KOLOKOLOVA] More questions? [JAN JOHANNSEN] Well-- [ANTONINA KOLOKOLOVA] Can I-- If I-- Oh yeah. Please please Pavel. Yeah. [PAVEL PUDLAK] Yeah. So, I understand the message is that the problem is that we are not able to distinguish between PA and PA1. We are not, not really able to understand what what are the, the basic
2:28:40
uh, things in Peano arithmetic. We, we know what, what is the induction but if Peano arithmetic was formalized with some stronger basic theory then eh, everything that we are able to prove about Peano arithmetic will-- would be the same. Uh, and, and this is wha-- What what I also, I completely agree with you, but I, I would like to add that the, the similar thing is in in complexity theory that we are not able to distinguish computations that have different basic
2:29:15
operations like uh, say, if we allow Turing machine an access to Oracle and say, "Well, what the Oracle computes is the elementary operation." So, then various things can happen and this is the relativizations.
2:29:36
I think it's an interesting [SHAI BEN DAVID] Analogy. [PAVEL PUDLAK] Sorry? [SHAI BEN DAVID] I think it's a very interesting analogy, right. [PAVEL PUDLAK] Yes, yeah. Okay. Thanks.
2:29:46
[ANTONINA KOLOKOLOVA] Actually, a question to both of you because I kept thinking about the relation between your talk, Shai, and Pavel's talk. Uh, Pavel talked about semantic classes and the question of complete problems and you heavily use the fact that P is a syntactic class. [SHAI BEN DAVID] Right. [ANTONINA KOLOKOLOVA] Is that right? So is there any kind of connection between those? [SHAI BEN DAVID] Yeah, I really don't know. Maybe I use very heavily, I mean,
2:30:14
all of this line of all of this machinery is about syntactic classes, right.
2:30:23
[ANTONINA KOLOKOLOVA] And Thomas is asking you to show the second last slide again. [SHAI BEN DAVID] Okay.
2:30:29
This one or the before that?
2:30:35
[ANTONINA KOLOKOLOVA] You can unmute him, sir. [THOMAS F KOCHMANN] Before that.
2:30:40
[SHAI BEN DAVID] Yes. [THOMAS F KOCHMANN] Thanks.
2:30:42
[SHAI BEN DAVID] Right. Yeah. This is about why, why we cannot distinguish PA1 from PA that Pavel was talking about. Yeah.
2:30:53
So do you want me to repeat it or you want to ask something about it?
2:30:59
[THOMAS F KOCHMANN] No, thank you. [SHAI BEN DAVID] Oh, okay. Yeah. [ALEXANDER RAZBOROV] So, Shai, I have I have very naive question. So assume that I am telling you that NP is not a subset of quasi-polynomial time in the real world.
2:31:20
Right? Uh-huh.
2:31:24
It means, or maybe I miss something, you are saying that it implies that P is not equal to NP, is like a weaker statement, is probable in P arithmatic. [SHAI BEN DAVID] Right. [ALEXANDER RAZBOROV] Is it-- [SHAI BEN DAVID] Yeah. [ALEXANDER RAZBOROV] Is it what you are saying? [SHAI BEN DAVID] Yeah. Yeah. Okay. This is a rough way of [ALEXANDER RAZBOROV] Putting it, right. Sounds very strong to me. Yep.
2:31:50
No, it's not probable in P arithmetic. It's probable in PA-1. [SHAI BEN DAVID] Yeah, that's-- The-- Oh, PA-- It's probably-- [ALEXANDER RAZBOROV] I'm sorry. I'm sorry. Move it so one slide farther or where you have result here, which is, it says PA. [SHAI BEN DAVID] Yeah, But here I have the caveat by any method known today. So what Pavel, Pavel was saying correctly, I mean-- Ah.
2:32:15
--it provably we can show it will be provable in PA-1
2:32:21
But there is no mathematical tool that will distinguish PA-1 from PA. So now we have to take a second step on top of it and saying-- [ALEXANDER RAZBOROV] Ah. By [SHAI BEN DAVID] Existing tools. [ALEXANDER RAZBOROV] Okay, good. Mm-hmm. Okay, thank you.
2:32:40
[ANTONINA KOLOKOLOVA] Mm. More question, comments to any speakers?
2:32:45
To and from any speakers.
2:32:58
Okay. Thank you very, very much, everybody. This was such a fantastic session. Sorry for running overtime, but I don't want it to end. This is fantastic.
2:33:09
So if people are interested they could go to, if you're an attendee, I posted a link to Gather.Town In the chat. This is a workshop, Gather.Town.
2:33:20
And if you want to could, anybody who wants is welcome to come there and we could chat and Yeah. So thank you so much uh, Sasha, Pavel, and Troy. All three of your talks are so inspiring and really make you think about the basic questions. So thank you very, very much.
2:33:47
[SHAI BEN DAVID] Thank you.
Here to help you learn
Sign in to keep a private conversation with your course tutor.
Ask me anything about the material…
Sign in to chat