5 ms·
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
by 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 agoExactly. What are axioms and what are rules of inference ends up being a distinction without a difference.
- mafribe 11y agoI'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?
- 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).