5 ms·
I suppose the inaccuracies caused by the 'prose' of Ampère's false proof that all continuous functions are differentiabe might be what inspired Hilbert's demand
by rocqua 9y ago
I suppose the inaccuracies caused by the 'prose' of Ampère's false proof that all continuous functions are differentiabe might be what inspired Hilbert's demand for rigor. In turn, this lead to Godel's incompleteness.
We are then left in the curious situation of despising any hand waving, whilst knowing deep down that at some point we need to accept things without rigorous proof. Of course, that other reason to hand-wave remains. Often, things are `obvious' and yet very very tedious to proof. It is an odd balance to strike.
- whatshisface 9y agoUnprovable statements weaken provable ones no further than the extent to which the undecidability of the halting problem makes my toaster burn my Eggos.
- visarga 9y agoYour toaster has a halting problem?
- eternalban 9y agohttp://lambda-the-ultimate.org/node/4302 http://lambda-the-ultimate.org/node/4302 There seems to me an enormous mistake there. ... Suppose I convince [someone] of the paradox of the Liar, and he says, 'I lie, therefore I do not lie, therefore I lie and I do not lie, therefore we have a contradiction, therefore 2x2 = 369.' Funniest thing is I agree with both of them ..
- whatshisface 9y agoYes, it has the halting problem for a machine much less powerful than a Turing machine, where the answer is always yes unless the thermostat fails. The idea is that just like there are programs less powerful than the halting oracle there are statements less powerful than the completeness of arithmetic.
- rocqua 9y agoI refer to Godel's second incompleteness theorem. That is, no system of axioms can prove itself to be consistent. Thus, all provable statements rest on an unproveable statement.
- deleted 9y ago[deleted]
- quickthrower2 9y agoI've heard that propositional logic helps with this because you don't assume everything is either true or false, but rather look at what can be implied. You can then decide if you want the law of the excluded middle or not. I'm paraphrasing a talk I watched but would love to hear from someone knowledgeable on this subject...
- sddfd 9y agoYou are probably thinking of intuitionistic logic versus classical logic. In the former, the law of excluded middle is not built in.
- quickthrower2 9y agoYes that's the one. Thanks
- mcguire 9y agoIf you have heard of the Curry-Howard equivalence, that programs and proofs are the same thing, the proofs in question are constructive, intuitionistic proofs.
- rocqua 9y agoI've been leaning towards intuitionism for exactly this reason. Sadly, it makes a lot of results harder to proof (and iirc it even makes some results impossible). I've been toying with the idea that these results are simply 'not useful'.
- adrianN 9y agoGödel's incompleteness theorem doesn't immediately imply that we have to accept some things without rigorous proof. It just shows the limits of what you can prove within one axiomatic system.
- bonzini 9y agoRight, but Hilbert wanted to axiomatize arithmetics and all of mathematics in order to make proofs rigorous. It was one of his 23 problems, and Godel solved it (negatively).
- n4r9 9y agoIt wasn't so much to make proofs rigorous, as to determine whether or not there would always exist "true" statements which could not be proved. Hilbert had already proposed a set axioms for second-order arithmetic - he just didn't know whether they were both complete and consistent.
- rocqua 9y agoHis second incompleteness theorem implies we can never rigorously know our axioms are consistent. Thus, no proof is 'truly' rigorous. We have to depend on the prose of 'these axioms are so self evident that it is obvious they are consistent'. This is what originally made people suspicious of the axiom of choice. It is much less self evident than the other axioms of ZF.
- xamuel 9y agoIt's better to think of axioms as definitions. If the axioms are inconsistent, it just means nothing satisfies the definition, which isn't the end of the world. People have spent time studying hypothetical properties of polynomial-time factorization algorithms, knowing full well there may be no such things if P<>NP. There are models of ZF where the axiom of choice holds, and there are models of ZF where the axiom of choice doesn't hold. To "assume" the axiom of choice, is nothing more than to restrict attention to the former. No more controversial than, say, deciding to write a paper specifically about golden retrievers, rather than a paper about all dogs.