Formal proof for a syllogism Let $p(x),q(x),r(x)$ unary predicates in some language. Consider the deduction
$$\exists x (p(x) \land q(x) ), \forall x (q(x) \rightarrow r(x)) \vdash\exists x (p(x) \land r(x))$$
I want to find a proof for this  using only Modus Ponens and introduction of universal quantifier. Algebraically, consider the monadic logic $(A,\exists, P) $, where $P$ is thought as the filter of provable propositions. Using the definition of filter and its closure under the universal quantifier, I want to show that $\exists x (p(x) \land q(x) ) \in P$ and $ \forall x (q(x) \rightarrow r(x)) \in P$ imply $\exists x (p(x) \land r(x)) \in P$.
I tried using the tautology
$$(p(x) \land q(x) )\land(q(x) \rightarrow r(x)) \rightarrow  (p(x) \land r(x)),$$
followed by introducing $\forall$, but it gets me nowhere. I can also use $A(x) \implies \exists x A(x)$ and MP to introduce an existential quantifier, hence obtaining $\exists x (p(x) \land r(x))$  on the conclusion, but I don't know how to deal with the premises this way.
I might me missing something simple here, any help is appreciated.
 A: I'll clear things up in this answer, since the question might be ambiguous.
A monadic logic is a triple $(A,P,\forall)$, where $A$ is a boolean algebra, $P$ is a filter, and $\forall:A \to A$ is an endomorphism such that for all $x,y \in A$:

*

*$\forall(P) = P$.

*$\forall(x) \leq x$ (where "$\leq$" is the lattice order in $A$).

*$\forall(x\land y)= \forall(x) \land \forall(y)$.

*$\forall  (\forall(x)) = \forall(x)$.

*$\forall(\neg \forall(x)) = \neg(\forall(x)).$

*$\forall(x \lor \forall(y) ) = \forall(x) \lor \forall(y)$
We can define in a dual manner the ideal $I = \{\neg p , p \in P \}$, and the mapping $\exists:A \to A$ given by $\exists(x) =  \neg \forall \neg(x)$. The triple $(A,I,\exists)$ can also be considered as a monadic logic. The axioms for this logic are

*

*$\exists(I) = I$.

*$\exists(x) \geq x$.

*$\exists(x\lor y)= \exists(x) \lor \exists(y)$.

*$\exists  (\exists(x)) = \exists(x)$.

*$\exists(\neg \exists(x)) = \neg(\exists(x)).$

*$\exists(x \land \exists(y) ) = \exists(x) \land \exists(y)$
We are required to prove that $\exists(p\land q) \in P$ and $\forall(q \rightarrow r) \in P$ imply $\exists(p\land r) \in P$.
(I) We show first that $\forall$ is an increasing function. Let $x,y \in A$ and suppose first that $\forall x \leq y$. Then $\forall x \land y = \forall x$, hence $$\forall (\forall x \land y ) = \forall x \land \forall y = \forall \forall x = \forall x,$$ which proves $\forall x \leq \forall y$. Then if $x \leq y$, we have that $\forall x \leq x \leq y$ implies $\forall x \leq \forall y$ by the preceding argument. Applying this to the quotient logic $A/P$ gives: If $\forall(x \rightarrow y) \in P$, then $\forall x \rightarrow \forall y \in P$.
(II) Now, we show that $\forall(x \rightarrow y) \in P$ implies  $(\exists x \rightarrow \exists y) \in P$.
$$
\begin{aligned}
\forall(x \rightarrow y) &\leq (x \rightarrow y) \\ &= (\neg y \rightarrow \neg x) \\  
\end{aligned}
$$
So $\forall (\neg y \rightarrow \neg x) \in P$, and by monotonicity, $\forall \neg y \rightarrow \forall \neg x \in P$. Applying contraposition yields the result.
(III) Note also that for all $x,y \in A$,
$$\exists x \land \forall y = \exists x \land \neg \exists \neg y = \exists(x \land \neg \exists \neg y) = \exists (x \land \forall y),$$
and moreover $$\forall y \leq y \implies x \land \forall y \leq x \land  y \implies \exists(x \land \forall y) \leq \exists(x \land  y), $$
since $\exists$ is also increasing. We conclude the inequality
$$\exists(x) \land \forall(y) \leq \exists( x \land y).$$
Proof: Note that
$$
\begin{aligned}
1&= (p\land q) \land (q \rightarrow r) \rightarrow (p \land r) \in P \\
 &\implies \forall ((p\land q) \land (q \rightarrow r) \rightarrow (p \land r)) \in P \\
&\implies \exists((p\land q) \land (q \rightarrow r)) \rightarrow \exists(p \land r) \in P \  \text{(by II)}.
\end{aligned}
$$
By hypothesis,  $\exists(p\land q) \land \forall (q \rightarrow r) \in P$, hence by (III), $(\exists((p\land q) \land (q \rightarrow r))) \in P$. Applying Modus Ponens ends the proof.
