In particular, it allows the elimination of Russell’s -terms and of the usual symbols for quantification.
1 Background, definitions and notation
In a first order theory with equality, whose domain is for example the set of positive integers, an object of the domain can be represented by a name, like "2", or by a complex expression, like "the positive square root of 4", in which case the number 2 is not even explicitly used.
The interesting difference between the two representations consists in the fact that the complex expression makes it possible to refer to an object with a certain property, even in the absence of the object’s name.
The first systematic study of this fundamental logical process was done by Bertrand Russell in Principia Mathematica and in Introduction to mathematical philosophy, where Russell proposed to call descriptions all expressions of the general form
"the object such that ".
In Introduction to mathematical philosophy Russell makes a distinction between definite and indefinite descriptions. These have the general form
"an object such that ".
This distinction did not find much echo in his subsequent logical theory, where the main focus became rather the development of a theory of definite descriptions.
Thus where a name is an arbitrary symbol assigned to an object of the domain, and one then says that the object is the denotation of the name, in contrast a description is a condition which applies to any object of the domain that satisfies it. In a definite description the object is characterized by the fact that a certain predicate is uniquely satisfied by the object.
In Principia Mathematica the notation introduced for the definite description is a functional variable, known as the description operator. It is build by the small Greek letter with as an index, followed by the predicate to which the operator is applied:
It is to such an expression that Russell calls a description.
the interpretation of which is the statement
"there is a unique object which satisfies and also satisfies ".
If the conditions stipulated by the uniqueness formulas are not satisfied, in propositions like for example "the smallest complex number is prime", the description "the smallest complex number" is said to be empty and the proposition in which it occurs is false.
Notice that the interpretation of the formula
is not an explicit definition of the description
If there is a derivation of the uniqueness formulas for then the symbol
is a term, in particular the term representing the unique object that satisfies .
The -operator is subject to the so called -Rule with the following content:
If the uniqueness formulas for have been derived then the description is a term and the formula
can now be derived by means of the following scheme:
The rule of the redenomination of bound variables for quantifiers can be applied to the bound variable of the -operator. Likewise the collision of bound variables, that one has to prevent when using quantifiers, has also to be prevented also with the use of the -operator.
3 Hilbert’s epsilon-axiom
On the face of it it would seem that the introduction of -terms and of the -Rule would allow the derivation of new formulas. But one can prove that if a formula of the first order predicate calculus with equality, with 0-occurences of -terms, is derivable by means of the -operator and the -Rule, then can also be derived without the use of the -operator.
Other than the formal eliminability of the -operator, Hilbert also adopted the introduction of a symbol which secures the eliminability of the -operator.
The basic idea is the following:
the descriptive term
formally represents the statement
"the object which has the property ".
As we have seen above this term can only be formally introduced after the derivation of the uniqueness formulas.
Hilbert proves that these formulas can be dispensed with and the -operator be replaced by his -operator.
The introduction of this operator is to be controlled by conditions that specify:
Which are the well formed formulas in which the operator is going to occur;
How the underlying logic is going to be adjusted;
They give an axiom that defines the use of .
In particular, let us assume that is a formula in which has a free occurrence. We can then build a term of the form
where the occurrence of is now bound.
If a term built with the -operator can be interpreted as a definite description, the term built with can be interpreted as an indefinite description.
So if there is at least a value such that is satisfied, then the term
denotes an object, without further specifications, which satisfies . If there is no such such that
then we let the term denote an arbitrary value. This already implies that the formula
The fundamental axiom is the following:
Axiom : If is a predicate with a free occurrence of , then
4 The axiom of choice
It was already pointed out that the variable of the -term is a bound variable and that the redenomination rule for bound variables can be applied.
The formula to which the -operator is attached as a prefix may contain variables, free or bound by , , or . In that case the formal definition of the -term can not give rise to the collision of bound variables.
To develop the analogy, let us suppose that
Hilbert’s -operator works like such a function, since the term
in the usual interpretation represents a chosen element from .
Thus if we have the following:
is a formula in which are the only free variables, and
A relation which maps every set of elements to at least an element such that
is a function which maps every set of values of the arguments to a unique value .
To sober up the analogy a little, it is to be noticed that Hilbert intended the choice function to have a finitistic meaning and accordingly to perform only a finite number of choices of one element at a time. In contrast the real choice function of the axiom of choice performs an infinite number of simultaneous choices.
5 The elimination of descriptions and quantifiers
We sketch now some of the best known properties of the -operator.
If for a formula it is at all possible to introduce the
The argument is the following:
i) If the -operator can be introduced then one has the term
ii) In the formula (), Hilbert’s axiom, we insert for and the descriptive term for and we obtain the formula
iii) By i) and modus ponens one has then
iv) This shows that if the descriptive term can be introduced then the -term satisfies the same predicate and therefore that
If we start with the -axiom
then by -introduction we obtain
Existential Generalization gives the formula
and by inserting the -term for we get
This shows that
We use as starting formula
The rule of insertion allows the reformulation
The propositional tautology
gives the formula
From predicate calculus we get
iii) Dictum de Omni
The same kind of argument allows the derivation of dictum de omni.
we start with the -axiom
and by the rule of insertion we get
The propositional tautology
gives the formula
But by Part ii) above this is
Double negation gives
|Date of creation||2013-03-22 18:39:18|
|Last modified on||2013-03-22 18:39:18|
|Last modified by||gribskoff (21395)|