I found the following exercise in the Discrete Mathematics and Functional Programming book by Thomas VanDrunen.
3.14.4
(a) $\forall x \in A, P(x) \land \lnot Q(x)$
(b) $\forall x \in A, x \in B$
(c) $\forall x \in B, \lnot Q(x) \implies R(x)$
(d) $\therefore \forall x \in A, R(x)$
These are the steps I've used to verify the argument.
Suppose $a \in A$
(i) $P(a) \land \lnot Q(a) $
By supposition, (a), and Universal Instantiation.
(ii) $\lnot Q(a)$
Using (i) and Specialization.
(iii) $a \in B$
Using our initial supposition, (b), and Universal Instantiation.
(iv) $R(a)$
By (c), (iii), (ii), and Universal Modus Tollens.
(v) $\therefore \forall x \in A, R(x)$
By supposition, (iv), and Universal Generalization.
My questions are:
- Is my verification OK? Or am I missing one step?
- Since I will continue tackling the rest of the exercises, I am wondering if is there a Computer System aiding with the task of verifying these arguments? Sort of a Calculator, like when you perform an Arithmetic Addition and you want to verify if you did it well. I haven't played with Coq, and these last days I've been reading about Agda, but I am not sure if those can be used for the task I am describing here.
Thanks!
--
Caleb