Логика первого порядка для доказательства. Управление квантификаторами

Хорошо, у меня есть данное соотношение: если F(x) неверно, то ни один случай не удовлетворяет G(x) и H(y,x). ((∀x ¬F(x)) ⇒¬(∀y G(y) ˄ H(y,x)))

Теперь, могу ли я преобразовать это в: (∀y G(y) ˄ H(y,x))) ⇒ ((∀x F(x)) ????

Если нет, то левая часть, по существу, должна подразумевать: Если F(x) неверно... Ничего не упоминает о квантификаторах «для всех» или «экзистенциальных кванторах». Могу ли я взять отрицание за пределы квантификатора, т. е. представить его как (¬(∀x F(x)), потому что это значительно упрощает работу???


logic prolog quantifiers first-order-logic
person gran_profaci    schedule 26.09.2012    source источник
comment
Правильным местом, чтобы задать этот вопрос, является math.stackexchange.com.   -  person Petr    schedule 26.09.2012

Ответы (1)


arrow_upward
2
arrow_downward

Я не уверен, что это правильное место, но нет, вы не можете. Удаление отрицания изменит квантор. Кроме того, исходная формула может быть не такой, как вы хотите: последний x — свободная переменная.

person NotAUser    schedule 26.09.2012
comment
Ясно, а что, если бы это было утверждение сейчас? (∀x ¬F(x)) ⇒¬(∃ y G(y)) ˄ H(y,x))? Извините, я допустил ошибку раньше... - person gran_profaci; 26.09.2012
comment
Все, что вам нужно здесь, это две основные эквивалентности. Извиняюсь за обозначения: (1) ∀x ¬F = ¬ ∃x F (2) F ⇒ G = ¬ F v G. Ответ вы легко найдете сами :) - person NotAUser; 27.09.2012