Epsilon calculus

For any formal language ${\displaystyle L}$, extend ${\displaystyle L}$ by adding the epsilon operator to redefine quantification:

• ${\displaystyle (\exists x)A(x)\ \equiv \ A(\epsilon x\ A)}$
• ${\displaystyle (\forall x)A(x)\ \equiv \ \neg \exists x\neg A(x)\leftrightarrow \neg {\bigl (}\neg A(\epsilon x\ \neg A){\bigr )}\leftrightarrow A{\bigl (}\epsilon x\ (\neg A){\bigr )}}$

The intended interpretation of ${\displaystyle \epsilon x\ A}$ is some${\displaystyle x}$ that satisfies ${\displaystyle A}$, if it exists. In other words, ${\displaystyle \epsilon x\ A}$ returns some term${\displaystyle t}$ such that ${\displaystyle A(t)}$ is true, otherwise it returns some default or arbitrary term. If more than one term can satisfy ${\displaystyle A}$, then any one of these terms (which make ${\displaystyle A}$ true) can be chosen, non-deterministically. Equality is required to be defined under ${\displaystyle L}$, and the only rules required for ${\displaystyle L}$ extended by the epsilon operator are modus ponens and the substitution of ${\displaystyle A(t)}$ to replace ${\displaystyle A(x)}$ for any term ${\displaystyle t}$.^[2]

In tau-square notation from N. Bourbaki'sTheory of Sets, the quantifiers are defined as follows:

• ${\displaystyle (\exists x)A(x)\ \equiv \ {\bigl (}\tau _{x}(A)|x{\bigr )}A}$
• ${\displaystyle (\forall x)A(x)\ \equiv \ \neg {\bigl (}\tau _{x}(\neg A)|x{\bigr )}\neg A\ \equiv \ {\bigl (}\tau _{x}(\neg A)|x{\bigr )}A}$

where ${\displaystyle A}$ is a relation in ${\displaystyle L}$, ${\displaystyle x}$ is a variable, and ${\displaystyle \tau _{x}(A)}$ juxtaposes a ${\displaystyle \tau }$ at the front of ${\displaystyle A}$, replaces all instances of ${\displaystyle x}$ with ${\displaystyle \square }$, and links them back to ${\displaystyle \tau }$. Then let ${\displaystyle Y}$ be an assembly, ${\displaystyle (Y|x)A}$ denotes the replacement of all variables ${\displaystyle x}$ in ${\displaystyle A}$ with ${\displaystyle 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 × 10¹², 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 × 10⁵⁴.^[3]

تُدمج النظرية المراد التحقق من اتساقها أولاً في حساب إبسيلون مناسب. ثانياً، تُطوَّر عملية لإعادة صياغة النظريات الكمية للتعبير عنها بدلالة عمليات إبسيلون باستخدام طريقة استبدال إبسيلون. أخيراً، يجب إثبات أن هذه العملية تُعيد صياغة النظرية بشكل معياري، بحيث تُحقق النظريات المُعاد صياغتها بديهيات النظرية. ^{[ 4 ]}