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

В логика предикатов, экзистенциальная реализация (также называемый экзистенциальное устранение)^[1][2][3] это правило вывода который говорит, что, учитывая формулу вида ${\displaystyle (\exists x)\phi (x)}$, можно сделать вывод ${\displaystyle \phi (c)}$ для нового постоянного символа c. Правило имеет ограничения: постоянная c вводимый правилом должен быть новый термин, который не встречался ранее в доказательстве, и он также не должен встречаться в заключении доказательства.

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

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

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

Смотрите также

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

Рекомендации

1. Херли, Патрик. Краткое введение в логику. Wadsworth Pub Co, 2008 год.
2. Копи и Коэн
3. Мур и Паркер