(∀x(s(x) → ¬q(x)) ∧ ∀x((¬p(x) ∧ q(x)) → s(x))) → (∃x(p(x) ∨ q(x)) → ∃xp(x))

Question

Can someone please help me solve this problem in predicate logics? I've been trying to take the antecedence and so I can conclude something but I didn't get anything...

Any kind of help is appreciated! Thank you in advance!

Answer 1

I've been trying to take the antecedence and so I can conclude something but I didn't get anything...

Yes. Do that thing (a conditional proof).

Just to check: the antecedent is $\forall x~(s(x) \to\lnot q(x))\land\forall x~((\lnot p(x)\land q(x))\to s(x))$ and the consequent is $\exists x~(p(x)\to q(x)) \to \exists x~p(x)$

That antecedent is a conjunction, you use your rule for ... simplification or conjunction elimination ... in whatever system you are using.

That consequent is another conditional statement you need to derive, so do another conditional subproof.

$\def\fitch#1#2{~~~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{}{\fitch{\forall x~(s(x) \to\lnot q(x))\land\forall x~((\lnot p(x)\land q(x))\to s(x))}{\forall x~(s(x)\to\lnot q(x))\\\forall x~((\lnot p(x)\land q(x))\to s(x))\\\fitch{\exists x~(p(x)\lor q(x))}{~~\vdots\\\exists x~p(x)}\\\exists x~(p(x)\to q(x)) \to \exists x~p(x)}\\(\forall x~(s(x)\to\lnot q(x))\land \forall x~((\lnot p(x)\land q(x))\to s(x)))\to (\exists x~(p(x)\lor q(x))\to \exists x~p(x))}$

Now use your rules for existential, universal, disjunction, and negation.