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.
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 system, it would indeed be very weird (though not a priori impossible) if “a = 0” didn't imply “a = 0”. But I have no problem imagining a formal system where “a = 0” isn't expressible (e.g., because equality is inexpressible), or implication isn't expressible (e.g., geometric logic), or implication has strange properties to someone only familiar with the classical and/or intuitionistic interpretation of “implication” (e.g., linear logic).
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.
(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.
Axioms and rules of inference are fundamentally different:
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
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).
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?
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.
Anyway, this analogy was pushed too far a long time ago.
> 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.
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.
Naïvely encoded in Martin-Löf type theory, that is.
This is not correct. There is no such thing as absolute truth. Something can only be true within a set of previously agreed constraints and rules. For example, I can simply imagine a scenario where a=0 implies a=0 is considered to be false, because I define it to be so.
Isn't that an absolute truth?
No, not at all. Axioms are better thought of as universally accepted truths which everything else depends on. https://en.wikipedia.org/wiki/Logical_atomism
It's obvious when applying math to real world. If you're talking about objects on Earth surface, for example, at first Euclid's geometry will get you good results, because objects you're working with can be assumed to fulfill it's axioms. However, when your scale gets bigger, you'll have apply a more complicated geometry apparatus.
Easiest analogy about axioms is interface in software engineering: you don't care what the object really is, but as long as it shows certain properties, you can prove theorems about it. Which will be true for any objects with these properties, and as true as exactly these properties are fulfilled by the real life object.