Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
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
up vote 10 down vote accepted

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.

share|cite|improve this answer

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

See also

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 .

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.