Can we define definitions as axioms in logic?

Question

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?

Answer 1

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.

Answer 2

Yes, absolutely you can introduce definitions as axioms. That's what Metamath does:

http://us.metamath.org/mpegif/mmset.html#definitions

See also

http://www.hss.cmu.edu/philosophy/techreports/181_Avigad.pdf

which defines a formal system with definitions:

We extend the foundational framework in two ways. First, we allow for explicit definitions of new predicates and functions on the universe of sets. And, second, we allow function symbols to denote functions that are only partially de- fined, using a logic of partial terms. We call the resulting formal system DZFC .