Do P and Q depend on x? Also, see this sticky thread.
Do P and Q depend on x? Also, see this sticky thread.
Hmm, I am not sure I understand "p and q are of type x." In terms of types, I would say, "P and Q are of type X -> Prop" where Prop is the type of propositions. But I understand that P and Q are unary predicates that accept arguments of type X.
A derivation depends on the axioms you have. For example, if you have an axiom (¬∃x. ¬Ax) <-> ∀x. Ax, then you can immediately use it to derive ¬∃x:X. ¬¬(Px ^ Qx). Similarly, if you have an axiom A ^ B <-> ¬(¬A v ¬B), then you can derive ¬∃x:X. ¬(¬Px v ¬Qx). Otherwise, it is significantly more tricky.
Also, do you use Fitch-style natural deduction (also called flag notation) or tree-like natural deduction?
P ^ ¬P is not an axiom since it is contradictory.
I'll describe the derivation in words. Assume . We need to derive a contradiction. Apply existential elimination to get an x and . Use universal elimination with that x on to get . We are going to make two assumptions and show that they are contradictory.
Assume and assume . Then , which contradicts . Therefore, we close and derive . Using disjunction introduction, this implies , which contradicts . Therefore, we close and derive . As before, this implies , which contradicts . Thus we closed both and and derived a contradiction.
Note that I have not used the law of excluded middle . Using it, it may be possible to make the derivation a little clearer. Basically, once you have and , you consider (using disjunction elimination) four cases where either or and either or hold. In each case, it is possible to derive a contradiction using the two premises above. This is similar to constructing a truth table.