News for hackers. Stuff that matters.
Re:There’s more to mathematics than rigour and proofs (2007) by hither_shores on Wednesday April 20, 2022 @12:45AM (#31092899)
That is not at all what the incompleteness theorems say.

The first incompleteness theorem says that for any consistent formal system T (with a recursively enumerable set of axioms) capable expressing of elementary arithmetic, T can express a statement which it can neither prove nor disprove.

The second incompleteness theorem says that T can't prove the statement "T is consistent". (I've still glossed over a number of technical details here; pick up a book on model theory if you want all the messy internals.)

First order logic is notably not capable of expressing elementary arithmetic. And observers aren't involved in any way.

Re:There’s more to mathematics than rigour and proofs (2007) by postingposts on Wednesday April 20, 2022 @01:27AM (#31093159)
Yes, it is.

Sorry if you can’t read deeply into it or something. I’m not posting for grad students. I can sense you just like to correct people. Ahhhh I’m so wrong, you’re right?

Re:There’s more to mathematics than rigour and proofs (2007) by dang on Wednesday April 20, 2022 @10:49AM (#31097751)
We've banned this account for continuing to break the site guidelines after we asked you to stop.

https://news.ycombinator.com/newsguidelines.html

Re:There’s more to mathematics than rigour and proofs (2007) by Agingcoder on Wednesday April 20, 2022 @08:00AM (#31095635)
Godel's theorems mean something quite specific, and rely on an equally specific set of hypothesis.

It's tempting to try to apply them (or rather the same kind of conclusions) in other (non math) contexts, but it's very not obvious that you'll get something sensible. While you can play with the ideas, invoking Godel's theorem outside of its specific context doesn't make much sense.

Re:There’s more to mathematics than rigour and proofs (2007) by MichaelBurge on Wednesday April 20, 2022 @03:50AM (#31093953)
I usually think of logics as search algorithms, since that's how the semantics for the meta-language describing them are defined.

I guess you could call a Turing Machine implementing the search algorithm for proofs implied by a logic an "observer", since it produces "reachability observations" i.e. proofs.