Экзистенциальная реализация

Экзистенциальная реализация

Тип	Правило вывода
Поле	Логика предикатов
Символическое заявление	$\exists xP\left({x}\right)\implies P\left({a}\right)$

В логике предикатов экзистенциальное создание экземпляров (также называемое экзистенциальным устранением ) — это правило вывода , которое гласит, что для данной формулы вида $(\exists x)\phi (x)$, можно сделать вывод $\phi (c)$ для нового постоянного символа c . Правило имеет ограничения: константа c, введенная правилом, должна быть новым термином, который не встречался ранее в доказательстве, а также не должна встречаться в заключении доказательства. Также необходимо, чтобы каждый экземпляр $x$ что связано с $\exists x$ должен быть равномерно заменен на c . Это следует из обозначений $P\left({a}\right)$, но его явное утверждение часто остается за пределами объяснений.

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

$\exists xP\left({x}\right)\implies P\left({a}\right)$

где a — новый постоянный символ, не встречавшийся в доказательстве.

См. также

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