Экзистенциальное создание

В логике предикатов, экзистенциальное воплощение (также называемое экзистенциальное исключение ) - это правило вывода, которое гласит, что для формулы вида $(\exists \; x)\; \varphi \; (x)\; \{\; \backslash \; displaystyle\; (\backslash \; exists\; x)\; \backslash \; phi\; (x)\}$, можно вывести $\varphi \; (c)\; \{\backslash \; displaystyle\; \backslash \; phi\; (c)\}$для нового постоянного символа c. Правило имеет ограничения, согласно которым константа c, введенная правилом, должна быть новым членом, который не встречался ранее в доказательстве, а также не должен встречаться в заключении доказательства.

В одном формальном обозначении правило может быть обозначено как

$\exists \; x\; P\; (x)\; ⟹\; P\; (a)\; \{\backslash \; displaystyle\; \backslash \; exists\; xP\; \backslash \; left\; (\{x\}\; \backslash \; right)\; \backslash \; подразумевает\; P\; \backslash \; left\; (\{\backslash \; mathbf\; \{a\}\}\; \backslash \; right)\}$

где a - новый постоянный символ, который не фигурировал в доказательстве.

• Экзистенциальная ошибка
• Универсальная реализация
• Список правил вывода