5 ms·

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 maki

by plutooo 11y ago

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.

catnaroek 11y ago
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.
- plutooo 11y ago
  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.
  - 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.
- dllthomas 11y ago
  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?
  - catnaroek 11y ago
    A “theorem” is by definition a statement in a mathematical theory that has a proof. In what sense is this true? Well, that depends on what “true” means in your model... :-p
    - js8 11y ago
      I agree with parent comment. At the heart of your disagreement is that you seem to use definition from logic of what axioms are, while your opponents use "definitions" from metamathematics.
  - aangjie 11y ago
    Umm. I've been of the understanding that we never change the inference rules, Can you point to some branch of mathematics that involves a change of inference rules?
    - dllthomas 11y ago
      At my level of understanding, it seems a reasonable characterization of intuitionistic logic to say that it operates with a more restricted set of inference rules. It was the parent who made the stronger claim about differences here, and they speak a bit more to the topic in nearby comments.
  - aangjie 11y ago
    Umm. I've been of the understanding that we never change the inference rules, Can you point to some branch of mathematics that involves a change of inference rules?
- mafribe 11y ago
  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
  - plutooo 11y ago
    Exactly. What are axioms and what are rules of inference ends up being a distinction without a difference.
    - mafribe 11y ago
      I'm not sure I would go that far. There is a difference, but it's not clear quite what it is. For example, it becomes progressively harder to get nice (with cut elimination and finite rule schemata) sequent calculi for richer axiomatic systems. For example I have not come across a nice (in the above sense) sequent style formalisation of ZFC set theory. Have you?
      - plutooo 11y ago
        No, but why is that a problem?
        mafribe 11y ago
        It's an indication, a hint, that rules and axioms are not always completely exchangable.
  - catnaroek 11y ago
    > 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. Yes, but the derivations themselves will change. > 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. Yep. I'm aware of the phenomenon that a single mathematical object of type T (say, infinity-categories) may admit multiple presentations by objects of type T' (say, model categories). But, just because two objects of type T' present the same object of type T (e.g., two Quillen-equivalent categories), it doesn't mean that they are equal in all respects (e.g., the category of simplicial sets is much nicer than the category of topological spaces).

by plutooo 11y ago

catnaroek 11y ago

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.

plutooo 11y ago
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.
- 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.
dllthomas 11y ago
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?
- catnaroek 11y ago
  A “theorem” is by definition a statement in a mathematical theory that has a proof. In what sense is this true? Well, that depends on what “true” means in your model... :-p
  - js8 11y ago
    I agree with parent comment. At the heart of your disagreement is that you seem to use definition from logic of what axioms are, while your opponents use "definitions" from metamathematics.
- aangjie 11y ago
  Umm. I've been of the understanding that we never change the inference rules, Can you point to some branch of mathematics that involves a change of inference rules?
  - dllthomas 11y ago
    At my level of understanding, it seems a reasonable characterization of intuitionistic logic to say that it operates with a more restricted set of inference rules. It was the parent who made the stronger claim about differences here, and they speak a bit more to the topic in nearby comments.
- aangjie 11y ago
  Umm. I've been of the understanding that we never change the inference rules, Can you point to some branch of mathematics that involves a change of inference rules?
mafribe 11y ago
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
- plutooo 11y ago
  Exactly. What are axioms and what are rules of inference ends up being a distinction without a difference.
  - mafribe 11y ago
    I'm not sure I would go that far. There is a difference, but it's not clear quite what it is. For example, it becomes progressively harder to get nice (with cut elimination and finite rule schemata) sequent calculi for richer axiomatic systems. For example I have not come across a nice (in the above sense) sequent style formalisation of ZFC set theory. Have you?
    - plutooo 11y ago
      No, but why is that a problem?
      - mafribe 11y ago
        It's an indication, a hint, that rules and axioms are not always completely exchangable.
- catnaroek 11y ago
  > 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. Yes, but the derivations themselves will change. > 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. Yep. I'm aware of the phenomenon that a single mathematical object of type T (say, infinity-categories) may admit multiple presentations by objects of type T' (say, model categories). But, just because two objects of type T' present the same object of type T (e.g., two Quillen-equivalent categories), it doesn't mean that they are equal in all respects (e.g., the category of simplicial sets is much nicer than the category of topological spaces).