CODEWITHSUNDEEP
logicpredicatecoq
Boris van Linschoten
Boris van Linschoten

Reputation: 21

Natural deduction for predicate logic

I've been stuck on a particular predicate logic problem (using Coq) for a long time. I've solved 30-40 predicate logic problems already but with this one I just can't figure it out.

This is the problem: ~all x, (P(x) / (Q(x) -> T(x))) -> ~all x, T(x).

Or in box form

Can anyone send me in the right direction? Thanks!

Edit:

This is the coq code for the problem:

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.

Upvotes: 1

Views: 224

Answers (1)

Zimm i48
Zimm i48

Reputation: 3081

It looks to me like your are using some very old version of Coq. After adding a missing declaration for D, and replacing all with forall, we get a statement that does not look provable. However, if I had a set of parentheses, I get a goal that is now provable. See the following code:

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.

Now, I don't think I should be giving the solution to this here, in public, but it's quite easy if you remember that ~H is defined as H -> False.

Upvotes: 2

Related Questions