In logic, Hilbert's epsilon calculus is an extension of a formal language 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 demonstration 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.[1]
For any formal language L, extend L by adding the epsilon operator to redefine quantification:
The intended interpretation of ϵxA is some x that satisfies A, if it exists. In other words, ϵxA returns some termt 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 and the substitution of A(t) to replace A(x) for any term t.[2]
Bourbaki notationedit
In tau-square notation from N. Bourbaki'sTheory 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 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 pairs, this number grows to approximately 2.4 × 1054.[3]
Modern approachesedit
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 methodedit
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]
Bourbaki, N. Theory of Sets. Berlin: Springer-Verlag. ISBN3-540-22525-0.
December 15, 2023
epsilon, calculus, logic, hilbert, epsilon, calculus, extension, formal, language, epsilon, operator, where, epsilon, operator, substitutes, quantifiers, that, language, method, leading, proof, consistency, extended, formal, language, epsilon, operator, epsilo. In logic Hilbert s epsilon calculus is an extension of a formal language 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 demonstration 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 1 Contents 1 Epsilon operator 1 1 Hilbert notation 1 2 Bourbaki notation 2 Modern approaches 2 1 Epsilon substitution method 3 Notes 4 ReferencesEpsilon operator editHilbert notation edit For any formal language L extend L by adding the epsilon operator to redefine quantification x A x A ϵ x A displaystyle exists x A x equiv A epsilon x A nbsp x A x A ϵ x A displaystyle forall x A x equiv A epsilon x neg A nbsp 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 and the substitution of A t to replace A x for any term t 2 Bourbaki notation edit In tau square notation from N Bourbaki s Theory of Sets the quantifiers are defined as follows x A x t x A x A displaystyle exists x A x equiv tau x A x A nbsp x A x t x A x A t x A x A displaystyle forall x A x equiv neg tau x neg A x neg A equiv tau x neg A x A nbsp where A is a relation in L x is a variable and t x A displaystyle tau x A nbsp juxtaposes a t displaystyle tau nbsp at the front of A replaces all instances of x with displaystyle square nbsp and links them back to t displaystyle tau nbsp 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 pairs this number grows to approximately 2 4 1054 3 Modern approaches editHilbert s program for mathematics was to justify those formal systems as consistent in relation to constructive or semi constructive systems While Godel 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 edit 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 edit Stanford overview section Stanford the epsilon calculus section Mathias A R D 2002 A term of length 4 523 659 424 929 PDF Synthese 133 1 2 75 86 doi 10 1023 A 1020827725055 MR 1950044 Stanford more recent developments sectionReferences edit Epsilon Calculi Internet Encyclopedia of Philosophy Moser Georg Richard Zach The Epsilon Calculus Tutorial Berlin Springer Verlag 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 Retrieved from https en wikipedia org w index php title Epsilon calculus amp oldid 1172352309, wikipedia, wiki, book, books, library,
