## Link https://www.youtube.com/watch?v=O45LaFsaqMA ## Clips ### Voevodsky begins start = 4:07 end = 4:30 ### It's the 80th anniversary of Gödel's second incompleteness theorem. First record we have of the first incompleteness theorem was September 6th 1930 start = 4:40 end = 6:10 ### This is extremely unsettling for any rational mind start = 8:42 end = 9:42 ### Voevodsky: "What we need are foundations which can be used to construct reliable proofs despite being inconsistent." start = 33:00 end = 36:00 ### We mathematicians will have to learn how to construct reliable proofs using inconsistent formal systems start = 34:00 end = 36:00 ### It's not easy, but I think it is possible. And such a possibility is emerging for the kind of foundations which are now being developed based on ideas coming from theoretical computer science mostly, at this time. So we need new foundations which will be formulated in a formal system which can be used, despite its inconsistency or possible inconsistency, can be used to construct reliable proofs. So the classical first order logic is not good at it, because of it has an inconsistency then one can prove everything and it stops being informative. However there are other types of formal systems which can be used for the formalization of mathematics. Which react to inconsistency in a much less drastic way in a sense. So inconsistency in such systems doesn't mean the system becomes totally uninformative. And one example of such classes of systems is the so called constructive type theories. And that is a class of formal systems which have been used extensively in the theory of programming languages. start = 35:00 end = 37:00