In a proof or deduction system, there are some axioms and some inference rules. To have a small proof system, axioms are defined for the primitives (for example for negation and implication in propositional logic). Now, we want to have a proof system that proves all provable formulae including the formulae contain non-primitive logical connectors (such as OR in propositional logic). The question is should we add definitions for non-primitives as axioms to the proof system, or we should do something else? In other words, do logicians accept definitions as axioms?
- Anybody can ask a question
- Anybody can answer
- The best answers are voted up and rise to the top
Given a theory $T$, you can enlarge it with definitions in two steps. First you enlarge the alphabet $L(T)$ to a new alphabet $L'$ which will contain the new symbols of constants, functions and relations that you need. Then you enlarge $T$ itself by adding axioms of the following form.
Let $\phi(x_1, \dots, x_n)$ be a formula of $T$ with free variables $x_1, \dots, x_n$ and $\psi$ a new symbol of $n$-ary relation. Then you can add an axiom $$\phi(x_1, \dots, x_n) \leftrightarrow \psi(x_1, \dots, x_n).$$ This axiom "defines the meaning of $\psi$". Similarly you can add new defininig axioms for functions.
The theory $T'$ with language $L'$ that you obtain in this way is called an extension by definitions of $T$. It is not difficult to prove that $T'$ is a conservative extension of $T$; that is, $T$ and $T'$ prove the same formulas of $L$. In this sense one can make precise the fact that definitions do not add nothing new to a theory.
Yes, absolutely you can introduce definitions as axioms. That's what Metamath does:
which defines a formal system with definitions: