Proving formally

34 Views Asked by At

$((\exists x : X.P) \Rightarrow (\forall x: X.Q)) \vdash (\forall x: X. PvQ) \Rightarrow((\forall x: X.P) \vee(\forall x: X. Q)$

exist stands for the existential quantifier all stands for for-all quantifier in discrete maths

1

There are 1 best solutions below

0
On

Assuming $((\exists x.P) \implies (\forall x.Q))$ and $(\forall x. P\vee Q)$, we want to deduce the last part. It suffices to write the following chain of deduction.

$\begin{array}{l} (\forall x. P\vee Q)\text{ (second axiom)}\\ (\forall x. Q)\vee (\exists x.P)\text{ (case disjunction)}\\ (\forall x. Q) \vee (\forall x.Q)\text{ (using first axiom)}\\ (\forall x. Q)\\ (\forall x. P)\vee(\forall x. Q)\text{ ($\vee$-introduction).} \end{array}$

So you can in fact prove something stronger, we always have $(\forall x. Q)$ if the assumptions are verified.