Логическое доказательство предикатов решить

Предоставьте доказательство следующего, используя FOL в forallx

Используйте систему естественного вывода и стратегии доказательства в forallx , чтобы получить формальное доказательство следующего. Пожалуйста, предоставьте фотографию вашего доказательства.

∃xFx ∧ ∀yGy ∴ ∃x(Fx ∧ Gx)

Что вы пробовали? Какие правила, по вашему мнению, следует использовать?
Я не специалист по системе доказательств forallx , но в рамках «стандартной» естественной дедукции доказательство представляет собой очень простое «упражнение» в применении правил квантификаторов.
Я не уверен, следует ли работать вперед или назад, чтобы сделать вывод.
Вы можете начать с упрощения Посылки.
Добро пожаловать в философию SE! Спасибо за ваш вклад. Пожалуйста, найдите минутку, чтобы совершить экскурсию или найти помощь . Вы можете выполнить поиск здесь или получить дополнительные разъяснения на мета-сайте . Не забывайте, что когда кто-то ответил на ваш вопрос, вы можете щелкнуть стрелку, чтобы вознаградить автора, и галочку, чтобы выбрать лучший ответ.
Этот вопрос касается того, понимаете ли вы правила исключения квантификатора существования. Подумайте об этом так: как бы вы использовали свои правила доказательства, чтобы выбрать конкретный постоянный термин «с», такой, что «F (с)»? Затем, когда у вас есть это «с», что еще вы можете с ним сделать, и что это может вам сказать?

Ответы (2)

Я не уверен, следует ли работать вперед или назад, чтобы сделать вывод.

Почему не оба? Вы знаете, с чего вам нужно начать и куда вы хотите пойти.

Ваша предпосылка представляет собой соединение экзистенциального и универсального. Обратитесь к правилам исключения союзов, универсального исключения и экзистенциального исключения. Посмотрите, с чем это начало дает вам возможность работать.

Ваш вывод есть экзистенциал конъюнкции. Обратитесь к Правилам конъюнктивного введения и Экзистенциального введения. Найдите то, что вам нужно, чтобы достичь конечной цели.

Соедините их вместе.

Предположим, что ∃xFx ∧ ∀yGy, затем докажем ∃x(Fx ∧ Gx) на основе этого предположения.

Используйте устранение конъюнкции, чтобы вывести ∃xFx из вашего предположения. Затем приведите переменную x к константе, скажем, a.* Результатом будет Fa.

Используйте исключение конъюнкции, чтобы получить ∀yGy из вашего исходного предположения. Исходя из этого, вы можете преобразовать переменную y в любую константу, скажем, a.** В результате получится Ga.

Используйте введение союзов, чтобы объединить Fa и Ga, в результате чего Fa ∧ Ga.

Используйте экзистенциальное обобщение с переменной x, заменяющей каждое вхождение a. Результатом является ∃x(Fx ∧ Gx).

*Константа уже не может быть использована в доказательстве. Это потому, что ∃ относится к чему-то в домене, но мы точно не знаем, к чему. **Универсальные значения применяются ко всему в домене, а не только к чему-то. Это означает, что мы можем выбрать экземпляр y для константы a.

Логическое доказательство предикатов решить
СпросиСетьПолитика конфиденциальности1y, 0v