Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Doing Mathematics Differently

inference-review.com

Post reply on HN
Print view View original

21–30 of 73 posts

Re: Doing Mathematics Differently

#21

Post by plutooo »

catnaroek wrote: post #20
plutooo wrote: post #19

Earlier quoted context omitted.

"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. You can still talk about their implications in absolute terms. No, you can't. Two mathematicians using different rules of inference (say, those of classical vs. intuitionistic logic) will arrive at different theorems, even if they begin from the same axioms. > "Assuming a=0 implies a=0" is absolutely true. Assuming that “a = 0” and implication are both expressible in our formal sys…

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 expressible, but to keep it short and concise I didn't choose to write out all the details. So the rebuttal is moot.

Re: Doing Mathematics Differently

#22

Post by gaur »

Rexxar wrote: post #14
gaur wrote: 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.

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.

Re: Doing Mathematics Differently

#23

Post by catnaroek »

plutooo wrote: post #21
catnaroek wrote: post #20

Earlier quoted context omitted.

> The axioms don't have to be true. You can still talk about their implications in absolute terms. No, you can't. Two mathematicians using different rules of inference (say, those of classical vs. intuitionistic logic) will arrive at different theorems, even if they begin from the same axioms. > "Assuming a=0 implies a=0" is absolutely true. Assuming that “a = 0” and implication are both expressible in our formal sys…

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) for free.

(1) A rule of inference exists in an external metatheory, where the original mathematical theory we were studying is treated as a syntactic object (also known as object language), in very much the same way a compiler treats the program being compiled as a (possibly annotated) syntax tree. A rule of inference defines a class of valid syntactic transformations, but doesn't concern itself with the impact of these transformations have on the meaning of the phases in the object language.

It is perfectly sensible to consider the effect of changing the rules of inference, on an axiomatic system.

Re: Doing Mathematics Differently

#24

Post by plutooo »

catnaroek wrote: post #23
plutooo wrote: 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)…

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.

Re: Doing Mathematics Differently

#25

Post by catnaroek »

plutooo wrote: post #24
catnaroek wrote: post #23

Earlier quoted context omitted.

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)…

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.

The problem with your analogy is that C and Java have completely different abstract syntaxes. A better analogy would be taking the syntax of an existing programming language, and completely changing its meaning. For instance, consider the effect of making Racket use lazy evaluation (Lazy Racket), or making Haskell use strict evaluation (the upcoming -XStrict pragma). Strict and lazy languages validate different sets of equational laws (and hence compiler optimizations!), neither of which is a subset of the other, so this is perhaps a more interesting example than switching between intuitionistic and classical logic.

Re: Doing Mathematics Differently

#26

Post by plutooo »

catnaroek wrote: post #25
plutooo wrote: 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.

The problem with your analogy is that C and Java have completely different abstract syntaxes. A better analogy would be taking the syntax of an existing programming language, and completely changing its meaning. For instance, consider the effect of making Racket use lazy evaluation (Lazy Racket), or making Haskell use strict evaluation (the upcoming -XStrict pragma). Strict and lazy languages validate different sets…

But I'm saying if you evaluate the axiom symbols two different ways, it's two different axioms.

Re: Doing Mathematics Differently

#27

Post by catnaroek »

plutooo wrote: post #26
catnaroek wrote: post #25

Earlier quoted context omitted.

The problem with your analogy is that C and Java have completely different abstract syntaxes. A better analogy would be taking the syntax of an existing programming language, and completely changing its meaning. For instance, consider the effect of making Racket use lazy evaluation (Lazy Racket), or making Haskell use strict evaluation (the upcoming -XStrict pragma). Strict and lazy languages validate different sets…

But I'm saying if you evaluate the axiom symbols two different ways, it's two different axioms.

What you're saying is more or less equivalent to “two C implementations targeting different [architectures / operating systems / whatever] are actually implementations of two different programming languages”.

Re: Doing Mathematics Differently

#28

Post by conceit »

conceit wrote: post #13
smilliken wrote: post #9

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…

You are being philosophic asserting that there would be a reality to reflect, in a rather colorful language, while axioms are real enough to not need to pull a strawman from beyond them.

> Formal mathematics has no concept of absolute truth

That's like an absolute truth in formal mathematics then, I suppose.

Re: Doing Mathematics Differently

#29

Post by dllthomas »

catnaroek wrote: post #23
plutooo wrote: 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)…

This seems to be a technical objection that dodges the meat of the parent's comment. In what sense is it true that a given theorem follows from a given set of axioms and a given choice of inference rules?

Re: Doing Mathematics Differently

#30

Post by plutooo »

catnaroek wrote: post #27
plutooo wrote: post #26

Earlier quoted context omitted.

But I'm saying if you evaluate the axiom symbols two different ways, it's two different axioms.

What you're saying is more or less equivalent to “two C implementations targeting different [architectures / operating systems / whatever] are actually implementations of two different programming languages”.

No, I'm saying the meaning behind statements are different. On some architectures, an int is 16-bit, on others 32-bit.

Anyway, this analogy was pushed too far a long time ago.

Post reply on HN