# Can we define definitions as axioms in logic?

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?

-
Lots of definitions can be considered just as notation - it's things like recursive definitions or inductively defined sets that you need a schema for. –  anon Sep 11 '10 at 13:02

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:

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