Live data from Hacker News

Doing Mathematics Differently

inference-review.com

41–50 of 73 posts

Re: Doing Mathematics Differently

#41
post #36

The author keeps talking about going through all possible proofs built from the axioms, as if that's a thing that obviously could be done. However, if your system is complicated enough to allow arbitrarily large combinations of axioms in your proofs, then I don't understand how you can expect enumeration of all proofs to be a finite process. Any statement that says "enumerate all possible proofs" followed by "and the…

He's not assuming finiteness, just countability.

An example of how this is useful: If it were provable that a program does not halt, an enumeration of all proofs would find the proof that the program does not halt. (If a program does halt, it is necessarily provable that it does so, for obvious reasons.)

Thus either,

- We can solve the halting problem, or - There exists something that is true but not provable.

Thus the uncomputability of the halting problem implied Goedel's incompleteness theorem. Proving the other direction can be done by similar techniques.

Re: Doing Mathematics Differently

#42

This is a good article, and an important topic, but it mischaracterizes the discipline of mathematics: > the principle that mathematical truth is black or white and provides absolute certainty. > Pure mathematicians like to think that they have absolute truth Formal mathematics has no concept of absolute truth; this is left for philosophy. It's just concerned with axioms and theorems (and their proofs). Whether an ax…

> Formal mathematics has no concept of absolute truth ...

Well, it does. If you drag the propositional calculus into the fray, "true" is arbitrarily but probably most elegantly defined as following:

true(x) = x or not x

False is defined like this:

false(x) = x and not x

These definitions are pretty much arbitrary. The lambda calculus does this:

true(a,b)=a

false(a,b)=b

It also works absolutely fine.

> It's just concerned with axioms and theorems (and their proofs)

In the general case, theorems are indeed "provable" or "unprovable" (not "true" or "false").

However, if a theorem has exclusively been derived from propositional calculus, it can also be "true".

Gödel's incompleteness is exactly about statements that are "true but unprovable". In terms of propositional calculus, the theorem is "true" but since you can show that the theorem can never be derived from the axioms, it is also "unprovable".

Re: Doing Mathematics Differently

#43
post #37
post #24

Earlier quoted context omitted.

If you have different rules, you have a different object and the meaning of the axiom is different. Even if it is written using the same symbols. To continue the compiler analogy.. Just because the ASCII sequence "int c=0;" means different things in C and Java, doesn't imply "int c=0;" is meaningless when specifically talking about only C.

Not necessarily. It's very possible for one system to embed inside the other. In this case you can often talk about exactly the same axiom/theorem/whatever within different inferential systems. An interesting example is the Axiom of Choice which is, naively encoded, a theorem of intuitionistic logic. That said, we can use flattening to embed classical logic inside of intuitionistic logic and then recover a whole fami…

> An interesting example is the Axiom of Choice which is, naively encoded, a theorem of intuitionistic logic.

Naïvely encoded in Martin-Löf type theory, that is.

Re: Doing Mathematics Differently

#44
post #42

This is a good article, and an important topic, but it mischaracterizes the discipline of mathematics: > the principle that mathematical truth is black or white and provides absolute certainty. > Pure mathematicians like to think that they have absolute truth Formal mathematics has no concept of absolute truth; this is left for philosophy. It's just concerned with axioms and theorems (and their proofs). Whether an ax…

> Formal mathematics has no concept of absolute truth ... Well, it does. If you drag the propositional calculus into the fray, "true" is arbitrarily but probably most elegantly defined as following: true(x) = x or not x False is defined like this: false(x) = x and not x These definitions are pretty much arbitrary. The lambda calculus does this: true(a,b)=a false(a,b)=b It also works absolutely fine. > It's just conce…

Well, it does not. Mathematics is a symbolic system invented by humans, but that system tells you nothing about the state of the world.

Used correctly, it can be used to describe the world, but it can also be used to describe phenomena that have not been physically observed. E.g., currently accepted theories allow for existence of wormholes, but we do not know whether the actual physical laws of the universe ("absolute truth") do.

So, no, there is no "absolute truth" in mathematics. There are only valid derivations, but taking them as the "absolute truth" is like mistaking the pointing finger for the moon.

Re: Doing Mathematics Differently

#45
post #22
post #14

Earlier quoted context omitted.

The author just probably like Leibniz a lot and prefer to make the citation in the original language of the text. Would you have preferred Latin or German ? Leibniz used them too.

> Would you have preferred Latin or German? I could get by with German, but that's beside the point: the essay is written for an English-speaking audience, so it's stupid to insert extended passages of foreign text without providing translation.

Obviously nobody is forcing you to read it. Perhaps it's written for an English speaking audience that doesn't mind skipping over some French here and there.

Re: Doing Mathematics Differently

#46
post #7

What's the point of inserting untranslated French text into an English article? Is it supposed to just be window-dressing? Is it supposed to promote the (outdated and highly dubious) notion that all educated people speak French? Is it just for the author to show off? Whatever the reason, it's a highly obnoxious practice and it doesn't improve the article.

Come on. Looking up what the quote means takes like 1% of the effort of understanding the article.

You shouldn't jump to assuming malice when someone's aesthetic tastes differ from your own.

By the way, the quote means (my own translation):

> God chose the one which was the most perfect; that is, the one which whose hypotheses were the simplest, and whose phenomena were the richest.

> But when a rule is very intricate, that which follows it seems irregular.

Re: Doing Mathematics Differently

#47

This is a good article, and an important topic, but it mischaracterizes the discipline of mathematics: > the principle that mathematical truth is black or white and provides absolute certainty. > Pure mathematicians like to think that they have absolute truth Formal mathematics has no concept of absolute truth; this is left for philosophy. It's just concerned with axioms and theorems (and their proofs). Whether an ax…

Have you followed Gödel's proof in detail? I know Fields medalists who like to speculate about Gödel, but haven't read Russell and Whiteheads Principia Mathematica (PM). Gödel's system is PM, but PM is quite an impossible read. Most of this discussed has been discussed over 30 years between 1900-1930. By the way Turing also builds on PM in his on computable numbers paper. PM is like a compiler before there were compilers. Today it would look more like metamath.org or https://github.com/vladimirias/Foundations

> Formal mathematics has no concept of absolute truth; this is left for philosophy.

No, it is called logic which is the intersection of both. And most mathematicians haven't done any logic whatsoever. They avoid it, because it means you actually have to think about things. You have to think about why greek symbols have special meanings. And as computer scientists/hackers know, computer code is an alternative medium.

I remember when I asked a math professor about the "=" sign and how things can be equal at all, since if they are either the same (A=A is trivial), it is trivial, or if they are different they are not the same (A=B is false). About 10 years later I discovered this is why physics has the notion of symmetries, which is a statement of the form A - B = 0. Two things are equal iff their transformation leads to the origin. But I should have known this all along, because in computer programs "=" can stand for various kinds of operations. It is just that the language of mathematics in general is so inaccurate that one gets lost on the way.

Re: Doing Mathematics Differently

#48
post #19

This is a good article, and an important topic, but it mischaracterizes the discipline of mathematics: > the principle that mathematical truth is black or white and provides absolute certainty. > Pure mathematicians like to think that they have absolute truth Formal mathematics has no concept of absolute truth; this is left for philosophy. It's just concerned with axioms and theorems (and their proofs). Whether an ax…

"Formal mathematics has no concept of absolute truth" This is false. The axioms don't have to be true. You can still talk about their implications in absolute terms. "Assuming a=0 implies a=0" is absolutely true. Regardless of whether a actually is 0.

"The axioms don't have to be true."

No, not at all. Axioms are better thought of as universally accepted truths which everything else depends on. https://en.wikipedia.org/wiki/Logical_atomism

Re: Doing Mathematics Differently

#49

This is a good article, and an important topic, but it mischaracterizes the discipline of mathematics: > the principle that mathematical truth is black or white and provides absolute certainty. > Pure mathematicians like to think that they have absolute truth Formal mathematics has no concept of absolute truth; this is left for philosophy. It's just concerned with axioms and theorems (and their proofs). Whether an ax…

Have you followed Gödel's proof in detail? I know Fields medalists who like to speculate about Gödel, but haven't read Russell and Whiteheads Principia Mathematica (PM). Gödel's system is PM, but PM is quite an impossible read. Most of this discussed has been discussed over 30 years between 1900-1930. By the way Turing also builds on PM in his on computable numbers paper. PM is like a compiler before there were compi…

I'm a bit dubious about your sweeping generalisation that "most mathematicians haven't don't any logic".

I also agree with GP that logic also does not deal with absolute truth. Proofs in formal logic may be applied to models, but they only provide truths modulo the assumptions made in those models.

As for your remark on equivalence. Your original description is one of syntactic identity, a sort of free equivalence. But any relation that is reflexive, transitive and symmetric can be considered an equivalence (indeed, there are infinitely many equivalence relations over the integers). Also note that this is not the same as how "=" is used in computer programs where for the most part it is asymmetric (a=b is rarely semantically equivalent to b=a).

Re: Doing Mathematics Differently

#50
post #21

Earlier quoted context omitted.

You can't have the same axioms with different rules of inference. The rules of inference are axioms. By the axioms being the same, you mean the ink-shapes making up the symbols on a piece of paper being the same. Not the actual meaning behind them. Edit: Since you added more content to this reply later on, let me respond. In this case I was talking about specifically a formal system where a=0 makes sense and is expre…

Axioms and rules of inference are fundamentally different: (0) An axiom is an internal statement to a mathematical theory that is assumed to be true. That is, inside of a mathematical theory, you don't need to prove that its axioms hold. However, if you want to construct a model of a mathematical theory, you need to prove externally that the axioms hold. In return, you get the theory's theorems (suitably interpreted)…

    Axioms and rules of inference are fundamentally different:

Things are not that simple, because you can often convert axioms to rules of inference or vice versa, without changing the set of derivable consequences.

As an example, consider pure first-order logic (FOL). As one extreme, you can present FOL with just one rule of inference (Modus Ponens), see for example [1]. The other extreme is Gentzen's sequent calculus [2] which has only one axiom (A |- A), everything else being a rule of inference. Most presentations of FOL are between these extremes.

[1] A mathematical introduction to logic, by H. Enderton

[2] Untersuchungen über das logische Schliessen I, by G. Gentzen

Post reply on HN