0
$\begingroup$

I have to give a natural deduction proof of the statement:
$$ \emptyset \;\; \vdash \;\; \forall x \exists y \forall z \exists w \;\; (Q(x, y) \lor \lnot Q(w, z)) $$

This is a valid formula as per Tree Proof Generator.

The rules we can use include intro- of the quantifiers, tautology ($F \lor \lnot F$), etc.

I'm unable to complete the proof. If I start with tautology to get: $\hspace{40pt}(Q(x, z) \lor \lnot Q(x, z))$
I can arrive till: $\hspace{205pt}\forall z \exists w \;\; (Q(x, z) \lor \lnot Q(w, z))$
using existential intro and universal intro.
However an existential intro in the next step won't be possible because z is now no longer free to be replaced.

How to do this?

$\endgroup$
1
  • 1
    $\begingroup$ @MauroALLEGRANZA The negation of the statement leads to contradiction (as per some online proof checkers). So this must be valid under all models. $\endgroup$
    – whoisit
    Feb 21 at 10:06

0

Reset to default

You must log in to answer this question.