$((\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
$((\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
Copyright © 2021 JogjaFile Inc.
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.