Hacker News Reader

Comment by plutooo | Hacker News Reader

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.

View on HN

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.

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.

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 family of propositions of which AC is one and also see why it has a difficult time holding in IPL.

> 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.

Still, "axiom of choice is a theorem in intuitionistic logic" is absolutely true whether or not you accept intuitionistic logic.

But thas is not Mathematics, they call it "metamathematics" for something.

Reply on news.ycombinator.com