Естественная дедукция для предикатной логики

Question

Я долгое время сталкивался с определенной проблемой логики предикатов (используя Coq). Я уже решил 30-40 задач логики предикатов, но с этим я просто не могу понять.

В этом заключается проблема: ~ все x, (P (x)/(Q (x) -> T (x))) -> ~ все x, T (x).

Or in box form

Может кто-нибудь прислать мне в правильном направлении? Благодаря!

Edit:

Это код Кока для задачи:

Variables P Q T : D -> Prop. 

Theorem pred_015 : ~all x, (P(x) \/ (Q(x) -> T(x))) -> ~all x, T(x). 
Proof. 
imp_i H. 



Qed. 

Answer 1

Он смотрит на меня, как ваши использует какую-то очень старую версию Coq. После добавления отсутствующего объявления для D и замены all на forall, мы получаем заявление, которое не выглядит доказуемым. Однако, если бы у меня был набор круглых скобок, я получаю цель, которая теперь доказуема. Смотрите следующий код:

Variable D : Set. 
Variables P Q T : D -> Prop. 

Theorem pred_015 : (~forall x, (P(x) \/ (Q(x) -> T(x)))) -> ~forall x, T(x). 
Proof. 

Теперь, я не думаю, что я должен дать решение этого здесь, в общественных местах, но это довольно легко, если вы помните, что ~H определяется как H -> False.