Epsilon calculus
In logic,
Epsilon operator
Hilbert notation
For any formal language L, extend L by adding the epsilon operator to redefine quantification:
The intended interpretation of ϵx A is some x that satisfies A, if it exists. In other words, ϵx A returns some
Bourbaki notation
In tau-square notation from N. Bourbaki's Theory of Sets, the quantifiers are defined as follows:
where A is a relation in L, x is a variable, and juxtaposes a at the front of A, replaces all instances of x with , and links them back to . 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
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 pairs, this number grows to approximately 2.4 × 1054.[3]
Modern approaches
Hilbert's program for mathematics was to justify those formal systems 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.[4]
Notes
References
- "Epsilon Calculi". Internet Encyclopedia of Philosophy.
- Moser, Georg; OCLC 108629234.
- Avigad, Jeremy; Zach, Richard (November 27, 2013). "The epsilon calculus". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.
- Bourbaki, N. Theory of Sets. Berlin: Springer-Verlag. ISBN 3-540-22525-0.