What if Current Foundations of Mathematics are Inconsistent? | Vladimir Voevodsky

Vladimir Voevodsky, Professor, School of Mathematics, Institute for Advanced Study
www.ias.edu/people/faculty-and...
In this lecture, Professor Vladimir Voevodsky begins with Gödel's second incompleteness theorem to discuss the possibility that the formal theory of first-order arithmetic may be inconsistent. This lecture was part of the Institute for Advanced Study's celebration of its eightieth anniversary, and took place during the events related to the Schools of Mathematics and Natural Sciences.
More videos at video.ias.edu

[@lucasthompson1650]

It should be mentioned that Vladimir passed away suddenly in September 2017. A lecture covering many of the subjects of his life's work can be found here: kzbin.info/www/bejne/eJLRfpqsmbCDbqc

[@saulberardo5826]

Thank you professor. While your ideas continuous to resonate through time, a part of you will be alive. RIP

[@kamilziemian995]

Truly outstanding lecture.

[@NoNTr1v1aL]

Absolutely brilliant video!

[@Sidionian]

Thank you for the upload.

[@ba0cbmft]

Every time I watch videos on this topic I keep thinking everything will eventually boil down to lambda calculus or something similar. While it's nice to have arithmetic operators defined at the outset, lambda calculus lets you build these from an even more primitive object: the act of computation itself. Of course there is the problem that it melts your brain because even defining simple things like numbers requires understanding how nested bags of NOP work (e.g. 3 := λf.λx.f (f (f x))).

[@jamma246]

49:10 This is clearly Witten :)

[@tricky778]

Why would you believe Gödel's theora when they might have been proved in an inconsistent logic?

[@UrgeidoitNet]

great job!

[@LaureanoLuna]

If the issue is that we cannot prove that first-order arithmetic is consistent, we should remember that if it were inconsistent, we could use it to prove it consistent. Thus, the initial assumption of the talk seemingly rules out its suggestion. It is known since Aristotle that not all that can be known can be proven: some points are too obvious to require or admit proofs.

[@DustinRodriguez1_0]

Isn't there a fourth possible choice? Accept that the sensation of 'knowing' that first order arithmetic is consistent is an illusion... but that first order arithmetic IS consistent and it is our system of proof which is inadequate. If general principles exist which unite all complex systems, those principles (unknown to us at present) may establish its consistency at a later date. They would have to be introduced as one or more axioms, of course, but I'm not aware of anything that rules such a thing out entirely.

[@alvaropintado9031]

No, not really. I don't know how much you've read, but after Godel's initial results, the results were further extended to essentially any formal axiomatic system (sufficiently strong for arithmetic), no matter what or how many axioms you have. So no, we won't one day find the "magic" axioms that will prove the First-Order Arithmetic is consistent.

[@JohnVKaravitis]

Good info. Has any further progress been made on this issue since 2012?

[@LaureanoLuna]

No, and doesn´t seem likely to be about to happen, at least in mathematical terms .

[@GrothenDitQue]

Ooooh yeah. Look for Univalent Foundations & Homotopy Type Theory (HoTT). 😉 It sadly seems to have slightly slid away from the Consistency concerns, thought 😔... In a different direction, you can have a look at Paraconsistent Logics too (and Dialetheism for the Physical part). 😊

[@LaureanoLuna]

34:00 "The nature of Goedel's argument shows that it is imposible to construct foundations for mathematics that will be provably consistent". That's true as long as such foundations are formal (a formal system), consistent and total (encompassing all our possible mathematical knowledge). For if they are formal and consistent, Gödel's second theorem prohibits them from proving their own consistency, and if they are total, nothing can be proved outside of them.

[@joanasequeirasilva]

You suffer from the same problem. You cannot think outside your own psychology.

[@forocultural81]

I revisited this talk after hearing of the death of this arresting mathematician. Sad that he died so early!

[@kamilziemian995]

Requiescat in pace. Yes, he die much too soon.

[@likebox2]

The basic principle of induction to epsilon-naught is self evident because epsilon naught is explicitly defined as a limit of ordinals produced by explicit operations on ordinals, and taking explicit ordinal limits. The justification for the principle is similar to the justification of the statement that if you count down from any integer, you reach 1 in a finite number of steps. The additional idea that if you count down from a limit ordinal, you are effectively counting down from any one of the elements of the sequences which approach this limit, and if all of these are finite, then counting down from the limit must be finite. This is a new self-evident principle, similar to counting, but unlike the formalization of counting by first order induction, the formalization of counting down from computable ordinals is very strong, it can prove the consistency of arbitrarily strong theories. But in the case of epsilon-naught, it is relatively weak, because epsilon-naught is a rather small ordinal. Gentzen proved the consistency of arithmetic in the correct way, it requires no noncomputable structures, and it is a proof which is completely convincing, and capable of generalizing to complete the whole of Hilbert's program.

[@Youtube_Stole_My_Handle_Too]

Why is the whiteboard covered by the live feed?

[@anon8109]

Such clarity of thought is rarely achieved when discussing views that are skeptical in the extreme regarding logic, math, and physics. Although the statement he puts up of Goedel's second incompleteness theorem seems too strong at first, he explains later why it actually is not.

[@Osama30061989]

As one mathematician has put it, Godel's theorem means that there is no theory of everything in mathematics.

[@dacianbonta2840]

F->T, but not T->F, so no sweat. Working out what's the "F" is in the foundations will be a great qwest

[@alquinn8576]

physics as a formal system where none of the problems halt (because theories are always potentially falsifiable)? Maybe there *is* a creative transcendental aspect to knowledge and awareness which sidesteps Godel that is not systemizable (e.g. Feyerabend "Against Method" and Penrose's view of the human mind). Disclaimer: i'm stoned :0

[@arekkrolak6320]

is this example theorem really true in domain of natural numbers?

[@GrothenDitQue]

Which example? And what do you mean "really true"? 😊

[@edmondedwards6729]

could it be more accurate to say that the mathematics is only as consistent as the underlying logic that makes it perform under certain limitations?

[@angelustt]

is this an official channel or..?

[@GrothenDitQue]

It is! Why?

[@alquinn8576]

how are constructive type theories an improvement over the Turing oracle machine which appears to fall prey to the same problems?

[@DonGateley]

@Carla: Prove it. :-)

[@truantj]

Okay, Hilbert...

[@auditionyourself1323]

I can't believe it 11,653 view and not a single comment.

[@justsignmeup911]

I would have liked to hear why he discounts the second choice.

[@magicsqr3414]

@ 57:00, is that the Waterboy asking a question? thank god we're listening to something sensible like the inconsistency of the 1st principles of mathematics as opposed to something silly like 'foolsball'

[@GrothenDitQue]

It is very weird how he seems not to even know the about Paraconsistent Logics (and Dialetheism for the Physical part)? 😮🤔

[@tarikozkanli788]

Can you prove that it is consistent?

[@GrothenDitQue]

That what is Consistent?

[@MyAce8]

no

[@mrnarason]

RIP

[@happycurmudgeon7430]

And you proved this?

[@GrothenDitQue]

Uh?

[@jimhebert888]

First order arithmetic is indeed consistent. The issue is that the consistency cannot be "Proven." This is important for subjects like theoretical computer science because programming languages are built on formal systems of mathematical logic. This proves that it is not possible to provide a formal "Proof" of the correctness of a computer program. In other words, all computer programs will have bugs.

[@GrothenDitQue]

Dude. You cannot know if it is if none proved it. X)

[@orlandomoreno6168]

Wrong. It's possible to prove correctness for programs. Even if finding the proof itself is undecidable, many programs will be correct and provably so.