Foundations of Mathematics: Inconsistency & Incompleteness | Voevodsky

[00:00:23]hello so I am Pingus in the school of ma and my task is to introduce use Vladimir voty so as a relative large number of mathematician in this country he was educated in the former Soviet Union he was student of Moscow State University from 83 to 89 then came to this country got his PD at AR in 92 was at Northwestern University from 96 to 99 and then he had some nce collaboration with susin and then he came to the Institute first as a member in 98 and became Professor here in 2002 so he has been able to successfully introduce methods of homot homotopy theory in algebraic geometry and for me this is somewhat like mixing water and fire object of algebraic geometry are very rid with very few maps from one to another where object of hotor are very flexible and it looks H hopelessly naive to try to mix the two together but that's what he has been able to do for me a first example was this extraordinary paper with susin where where it's clear that you cannot imitate the definition of hology using simplees in algebraic geometry just by using algebraic map from simplees to algebraic varieties but what this paper for is that if you allow fin nightly many valued map instead of plain Maps then you can perfectly imitate the definition of simplical using this kind of algebraic simplies at least for to and coent integral coefficient it's Hess anyway uh then you has also be you able to use IDE of aotop theory to obtain a good triangulated category of motive hopefully good and has been able to use such tool to prove extraordinary result about galak m v so corology for G group of field uh first he proved this is related to not two cor The Milner Conor about its structure relation with Milner G groups and for this he got the fields medal in 2002 and then more recently with some geometric input from Roost he obtained similar result for all primes so about gal holog of field and now his interest are in another direction another improbable mixture ear homotopy Theory formal language automatic verification of proves things which seems to have not much in common is startled today what if current Foundation of mathematics are inconsistent and I am very curious to hear what he has to say [Applause] um hello and uh thank you everybody for uh coming to my talk I'm quite nervous because of the uh because the subject is such a um controversial thing so I'll um I'll try to do my best and I'll try to explain what I mean by current foundations and what I mean by their possible inconsistency so but I'll start with with a few um historical um actually comments so we are celebrating um these days the 80th anniversary of the um Institute for Advent studies but we could actually be also celebrating uh the 80th anniversary of something else which is probably even more MOS uh than the foundation of the institute for advanced studies and as it happens it's almost exactly 80 years ago that GLE um understood GLE came up with a proof of his second incompleteness theory um what we know we don't know of course the exact date when it sort of uh crystallized in his mind but what we do know is that when he was Pres presenting his uh the proof of his first incompleteness theorum uh on September 6 1930 he didn't know about the second incompleteness theorum and when he uh submitted an abstract of his final paper in October 23 1930 he already knew about the second incompleteness theorum so it happened somewhere between September 6 and October 23 so it's like we're almost right in the middle of that uh period 80 years ago so um let me formulate the uh his second incompleteness theorum in the following form which might be might look a little bit uh uh too strong for some who uh who know the uh the original formulation but um I'm going to argue that uh that's uh how it really should be understood so the theorem says in my understanding is that uh it can be proved that it's impossible to prove uh consistency of uh the first order arithmetics Elementary number Theory or of any other Theory which is um at least as strong now um uh for Norman uh commented on uh for Norman somehow understood that Good's first in completeness theorem which spoke about U just unprovable statements in in um arithmetic uh implied the second and uh he wrote to to gel the following uh interesting words that uh thus I think that your result has solved negatively the foundational question there is no rigorous just certification for classical mathematics and that's for nman to on November 29 1930 again 80 years ago pretty much so um so let's see how things kind of developed after that um um I'm so G himself I I I'll I'll come to it in in in the next slide but okay let me first say that so we have like something which I'm I'm choosing to call G's Paradox uh so the on the one hand we know and I probably should have put quotes around this know that the first order arithmetics is consistent that's that's the common commonly accepted fact among mathematicians and um as a consequence among everybody else on the other hand it can be proved that it's impossible to prove that it is consistent so we have this two statements and uh I should tell you if one really thinks deeply about it this is extremely unsettling for any rational mind it's um and what one comes to is that so what are the choices in in resolving this Paradox and there are three choices um well aside from well there are three choices so the the first choice is that if we know that it's consistent then somehow we should be able to come up with a proof and then the go theorum the second incompleteness theorum as it been stated um before is incorrect uh that is uh the that is a choice which was essentially made by 90% of uh people who were seriously are working on the subject so it was the choice I think made by good himself and it was a choice made by many others so there was many many attempts uh to to still kind of prove that the first order arithmetics is consistent despite the godal theorum and somehow circumvent this theorum in one way or another and I will speak about um such attempts in a few minutes so there is a second possibility which is uh which we can admit that there is some kind of transcendental knowledge uh which humans can obtain uh which is correct but not not just which not just cannot be rationally kind of supported but can be it can be proved that it cannot be rationally supported and um that uh Choice have been also made by many and been a source of of a really large body of dubious philosophical uh texts I would say and um well dubious is of course my own personal opinion um and so um the third possibility which is the least uh least considered one so to speak is is that uh we can admit the fact that our conviction that we know that it is consistent is actually an illusion in this case and that the actual formal system of the first order arithmetic is inconsistent and that's what the proof means and um I want to um discuss this third possibility today because I think that uh it is time to consider this third possibility very very seriously and to um and that's basically the only the only choice which is left because the um so many efforts were made to try to uh justify the first choice and they were all ins successful uh the second choice seems to be like I personally don't want to talk about it much and uh so we are only left with the third and so so let's let's consider it as a serious possibility and see what consequences it might have so so first let's uh let's see what kind of arguments uh do we have in the support of of this knowing uh of the consistency and in the process I'll U outline what consistency actually means and it inconsistency of of first or arithmetic doesn't mean that 2 + 2 doesn't equal four please don't worry it it's something much much more uh kind of it really has nothing to do with with the uh validity of the usual computational uh mathematics which is being used all around us and and if arithmetics is this first order arithmetic is inconsistent it doesn't mean that planes still start falling uh from from the from the air or Bridges start falling down no it's uh mathematics constructive well the actual computational mathematics uh is supported by much more than our belief in consistency of formal Theory so um so anyway so the the two uh mathematical arguments in the support of the consistency of the first order arithmetic as a formal Theory standard to um are as follows so the first one I I'm calling it formulas as subset interpretation of U first order arithmetic and I'll explain what it is and the second one is a proof given by um German logistician gansen at the end of uh 1930s uh and this argument uh uses induction on the lens on the structure of the proofs in arithmetic to show that one cannot uh obtain a proof of absurdity and I will um show what what both of those mean so first of all what is the first order arithmetic and what does it mean by it's in or consistency so the first order arith is it's not a collection of rules for operating with uh with numbers no it it's something entirely different it's a u it's a mathematical object uh which belongs to a class of mathematical objects which are called formal theories in first order logic and uh a formal Theory uh is specified by collection of data of the following form so it's uh specified by uh two alphabets one for special symbols and one for names of variables um it's spe there are certain rules which one probably which which I'm calling syntactic rules which determine what sequence of uh of letters from from both alphabets um which which actually specify for for a given collection of names of uh variables it specifies which sequences of letters from both alphabets are grammatically correct formulas in these variables and these syntactic rules are such that it's easy to verify so if one given sequence of U symbols from both alphabets then doing some simple verification algorithm one can U determine whether it's a u grammatically correct formula or not then there are deduction rules so there is a notion of a closed formula closed formula is a formula with no free variables so the number of free variables is zero so there are deduction rules which are certain operations on closed formulas so it's it's certain ways to to combine some closed formulas to obtain a new closed formula um there kind of combinatorial rules um and um I'll come to it in a moment again so the first component of a of a formal theory is a collection of kind of initial closed formulas which are called axom so we have this kind of a um combinatorial game Lego I don't know where we have some initial pieces and we have rules by means of which we can form new pieces out of these initial ones and um anything which can can be formed from these initial axioms by by means of this uh deduction rules is called a seror uh in principle this is an extremely general definition and one can have formal in this in formal theories in that sense which have no meaning other than just some combinatorial uh rearrangement of symbols but uh typically they're being um used to uh to formalize some some uh fragments of of natural reasoning and it's done as follows um so a series of first order logic form a subclass of among all formal theories and among their special symbol sybols there are this six uh standard symbols of first order logic which uh um every mathematician I don't know if if they're learned at school in any uh in any way but definitely learned by any mathematicians so there the first few are called quantifiers it's for all and exist uh yeah so excuse me for all and exist and I should say something about it so so this these are symbols this inverted a inverted e and this little V and this uh little inverted V and this this this six six things are symbols of um of the special symbol alphabet now what's written on the right from them in in quotes these are translations of these symbols into natural language so this is not a part of formal Theory at all it's uh it's it's something uh external to the formal Theory it's some rules which allow one to translate formulas of the formal Theory into sentences of natural language um and uh so so here the um the rules are such that this uh inverted a is translated as for all inverted e is translated as there exist and then there is or and implies and not there are also parenthesis and um and I think usually period which I used as punctuation marks in in the formulas um so A first order theory is called inconsistent um if uh if there is a closed formula such that closed formula a such that a is a theorum and also not a is a theorum so um the formal system of arithmetic contains among it special symbols also symbols for 0 1 well there actually several different versions but like one of the standard ones it would contain additional symbols for zero one uh addition multiplication equality and let's say the uh the greater um sign um so again these are special symbols and when I'm saying that it's equality it means that that's how I translate the appearance of this special symbol in the formula into um natural language so that's an example of a closed formula and U that's its uh actual form it's just a sequence of symbols from this alphabets um and what is below is its translation into natural language it translates into for all n there exist M such that and then there is some um arithmetical expression oh uh ah interesting actually so that I've corrected it yeah thank you there should be a yeah as as stated here this uh this sequence of symbols represents a syntactically incorrect expression so for it to be syntactically correct closed formula one has to put an n between the star and the plus and that's my um typo um so so closed formulas can be translated into English as statements about natural numbers uh formulas which are not closed so which contain free variables as as it's called can be translated in into English as descriptions of subsets uh in the set of natural numbers or more generally in the set of sequences of natural numbers so for example if I remove the very uh beginning of the of the uh first Formula so instead of writing for all n I'll just remove this for all n just considers this so this says there exist m 3 n² + 5 m² + 7al 17 MN so one translate one interprets it as a description of this subset of natural numbers which consist of natural numbers n such that there exist M such that this equation is satisfied if I had more than one free variable I would have a description of a subset in uh the set of pairs of natural numbers now the deduction rule says as I said are just formal uh combinatorial rules to operate with the sequences of symbol they're kind of you have one sequence of symbols which satisfies some condition you have another sequence of symbols which satisfies some condition then you can kind of permute them in a certain way and do certain things with them and you get another sequence of symbols which is said to be uh deduced from the two previous ones and uh those combinatorial rules are um are chosen in such a way as to reflect the usual natural deduction rules for uh for statements in this case about subsets um of sequences of natural numbers so for example if there is a statement that uh for all n uh something holds U and then there is um uh and then there is a statement that there exist and that something else holds then from this I can deduce that there exist n such that both the first something and the second something holds I can do it using one of the U formal deduction rules so now what uh so going back to the definition of a formal system one one starts with the axioms which is collection of statements which are kind of verifiably correct so which when you translate them into English they they map into into something which which uh which is true about natural numbers uh and then there are deduction rules and using this deduction rules you get many many more statements which are also supposed to be true because in each step you use the logical uh operation which should make a true statement out of other true statements now that would make perfect sense if if each uh um formula actually had kind of a serial meaning in a sense what happens in arithmetic is is not that um there is a serious problem with the uh with this interpretation U so this interpretation of of formulas as subsets was of course the original uh source for the certainty that arithmetic is consistent and in fact it was I I suspect the source of the original formulation of of formal arithmetic as it was so um the problem here is that these subsets which correspond to General formulas are really not um are really totally surreal they uh it can be proved uh that that there are formulas like let's say with one free variable so a formula with one free variable will describe a subset of natural numbers but one can prove that there are formulas with one free variable which describe a subset for which it's algorithmically impossible to show for not for a single number whether it belongs to this subset or not or doesn't belong to this subset so it's it's a subset about which you can prove that it's impossible to say anything about this subset whatsoever uh so using this this kind of objects as intermediate steps in in logical um in Chains of logical conclusions uh I find it inconvincible um explain it in in much detail here um what he does is he considers this as a formal system and no interpretations are assumed uh and he considers the structure of the deduction sequences so to speak and each deduction sequence can be assigned kind of a something like like a collection of trees finite trees trees I mean in mathematical sense so kind of combinatorial object object so one can assign a combinatorial object which measures the complexity of the deduction process and then one can uh then one can present an argument which uses induction on this uh so so this this combinatorial objects are called are called ordinals less than epsilon0 and one can uh give a definition what is what does it mean for two ordinals to be less one less than another and that's all quite quite constructive and um and then he shows gon's proof is that um if there is a proof of contradiction if there is a inconsistency in uh formal arithmetic then there would exist a sequence of this um ordinals which is decreasing at each step but never terminates so infinite decreasing sequence of this ordinals and then he uh and then there is a certain uh argument I would put it quote unquote which uh then he says that that's unlikely I mean ra rather it's something like he says that it's self self-evident that that cannot happen um so this self-evidence is extremely uh suspicious because uh in a complete agreement with goodle theorem one can show that it's impossible to prove using the usual induction and usual enumeration techniques that any such decreasing sequence uh terminates so it's impossible to prove using the usual U reasoning means that it terminates uh the only reason to um to say that it terminates is to declare that it's self-evident so that again is not uh very convincing so um so basically what it means is that if we find inconsistency in um in the first order arithmetic it will mean that there will be this non-terminating sequence of of ordinals less than epsilon0 so what that that's that's an interesting conclusion but it's U it's not earth shattering in any way um so um so here we come to the uh second part of um of our investigation in terms of what uh what such an inconsistency would imply so so the first part was kind of so there are this arguments in support of consistency let's consider let's look at them carefully and see so assuming consistency let's look at this argument and don't get some sort of a really uh obvious contradiction and I'm I'm arguing that no we don't get any obvious contradiction we we get that certain things which look self-evident to which looked self-evident to some people will turn out to be false but these things have absolutely no uh material meaning I mean this this these are things which can be neither verified nor falsified by any sort of an experiment so so the things are purely surrealistic and so can be either false or true with with no problem uh but let's see what it will mean for mathematics because that's um that's of course something which on the mind of anyone any mathematician who starts to consider such a possibility so first of all inconsistency in the first order arithmetic will mean uh inconsistency of almost every other found foundational theory in mathematics standard foundational theory in mathematics so it would mean inconsistency of set theory in particular or of all all kinds of flavors of set theory uh what is a little less known but uh also true is that inconsistency of classical first order arithmetic implies inconsistency of so-called constructive or intuitionistic um arithmetic and that has been shown by by Godel himself in 1930 three and that's a purely formal um proof which takes proof of contradiction in In classical Theory so so the difference for for non for non mathematician non logician the difference here between classical and and intuitionistic is that intuitionistic doesn't allow for um it doesn't include the rule that double negation of a proposition equals the proposition so class in classical case one one has the rules that the double ation of a statement is equivalent to the statement itself in intuitionistic this rule is excluded um however one can show that as far as the issue of consistency is concerned it it doesn't change is thing so if if the first if we find inconsistency in the first arithmetic then then all of those theories are um then we'll be able to construct inconsistencies in all of these theories as well so um so so what what what should we do about it because I'm I'm quite seriously uh suspecting that such an inconsistency can uh at some point be found as as I said because of the three uh only three choices there and um one of them must be true and the first two are unlikely to be true so um well actually as far as um as far as the transcendental knowledge is concerned I I want to to point out that um while I may uh admit a possibility of such knowledge concerning things natural in a sense uh the such a thing as the first or formal first order arithmetic is totally a creation of of human minds and there's absolutely no reason for transcendental forces to kind of Ensure it's it's consistency by transcendental means um so the G argument um in fact is General enough to basically show that uh so if the first or arithmetic is inconsistent it makes little sense to try to find foundations which are consistent uh any foundations which are rich enough to um to be used to be useful for the formalization of kind of mathematical abstract mathematical thinking which we are so fond of any such foundations will uh necessarily be inconsistent if the first order arithmetic is inconsistent so uh so the only uh possibility here and is to is that we mathematicians will will have to learn how to construct reliable proofs uh using inconsistent formal systems and uh and I think it is possible it's it's entirely not uh it's not easy and it's uh but uh I think it is possible and um it is emerging such a such a possibility is emerging for the kind of Foundations which are now being developed which are based on ideas which are coming from theoretical computer science mostly um at this time so uh one possible candidates for such so so we need New Foundations which uh which will be formulated in in a formal system which allows one to which can be used despite it inconsistency or possible inconsistency can be used to construct reliable proofs so the classical first order logic is not good at it because if if it has an inconsistency then one can prove everything and uh it's it it stops being informative uh however the there are other types of U formal uh formal systems which can be used for uh formalization of mathematics which uh react to inconsistency in a much less drastic way in a sense so uh inconsistency in such systems doesn't mean that system totally um um becomes totally informative and uh one of the examples of such classes of systems is the class of um so-called constructive type Series so that is a class of uh formal systems which have been used extensively for the in the theory of programming languages and uh it's it's rather standard um it's becoming rather standard uh thing which theoretical computer scientists May learn about and what is important for us is that um well they have many nice many interesting features which um I don't have time to speak about but what's important is that a proof in such a system a proof of a formula in such a system is itself a formula in this system so a proof is not something external to to the statement but to the language it's like it's not like there are no deduction rules per se there are only syntactic rules and um proving a statement means uh constructing a syntactically correct statement of a certain form which includes the original one so kind of extending in a certain way so uh so a proof becomes an object which can be studied inside the system itself and so if one has an inconsistency for example so one has a proof of of a and a proof of non a then one can um then one can show in in many systems of course not in any uh in many systems that any such proof uh can be well it sort of can be detected I mean the proofs which are which lead to inconsistences have um have certain negative properties which can be determined by an algorithm so um so what might be possible and here I'm that that's becomes a bit of a fantasy because uh it's it's very um much kind of recent activity so to speak so um what might be possible is the following type of workflow uh which in constructive types here in particular particular as possible so we take a mathematical problem we formalize it we formalize it in a language which allows all kinds of obstructions and which which is probably even more powerful than uh that our set theory which we're using today and allow us for more abstract um steps to be performed and more abstract um ideas to be used so using this formal system we create a solution of the original problem and that's that's a creative part which will always remain creative there is no uh no danger about that uh then this proof is submitted to uh to a verification algorithm which uh well we're already assuming that the proof is kind of syntactically correct so it's logically correct but then there is a verification that it's reliable in a sense and this verification will not be um as examples show such a verification algorithm we will not know whether it terminates or not in general so uh if it terminates then then the proof is reliable if it doesn't terminate then we know nothing and um it means that we probably have to look for another proof for which algorithm will terminate faster but but also there is the idea that most proofs which one constructs in such a way are reliable so so it doesn't happen often that it it doesn't terminate um so that that's kind of a more technical comment that there about how to ensure reliability of a given proof term and that there are probably different ways I mean I'm sure there are different ways like the simplest one which comes to mind is that solution is reliable so there is the proof term apply normalization procedure to it and if after normalization it um lands in the subsystem for which consistency can be proved so kind of all the all our abstrct thinking kind of cancels out in the Pro process of of normalizing the proof then we can rely on it if it doesn't then then uh it's not so clear so um and um so I want to summarize because the schedule for this talk was uh I was told to to have a shorter talk and longer session for questions and aners because uh and uh the um here is as follows so first of all I suggest that the correct interpretation of second incompleteness theorem is to consider it as a step uh towards future proof of inconsistency in the mathematical uh in the formal systems which um which this theorem refers to and that is of course purely a conjecture uh you can say that it's making this as a the conjecture and uh it would be wonderful if we could find the actual inconsistency uh because then we would kind of know where um that that would provide us with with a huge amount of of new knowledge and understanding uh but I don't know I don't know when that may happen but even just having in mind that this is a really interesting uh problem to consider I think is very important so such an interpretation definitely cancels out a lot of dubious philosophical um noise around G serum which I think would be very good uh and um as far as mathematics is concerned and uh so if if there is indeed an inconsistency in in the first or arithmetic uh it would mean inconsistency in basically any U sufficiently reach foundational system so in mathematics we will uh that now that's that's my idea that's the only thing which which uh the only kind of solution which comes to my mind is that we may have to learn to um to use inconsistent systems to obtain reliable proofs and ultimately if we do learn to do such a thing it will be very uh liberating because then one can use uh reasoning systems which are known to be inconsistent but which are are closer to our intuitive thinking uh to construct proofs which can then be verified formally to be reliable so ultimately it can lead to u to more freedom in um in the mathematical uh workflow so to speak there are also uh some important uh speculations one can do concerning the changes in mathematics which it may lead to and how it relates to the uh to the existing troubles between mathematics and physics and stuff like this but uh that would be um more that would rather be a subject of a separate talk so the for this talk what my my main intention was to uh to attract everybody's attention kind of seriously to the possibility of such an inconsistency and to to argue that such an inconsistency would not mean the end of the world but uh but rather a liberation of a lot of um of our thinking in mathematics and and it may have a lot of constructive and positive consequences um thank you very much [Applause] so we have time for questions your alteres at the begin and that's all right um that's definitely acceptable uh the uh um but but uh when one hopes for something one also uh allows for the possibility of uh of the opposite so um as long as it's not kind of I know is consistent and nothing else is ever possible uh any other kind of intermediate uh situation is is I think a personal choice in a sense one statement something two theems which cannot from the foundation how does one children the can one circumstance I think2 every even number can be expressed as noter example has ever been found suppose it is the case that no counter example will ever be found and yet it may not be able from the foundation so you have a the which can something yeah well there there are many such things I mean there can be many uh we know it from Good's own work that um there is the first incompleteness Theory which which says that there are multiple statements which in any formal system there will be in any consistent formal system there will be multiple statements which um cannot be proved from from the axioms um that kind of that doesn't bother me in any way at all um after all the question of proving or unproven goldb conjecture is I mean okay I I no that's all right that that doesn't bother me so I'm sorry I yeah so what was your question do you anticipate such inconsistencies also in experimental Sciences where you can do an experiment and verify what's true independent of what my our imagination dictates well there can be no inconsistency in experimental science there can only results of an experiment uh by by definition so so inconsistency is when when uh when when when you think is is not what it what actually happens that's that's in consistency and um so no I I definitely consider the material reality as the uh kind of absolute uh judge of of uh truth and so so there can be no inconsistency in experimental I don't know what is inconsistency in physics I mean what is inconsistency in in in formal arithmetics I have explained very uh concretely I don't know what is an inconsistency in physics I know you said it was essentially for another lecture but could you just give us although you said this would be properly in another lecture which hopefully we'll get the chance to invite you to give I just wonder if you can offer any thoughts about how analysis our concepts of real numbers and so on might be different if the usual foundations are inconsistent so first of all for that we don't need them to be inconsistent we it it is entirely possible that our understanding of real numbers is is not ad is not an adequate formalization of the notion of continuity and that possibility is is quite quite real even without any inconsistency so this inconsistency here is unnecessary for for this um side of the story to develop and uh the notion of real numbers is as many um I think as many different observations kind of show mind observations the notion of real number is seem to be over idealized in a sense so it's it's an over idealized object which and it's clear that this over idealization uh was necessary in order to make reasoning about real numbers simple enough for for uh for it to be U humanly uh practical um and it's quite possible that in in years to come because of this development of the computer assisted um thinking let's put it this way especially about uh mathematical objects um maybe we'll be able to explore other possibilities in which the notion of continuity will be formalized in in a less idealized way and and so will allow for and and which will then avoid some of of the physical paradoxes I mean some of the physical paradoxes so to speak which which one encounters when one tries to use the usual uh notion of continuity to uh to describe the physical reality and together with the notion of locality when one gets into this stupid situation where in order for something at all to happen two real numbers have to to be precisely equal at some point and which of course can never happen and um but but this is this line of development is does not require any any inconsistency it's it's can be and it it will proceed I'm sure uh independently on on that can I summize what you're saying um even if the usual foundations are inconsistent are consistent there might be a better theory of real numbers is that what you're saying there might be a better way to uh even if the usual foundations are consistent there might better foundations first of all uh and uh and uh second even in in in a in a given in given foundations there might be a better way of uh formalizing the concept of continuity than the current one but I I would rather uh go for for New Foundations and new formalization of continuity in New Foundations as as a prediction so so I I just wanted to make the comment or raise again the issue of whether experiments are uh results of experiments are consistent in the sense that it's almost impossible to think about the results of an experiment without putting some kind of interpretation on it even if it's even if it's the interpretation is simply that the experiment is generalizable that's already an interpretation and we have you know um uh experimental truths that have in a sense been falsified at The Institute like velocities ad and so on you know um like what that velocity add that you know turns out not to be true in special relativity but yet for centuries it appeared to be experimentally incontrovertible you know that's just the simple I mean I could think of other examples but um you know we make a measurement there's always some limitations of how we're observing it and we assume it's generalizable we don't really know that we put all kinds of interpretations on it um you you know I would almost it's hard for me to figure out which is more unprovable an experiment or or a mathematical theorem I I mean I don't know if others want to comment but which is more which is more unprovable well experiment is is well there there isn't really a notion of a proof for an experiment there is a notion of proof for mathematical statement if it's formulated in in a a particular formal system um there is not a well- defined notion of it's not clear what it means to prove an experiment um I think you know there is this I mean it is one can one can argue that it is true that like because of the quantum mechanics for example there there is are possibility that we all right now just uh float in the air because even not quantum mechanics just just random movement of our molecules will will suddenly all coincide in Direction and will all move start floating in the air and there is a certain uh probability for for that to happen uh and uh and that because of that the the the gravitation kind of that would falsify the the gravitational laws which which explain why we are actually not floating so that the the argument against such an argument is that there is a I I I I like to to use the the expression gape and scale there's like a huge gap and scale between the probabilities involved in our all of us floating in the air and uh all the probabilities with which we are dealing in in any kind of uh experiment or prediction or anything like that and so this this kind of this Gap in scale and probabilities is so huge that it permits us to to speak of one of those things to as as to be simply impossible so so that's that's about proving an experiment I mean you're right I mean there there all kinds of things which may happen with very very low probability which you might have made an experiment and like measured something and that something been constant for a year and then or or 10 years or 20 years and then you can say okay there is still a little probability that in 5 seconds after that it will totally change yes there is but um um it's um it's it's uh it's not practical to um to take such a probability into account uh it would uh so um uh yeah I think your you should be moderating so one of the in physics so so physics is somewhat temporary knowledge but would could this happen in MA mathematics could you get to a certain state where you sort of believe some things some mathematical truth but you entertain the possibility that they will uh later be disproved and something replace it mathematics tend to be absolute but maybe mathematics is yeah it's it's um it has been um historically kind of static I would I would say instead of absolute so if if something has been proved it been proved forever uh and one can speculate about a possibility of kind of dynamic mathematics in that sense but it's it's I think there's again a gap in scale between this and even the inconsistency issue I mean this the more the more complicated mathematical theories could be that have that you could have it's very hard to imagine at this point and uh it's harder to imagine that inconsistency of virus AC no no but this is simply a for this is simply a wrong proof and that's that's what the computers are are here for so um so I'm afraid it's time to conclude so I would like to thanosi for [Applause] his thank you than