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

Пікірлер: 51

  • @saulberardo5826
    @saulberardo58266 жыл бұрын

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

  • @lucasthompson1650
    @lucasthompson16505 жыл бұрын

    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: kzread.info/dash/bejne/dJWir8mvlK62aKg.html

  • @kamilziemian995
    @kamilziemian9952 жыл бұрын

    Truly outstanding lecture.

  • @NoNTr1v1aL
    @NoNTr1v1aL11 ай бұрын

    Absolutely brilliant video!

  • @tricky778
    @tricky778 Жыл бұрын

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

  • @jamma246
    @jamma2467 жыл бұрын

    49:10 This is clearly Witten :)

  • @Sidionian
    @Sidionian8 жыл бұрын

    Thank you for the upload.

  • @ba0cbmft
    @ba0cbmft7 жыл бұрын

    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))).

  • @LaureanoLuna
    @LaureanoLuna6 жыл бұрын

    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.

  • @UrgeidoitNet
    @UrgeidoitNet7 жыл бұрын

    great job!

  • @DustinRodriguez1_0
    @DustinRodriguez1_07 жыл бұрын

    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

    @alvaropintado9031

    5 жыл бұрын

    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
    @JohnVKaravitis7 жыл бұрын

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

  • @LaureanoLuna

    @LaureanoLuna

    6 жыл бұрын

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

  • @GrothenDitQue

    @GrothenDitQue

    5 жыл бұрын

    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
    @LaureanoLuna9 жыл бұрын

    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

    @joanasequeirasilva

    4 жыл бұрын

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

  • @forocultural81
    @forocultural816 жыл бұрын

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

  • @kamilziemian995

    @kamilziemian995

    2 жыл бұрын

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

  • @dacianbonta2840
    @dacianbonta28402 ай бұрын

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

  • @anon8109
    @anon81097 жыл бұрын

    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.

  • @Youtube_Stole_My_Handle_Too
    @Youtube_Stole_My_Handle_Too2 жыл бұрын

    Why is the whiteboard covered by the live feed?

  • @alquinn8576
    @alquinn85766 жыл бұрын

    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

  • @likebox2
    @likebox28 жыл бұрын

    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.

  • @arekkrolak6320
    @arekkrolak63207 жыл бұрын

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

  • @GrothenDitQue

    @GrothenDitQue

    5 жыл бұрын

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

  • @Osama30061989
    @Osama300619896 жыл бұрын

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

  • @edmondedwards6729
    @edmondedwards67296 жыл бұрын

    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?

  • @alquinn8576
    @alquinn85766 жыл бұрын

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

  • @angelustt
    @angelustt10 жыл бұрын

    is this an official channel or..?

  • @GrothenDitQue

    @GrothenDitQue

    5 жыл бұрын

    It is! Why?

  • @DonGateley
    @DonGateley10 жыл бұрын

    @Carla: Prove it. :-)

  • @justsignmeup911
    @justsignmeup9116 жыл бұрын

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

  • @truantj
    @truantj10 жыл бұрын

    Okay, Hilbert...

  • @magicsqr3414
    @magicsqr341410 жыл бұрын

    @ 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
    @GrothenDitQue5 жыл бұрын

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

  • @auditionyourself1323
    @auditionyourself13238 жыл бұрын

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

  • @tarikozkanli788
    @tarikozkanli7888 жыл бұрын

    Can you prove that it is consistent?

  • @GrothenDitQue

    @GrothenDitQue

    5 жыл бұрын

    That what is Consistent?

  • @MyAce8

    @MyAce8

    3 жыл бұрын

    no

  • @happycurmudgeon7430
    @happycurmudgeon74309 жыл бұрын

    And you proved this?

  • @GrothenDitQue

    @GrothenDitQue

    5 жыл бұрын

    Uh?

  • @mrnarason
    @mrnarason5 жыл бұрын

    RIP

  • @jimhebert888
    @jimhebert8888 жыл бұрын

    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

    @GrothenDitQue

    5 жыл бұрын

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

  • @orlandomoreno6168

    @orlandomoreno6168

    4 жыл бұрын

    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.