My Math Forum > Math Are you skeptical of pure math?
 User Name Remember Me? Password

 Math General Math Forum - For general math related discussion and news

July 9th, 2014, 11:52 AM   #11
Senior Member

Joined: Dec 2013
From: Russia

Posts: 327
Thanks: 108

Quote:
 Originally Posted by CRGreathouse Goedel's incompleteness theorem is very simple -- some of the modern proofs (see, e.g., Aaronson for exposition) are quite short and easy to follow.
Is this a proof using Turing machines instead of the fixed-point lemma? I found some lecture notes, but is there a book or an article?

Quote:
 Originally Posted by CRGreathouse His second incompleteness theorem is essentially just a corollary to the first, trivial to prove given that.
I am not sure I agree with that. The proof that I've seen requires a large amount of technical work, but it can be hidden behind the phrase, "the proof of … can be formalized". I am talking about Hilbert-Bernays derivability conditions.

Quote:
 Originally Posted by CRGreathouse Goedel's completeness theorem, I will admit, I have not proven. As I understand the proof is straightforward but rather involved.
When I had an introductory logic course, the completeness theorem was proved by the middle of the course while Gödel's incompleteness theorems were proved at the very end. Compared with the proof of the first incompleteness theorem that uses the fixpoint lemma, if one counts all the technical development about Gödel numbers, I believe the proof of the completeness theorem is shorter.

First incompleteness theorem has been proved in Coq by Russell O'Connor in 2003 (Wikipedia).

 July 9th, 2014, 12:17 PM #12 Senior Member   Joined: Jul 2013 From: United Kingdom Posts: 471 Thanks: 40 To bobsmith76 I'd say that the scientific method is the most powerful tool you can use to reason. Those that developed this method of reasoning acknowledged the fact that the universe is unpredictable. They had also acknowledged the fact that humans make errors. They had understood that facts we accept today may not be accepted tomorrow. All theories contain errors. That is why they are called theories. They are not absolute truths. Our scientific and mathematical theories are a work in progress. The best theories help us explain how the world works, and they make sense to us today. They may not make sense tomorrow. Better theories will emerge and some theories will be scrapped. Nothing is set in stone. Try not to attach yourself to a belief system. Keep your mind open.
July 9th, 2014, 12:30 PM   #13
Global Moderator

Joined: Nov 2006
From: UTC -5

Posts: 16,046
Thanks: 938

Math Focus: Number theory, computational mathematics, combinatorics, FOM, symbolic logic, TCS, algorithms
Quote:
 Originally Posted by Evgeny.Makarov Is this a proof using Turing machines instead of the fixed-point lemma? I found some lecture notes, but is there a book or an article?
It's a reduction from Turing's theorem, yeah. I believe it was published in Quantum Computing Since Democritus (2013).

Quote:
 Originally Posted by Evgeny.Makarov The proof that I've seen requires a large amount of technical work
I'm fairly sure I could prove this in a few tens of minutes. The last time I worked on it I found it very easy.

I would *not* have found Aaronson's proof of the (first) incompleteness theorem on my own, though! "Easy to follow" is not the same as "easy to prove" (well, modulo P != NP... ).

Quote:
 Originally Posted by Evgeny.Makarov When I had an introductory logic course, the completeness theorem was proved by the middle of the course while Gödel's incompleteness theorems were proved at the very end. Compared with the proof of the first incompleteness theorem that uses the fixpoint lemma, if one counts all the technical development about Gödel numbers, I believe the proof of the completeness theorem is shorter.
I agree that the standard treatment of the (first) incompleteness theorem is longer than the standard proof of the completeness theorem, yes. But now I'm a convert to the easier proof. I find it more enlightening than the standard proof, for one thing.

Quote:
 Originally Posted by Evgeny.Makarov First incompleteness theorem has been proved in Coq by Russell O'Connor in 2003 (Wikipedia).
It was also proved in HOL Light, Isabelle, and nqthm according to Freek Wiedijk's standard reference "Formalizing 100 Theorems". (The Completeness Theorem is on his 'bonus' list but that doesn't mention whether it's been formalized or not.)

It looks like the Completeness Theorem has been proved in Isabelle here: http://afp.sourceforge.net/entries/C...ness-paper.pdf (Margetson 2004).

Last edited by CRGreathouse; July 9th, 2014 at 12:34 PM.

 July 9th, 2014, 12:31 PM #14 Senior Member   Joined: Jul 2013 From: United Kingdom Posts: 471 Thanks: 40 If you search for errors you will find them - in everything. Perfection contradicts itself. We live in a universe based on probabilities, not absolute certainties. Our universe is multi-dimensional, not linear. There are too many variables for us to cope with. Even our most powerful computers struggle to make accurate predictions about the future. This may be hard to accept, but nature has shown us that there is a lot to understand about this universe we inhabit. There is a lot to uncover. Logic won't provide answers to everything, and maths won't either. We are only human beings after all.
July 9th, 2014, 12:32 PM   #15
Math Team

Joined: Dec 2013
From: Colombia

Posts: 7,664
Thanks: 2644

Math Focus: Mainly analysis and algebra
Quote:
 Originally Posted by bobsmith76 just look at Godel's Theorems which everyone believes (most simply accepting it on authority) but are most likely false
Generally, I'm not sceptical of mathematics where there are extant, accepted proofs. Especially where I understand them myself.

Given the nature of your question, and the rest of the hullabaloo in this thread, I think you should explain on what basis you rest your claim rather than expecting others to justify why they believe in published, peer reviewed work.

 Tags math, pure, skeptical

 Thread Tools Display Modes Linear Mode

 Similar Threads Thread Thread Starter Forum Replies Last Post herozs Career Guidance 12 July 18th, 2017 10:37 PM BenFRayfield Math Software 0 May 29th, 2013 06:35 PM J.Xavier Academic Guidance 1 May 14th, 2013 11:32 AM hemantc007 New Users 9 May 19th, 2010 06:24 AM 321 Academic Guidance 2 April 3rd, 2010 01:56 PM

 Contact - Home - Forums - Cryptocurrency Forum - Top