Live data from Hacker News

Gottlob Frege: The machine in the ghost (2017)

prospectmagazine.co.uk

21–26 of 26 posts

Re: Gottlob Frege: The machine in the ghost (2017)

#21
post #18

Earlier quoted context omitted.

Principia was destroyed by Gödel, within about two years of its publication. That's what I'm referring to.

No, it wasn't. I'm sometimes not sure if philosophers understand Goedel's incompleteness theorem. What do you base your claim on? GIT is more a statement about the limitations of the proof-driven approach to mathematics than it is about any formalisation of mathematics like Principia's. It shows that whatever assumptions proofs are based on cannot be shown consistent except by assuming something even stronger. Princi…

Well, I'm out of my depth. I didn't study Principia or Gödel at school, and I've never really looked into Principia. My understanding is that Principia was an effort to prove that (a) mathematics was logic; and (b) that mathematics was self-consistent. And that Gödel proved that this goal couldn't be achieved.

Is that wrong? If I've got that wrong, I have a big attitude adjustment coming down the track towards me.

Re: Gottlob Frege: The machine in the ghost (2017)

#22
post #18

Earlier quoted context omitted.

Principia was destroyed by Gödel, within about two years of its publication. That's what I'm referring to.

No, it wasn't. I'm sometimes not sure if philosophers understand Goedel's incompleteness theorem. What do you base your claim on? GIT is more a statement about the limitations of the proof-driven approach to mathematics than it is about any formalisation of mathematics like Principia's. It shows that whatever assumptions proofs are based on cannot be shown consistent except by assuming something even stronger. Princi…

> I'm sometimes not sure if philosophers understand Goedel's incompleteness theorem

I'm usually not sure if I understand it (reverse: Im usually sure that I don't understand it). Also: I'm not a philosopher - I'm an old man that did a philosophy BA 40 years ago. I can't unpack this stuff.

I see a consonance between Gödel's theorems, Heisenberg's principle, Turing's work on computability, and some of the stuff in Frege and Wittgenstein. Maybe even Cantor. I wish I could to say this clearly-enough for someone to knock down. But I can't do the maths; I'm entirely dependent on the explanations of others.

Re: Gottlob Frege: The machine in the ghost (2017)

#23
post #15
post #11

Earlier quoted context omitted.

There's too much focus on Frege (as well as Russell and Wittgenstein) in analytic philosophy. You would think people such as Boole, Peirce, Łukaiewicz, Tarski, Brouwer, Heyting, Gentzen, Prawitz, Girard, and Martin-Löf are mere footnotes in the history of logic. Yet their work is more relevant and used by working mathematicians and computer scientists.

This is a brilliant comment. Thank you. Each in turn: Boole invented propositional logic. Peirce supposedly invented a lot, but got overlooked. Łukaiewicz, I'm not sure. Tarski employed quantifier elimination to prove the decidability of various theories like Euclidean geometry. Brouwer invented intuitionistic logic, and a(n arguably) viable approach to doing analysis and topology intuitionistically. Heyting provided…

And Gödel, of course.

Re: Gottlob Frege: The machine in the ghost (2017)

#24
post #15
post #11

Earlier quoted context omitted.

There's too much focus on Frege (as well as Russell and Wittgenstein) in analytic philosophy. You would think people such as Boole, Peirce, Łukaiewicz, Tarski, Brouwer, Heyting, Gentzen, Prawitz, Girard, and Martin-Löf are mere footnotes in the history of logic. Yet their work is more relevant and used by working mathematicians and computer scientists.

This is a brilliant comment. Thank you. Each in turn: Boole invented propositional logic. Peirce supposedly invented a lot, but got overlooked. Łukaiewicz, I'm not sure. Tarski employed quantifier elimination to prove the decidability of various theories like Euclidean geometry. Brouwer invented intuitionistic logic, and a(n arguably) viable approach to doing analysis and topology intuitionistically. Heyting provided…

The people I mentioned and their work are intentionally overlooked because it doesn't fit a dogma around Platonic Realism and Classical Logic.

Re: Gottlob Frege: The machine in the ghost (2017)

#25
post #18

Earlier quoted context omitted.

No, it wasn't. I'm sometimes not sure if philosophers understand Goedel's incompleteness theorem. What do you base your claim on? GIT is more a statement about the limitations of the proof-driven approach to mathematics than it is about any formalisation of mathematics like Principia's. It shows that whatever assumptions proofs are based on cannot be shown consistent except by assuming something even stronger. Princi…

> I'm sometimes not sure if philosophers understand Goedel's incompleteness theorem I'm usually not sure if I understand it (reverse: Im usually sure that I don't understand it). Also: I'm not a philosopher - I'm an old man that did a philosophy BA 40 years ago. I can't unpack this stuff. I see a consonance between Gödel's theorems, Heisenberg's principle, Turing's work on computability, and some of the stuff in Freg…

[I wrote this yesterday, but didn't post it]

Let's assume that mathematics is a job that follows the following rules: You use two languages: Predicate Logic and Natural Deduction. You use Predicate Logic to write claims like "There are infinitely many prime numbers", and you use Natural Deduction to construct proofs of such claims. Both languages are formal. And you can even use a computer to verify that you're using them correctly.

To prove things, you need to assume that some things are true. These "assumptions" are called axioms, and are expressed using Predicate Logic. Philosophically speaking, the rules of Natural Deduction can be thought of as axioms for how to correctly construct proofs, but they're usually called "inference rules" and not axioms for minor technical reasons.

The methodology which we described arises inevitably from a proof-driven approach to mathematics, because mathematicians need a way to agree which methods of argumentation they think are correct, and also to prevent people from making things up. Admittedly, this is only true for those mathematicians who have looked into these foundational matters.

Some axioms can lead to an accident where you can prove a proposition and its negation simultaneously. (An example in set-theoretic foundations is Unrestricted Comprehension.) By a simple result called the principle of explosion, in such a situation you can prove every proposition and its negation. So such axiom sets are useless. We call them inconsistent.

A question arises: Given a set of axioms which is sufficient to serve as a foundation of mathematics - like ZFC set theory for instance, or less obviously Peano arithmetic - is it possible to construct a proof of their own consistency from those same axioms alone? The answer is no, and this is Goedel's 2nd Incompleteness Theorem.

You can - in a way - prove that Peano arithmetic (for instance) is consistent, but you need to assume axioms which are strictly more powerful than Peano arithmetic. And to show the consistency of those axioms, you need to assume yet stronger ones. This is quite a disturbing situation.

Ultimately, the theorem is a statement about the methodology for doing mathematics which we described. But there is no escaping it if mathematics is about stating claims and proving them.

Re: Gottlob Frege: The machine in the ghost (2017)

#26
post #25

Earlier quoted context omitted.

> I'm sometimes not sure if philosophers understand Goedel's incompleteness theorem I'm usually not sure if I understand it (reverse: Im usually sure that I don't understand it). Also: I'm not a philosopher - I'm an old man that did a philosophy BA 40 years ago. I can't unpack this stuff. I see a consonance between Gödel's theorems, Heisenberg's principle, Turing's work on computability, and some of the stuff in Freg…

[I wrote this yesterday, but didn't post it] Let's assume that mathematics is a job that follows the following rules: You use two languages: Predicate Logic and Natural Deduction. You use Predicate Logic to write claims like "There are infinitely many prime numbers", and you use Natural Deduction to construct proofs of such claims. Both languages are formal. And you can even use a computer to verify that you're using…

Thanks - that's a succinct and interesting summary of something; but I'm not sure how it's a reply to my comment :-)
Post reply on HN