Hacker News Reader

Comment by rocqua | Hacker News Reader

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.

View on HN

Unprovable statements weaken provable ones no further than the extent to which the undecidability of the halting problem makes my toaster burn my Eggos.

Your toaster has a halting problem?

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

Yes, 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.

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

Gö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.

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

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

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

It'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.

If your axioms are inconsistent, you can use reductio ad absurdum to prove any statement. I'd say that it is rather problematic when I can prove any statement and it's converse.

Of course, just because the axiom of choice isn't obvious doesn't mean that ZFC is inconsistent. It just means that the argument for ZFC being inconsistent is more hand-wavy.

Of course you can prove any statement. The statements only hold for things which satisfy the axioms. "If X is a model of ZF where 1=0, then X also satisfies anything else you want." (Fine, there is no such X so who cares.) You're getting confused because of the shorthand where statements within the model are stated as if they are statements about the world we live in. That's just a shorthand.

Yes we must take saxioms on faith alone. Embrace pluralism and move on.

https://m.youtube.com/watch?v=O45LaFsaqMA by the late great Voedvodvosky is more interesting.

I'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...

You are probably thinking of intuitionistic logic versus classical logic. In the former, the law of excluded middle is not built in.

Yes that's the one. Thanks

If you have heard of the Curry-Howard equivalence, that programs and proofs are the same thing, the proofs in question are constructive, intuitionistic proofs.

I'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'.

Reply on news.ycombinator.com