Definitions de-mystified.
(These criteria, rules and discussion are adapted from P. Suppes, 'Introduction
to Logic', Chapter 8, "Theory of Definition", although essentially
the same rules appear in various standard logic texts).
Criteria for the proper definition of new non-logical symbols from the primitive
symbols of a first order language and theory..
Criterion of Eliminability. A formula S introducing a new symbol into a theory
T of a first order language L satisfies the criterion of eliminability if
and only if whenever F1 is a formula in which the new symbol occurs, then
there is a formula F2 in which the new symbol does not occur such that 'S=>
(F1<=>F2))' is derivable from the axioms of T together with any preceding
definitions of the theory, if any.
Discussion: proper definitions are not to function as new axioms in logical
inference.They are instead to serve as notational conveniences, which are
always eliminable from the axioms of the theory.
Criterion of Non-creativity. A formula S introducing a new symbol into a theory
T of a first order language L satisfies the criterion of non-creativity is
and only if tthere is no formula F in which the new symbol does not occur
such that ''S => T' is derivable from the axioms and preceding definitions
(if they exist) of the theory T, but F is not so derivable.
Discussion: proper definitions must not permit the derivation of new content
in a theory. Consider the theory consisting of the one axiom (expressing associativity
of the operation '*') 'X*(Y*Z) =(X*Y)*Z'. A 'definition' introducing a new
constant 'e' such as 'X*e=X', would permit the derivability of this new formula,
previously underivable from the associativity axiom: '(exists X (forall Y(
X*Y=X)))'. Thus such a 'definition' would be creative and improper, as it
would function as a new axiom..
Rules for defining relation symbols:
An equivalence D introducing a new n-place relation symbol P to the first
order language L and theory T in L is a proper definition if and only if D
is of the form, P(V1,..., Vn) <=> S, where 'P' is a to be an atomic
symbol of L, and the following restriction apply to the symbolic formula S:
1) V1,...,Vn are distinct variables,
2) S has no free variables other than V1,...,Vn,
3) S is a formula of L in which the only non-logical constants are primitive
symbols of T (and, hence, of L) or previously defined symbols of T.
Discussion:
Restriction (1) prevents definitions like 'X <= X <=> (X = X or X
< X)'. This formula does not define the binary relation, X<=Y, in the
usual sense, as might carelessly be thought, since only one free variable
appears in the defiendum. .We could, though, according to our restriction,
legally define the trivial unary property 'U(X)', by 'U(X) <=> (X=X
or X<X)'.
Restriction (2) prevents definition like 'R(X) <=> (X + Y=0)', where
a variable 'Y' appears in the defiendum but not the defniens. If such were
permitted, we could derive 'if there is a Y such that X + Y = 0, then for
all X, X + Y = 0'. (Exercise for the reader)
Note that restriction (2) does not prohibit variables from appearing unbound
in the definiendum but not the definiens. However, such appearances are trivial
and eliminable. (Exercise for the reader).
Restriction (3) prevents definitions such as 'R(X) <=> R(X)', and pairs
of defintions like, "P(X) <=> not Q(X)' and 'Q(X) <=> not
P(X)'. In such cases the symbol(s) being introduced would not be eliminable.
Rules for defining operation symbols:
Remark: in introducing new function symbols (N.B. including the special case
of 0 place function symbols, a.k.a non-logical constants), a new restriction
is to be added to the 3 given above for the introduction of new relation symbols.:
An equivalence D introducing a new n-place operation symbol O is a proper
definition in a first order language L and theory T if and only if, D is of
the form,
O(V1,...Vn) =W <=> S,
and the following restrictions are satisfied:
1) V1,...,Vn are distinct variables,
2) S has no free variables other than V1,...,Vn,
3) S is a formula of L in which the only non-logical constants are primitive
symbols or previously defined symbols of T,
4) the formula,' (exists W ( S(W) and (forall Y (S(Y) <=> Y=W))))',
is derivable in T.
Discussion: restriction (4) prevents the introduction of 'pseudo operations',
like 'X*Y=Z <=> (X <Z and Y<Z)'. An example of a violoation of
this principle: a contradiction would be derivable from the theory of arithmetic
were such a definition permitted (Exercise for the reader).
It can be shown, although it will not be shown here, that definitions of relation
or function symbols satisfying the rules for proper definitions also satisfy
the criteria of non-creativity and eliminability, and vice versa.
Rules for the introduction of operation symbols via statements of identity.
"It is reasonable to ask why equivalences are ever used to define individual
constants. The answer is very simple: identities alone are not adequate for
the job" (in the absence of a definite description operator for the first
order language). P. Suppes, 'IL', p 161.
Rule for defining operation symbols. An identity D introducing a new n-place
operation symbol O is a proper definition in a theory T in a first order language
if and only if D is of the form O(V1,... ,Vn) =t, and the following restrictions
are satisfied:
1) V1,.. Vn are distinct variables,
2) the term t has no free variables other than V1,...,Vn,
3) the only non-logical constants in the term t are primitive symbols and
previously defined symbols of the theory.
Remark: when identities are used to define operation symbols, no justifying
theorem is need to guarantee that the symbol t is well-defined, since the
formula, '(exists W ( W=t and (forall Y (W=t <=> Y=t))))', is a truth
of logic.
Axiom-free definitions.
There is a form of definition for introducing new function symbols which does not require the use of axioms to justify it.
An equivalence D introducing a new n-place operation symbol O is a proper
axiom-free definition in a first order language L and theory T if and only
if, D is of the form,
O(V1,...Vn) =W <=> (forall Z ( Z=W <=> S(V1,...,Vn,Z))) or (not
(exists V (forall X ( X = V ,=> S(V1,...,Vn, X) and W=,
and the following restrictions are satisfied:
1) V1,...,Vn are distinct variables,
2) S has no free variables other than V1,...,Vn,
3) S is a formula of L in which the only non-logical constants are primitive
symbols or previously defined symbols of T,
4) the formula,' (exists W ( S(W) and (forall Y (S(Y) <=> Y=W))))',
is derivable in T.
Conditional definitions considered.
It is customary practice in mathematics to use conditional definitions.