Метод $\varepsilon$-подстановок для исчисления предикатов с равенством

Метод $\varepsilon$-подстановок работает в языке, введенном Гильбертом и использованном позднее разными авторами, включая Бурбаки. Главная предикатная связка этого языка – эпсилон-символ $\varepsilon xF[x]$, который читается "некоторый $x$, удовлетворяющий условию $F$". В арифметических контекстах он часто интерпретируется как "наименьшее натуральное число $x$, удовлетворяющее условию $F$". Кванторы существования и всеобщности определяются через $\varepsilon$. В работе определяются $\varepsilon$-подстановки “снизу” для исчисления предикатов и его расширений равенством и схемой экстенсиональности, доказывается сходимость последовательности $\varepsilon$-подстановок и выведены соответствующие теоремы эрбрановского типа. В действительности установлена сильная сходимость: любая последовательность редукций (а не только последовательность со специальными свойствами) сходится. Библ. – 18 назв.