5 ms·

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 t

• catnaroek 11y ago
  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.
  • plutooo 11y ago
    But I'm saying if you evaluate the axiom symbols two different ways, it's two different axioms.
    • catnaroek 11y ago
      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”.
      • plutooo 11y ago
        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.
        • catnaroek 11y 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.
• tel 11y ago
  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.
  • catnaroek 11y ago
    > 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.
  • plutooo 11y ago
    Still, "axiom of choice is a theorem in intuitionistic logic" is absolutely true whether or not you accept intuitionistic logic.
    • pfortuny 11y ago
      But thas is not Mathematics, they call it "metamathematics" for something.