Re:Doing Mathematics Differently
by catnaroek on Friday February 26, 2016 @08:59PM
(#11185687)
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.
[ Parent
| on HN ]
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.
Ah, lovely! You just arrived exactly where I was trying to get.
> I'm saying the meaning behind statements are different.
Yes, exactly! And, just like a single C program can have two different meanings under two different implementations, the same axiomatic system can have two different meanings when deducing its consequences (proving theorems) using different rules of inference.