epsilon calculus
   HOME

TheInfoList



OR:

Hilbert's epsilon calculus is an extension of a
formal language In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules. The alphabet of a formal language consists of symb ...
by the epsilon operator, where the epsilon operator substitutes for quantifiers in that language as a method leading to a proof of consistency for the extended formal language. The ''epsilon operator'' and ''epsilon substitution method'' are typically applied to a first-order predicate calculus, followed by a showing of consistency. The epsilon-extended calculus is further extended and generalized to cover those mathematical objects, classes, and categories for which there is a desire to show consistency, building on previously-shown consistency at earlier levels.


Epsilon operator


Hilbert notation

For any formal language ''L'', extend ''L'' by adding the epsilon operator to redefine quantification: * (\exists x) A(x)\ \equiv \ A(\epsilon x\ A) * (\forall x) A(x)\ \equiv \ A(\epsilon x\ (\neg A)) The intended interpretation of ϵ''x'' ''A'' is ''some x'' that satisfies ''A'', if it exists. In other words, ϵ''x'' ''A'' returns some term ''t'' such that ''A''(''t'') is true, otherwise it returns some default or arbitrary term. If more than one term can satisfy ''A'', then any one of these terms (which make ''A'' true) can be chosen, non-deterministically. Equality is required to be defined under ''L'', and the only rules required for ''L'' extended by the epsilon operator are
modus ponens In propositional logic, ''modus ponens'' (; MP), also known as ''modus ponendo ponens'' (Latin for "method of putting by placing") or implication elimination or affirming the antecedent, is a deductive argument form and rule of inference. ...
and the substitution of ''A''(''t'') to replace ''A''(''x'') for any term ''t''.


Bourbaki notation

In tau-square notation from N. Bourbaki's ''Theory of Sets'', the quantifiers are defined as follows: * (\exists x) A(x)\ \equiv \ (\tau_x(A), x)A * (\forall x) A(x)\ \equiv \ \neg (\tau_x(\neg A), x)\neg A\ \equiv \ (\tau_x(\neg A), x)A where ''A'' is a relation in ''L'', ''x'' is a variable, and \tau_x(A) juxtaposes a \tau at the front of ''A'', replaces all instances of ''x'' with \square, and links them back to \tau. Then let ''Y'' be an assembly, ''(Y, x)A'' denotes the replacement of all variables ''x'' in ''A'' with ''Y''. This notation is equivalent to the Hilbert notation and is read the same. It is used by Bourbaki to define cardinal assignment since they do not use the axiom of replacement. Defining quantifiers in this way leads to great inefficiencies. For instance, the expansion of Bourbaki's original definition of the number one, using this notation, has length approximately 4.5 × 1012, and for a later edition of Bourbaki that combined this notation with the Kuratowski definition of
ordered pair In mathematics, an ordered pair (''a'', ''b'') is a pair of objects. The order in which the objects appear in the pair is significant: the ordered pair (''a'', ''b'') is different from the ordered pair (''b'', ''a'') unless ''a'' = ''b''. (In con ...
s, this number grows to approximately 2.4 × 1054.


Modern approaches

Hilbert's program for mathematics was to justify those
formal system A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A form ...
s as consistent in relation to constructive or semi-constructive systems. While Gödel's results on incompleteness mooted Hilbert's Program to a great extent, modern researchers find the epsilon calculus to provide alternatives for approaching proofs of systemic consistency as described in the epsilon substitution method.


Epsilon substitution method

A theory to be checked for consistency is first embedded in an appropriate epsilon calculus. Second, a process is developed for re-writing quantified theorems to be expressed in terms of epsilon operations via the epsilon substitution method. Finally, the process must be shown to normalize the re-writing process, so that the re-written theorems satisfy the axioms of the theory.Stanford, more recent developments section


Notes


References

* * * *{{cite book , last = Bourbaki , first = N. , title = Theory of Sets , location = Berlin , publisher = Springer-Verlag , isbn = 3-540-22525-0 Systems of formal logic Proof theory