Prove the following rules for formulas with bounded quantifiers I have a question that goes like this: Prove the following rules for formulas with bounded quantifiers (derive them from suitable logical rules for unbounded quantifiers):
a) [(∀x)α(x) φ(x) ∧ (∀x)α(x) ψ(x)]⇔(∀x)α(x) (φ(x)∧ψ(x))
b)∼(∃x)α(x) φ(x) ⇔ (∀x)α(x) ∼φ(x)
My attempt to solve it:
a) I started with the LHS to derive the RHS:
[(∀x)α(x) φ(x) ∧ (∀x)α(x) ψ(x)] ⇔ [(∀x)α(x) ⇒ φ(x)] ∧ [(∀x)α(x) ⇒ ψ(x)] ⇔ (∀x)[α(x) ⇒ φ(x) ∧ α(x) ⇒ ψ(x)] ⇔ (∀x)α(x)[α(x) ∧ ψ(x)]
b) The same approach, I started with LHS:
∼(∃x)α(x) φ(x) ⇔ ∼(∃x)[α(x) ∧ φ(x)] ⇔ (∃x)[∼α(x) ∨ ∼φ(x)] ⇔ ∼(∃x)[∼α(x) ⇒ φ(x)] ⇔ (∀x)∼[∼α(x) ⇒ φ(x)] ⇔ (∀x)[α(x) ∧ ∼φ(x)] ⇔ (∀x)α(x) ∼φ(x).
I am not sure if what I did are correct especially for b)! Any help may be appreciated!
 A: I'm going to assume that you're looking for an intuitive proof rather than working in a formal proof calculus with fixed rules. If you are in the market for a proof calculus and one isn't part of the course, I suggest taking a look at the first-order tableau calculus without unification and the sequent calculus LK.
The notation you're using for bounded quantifiers is a little bit hard to read. Here's an alternative notation that's fairly standard.
$ \forall x \in P \mathop. Q(x) $ means for every $x$ in $P$, $Q$ holds of $x$.
$ \exists x \in P \mathop. Q(x) $ means for some $x$ in P, $Q$ holds of $x$.
Here is an equivalence that holds for bounded quantifiers (this is frequently how they are defined). You are using these equivalences in your argument, but I think it may be a good idea to call them out explicitly.
$$ \forall x \in P \mathop. Q(x) \;\text{holds} \;\;\text{if and only if}\;\; \forall x \mathop. P(x) \to Q(x) \; \text{holds} $$
$$ \exists x \in P \mathop. Q(x) \;\text{holds} \;\;\text{if and only if}\;\; \exists x \mathop. P(x) \land Q(x) \; \text{holds} $$
The theorems that you have written are both correct, although the proof for $b$ appears to contain a problem.
The proof for $a$ is correct, although you do not seem to be using a proof calculus with specific rules.
The proof for $b$ contains at least one invalid step. It has
$$ \textbf{wrong:} \;\; \lnot (\exists x \mathop. \alpha(x) \land \varphi(x)) \;\;\text{is equivalent to}\;\; \exists x \mathop. \lnot \alpha(x) \lor \lnot\varphi(x) $$
For the kind of rewrite that you did where you push a negation into the leaves of an expression, you need to replace each quantifier with its dual in addition to swapping $\land$ and $\lor$ (which are similarly dual).
$$ \lnot (\exists x \mathop. \alpha(x) \land \varphi(x)) \;\;\text{is equivalent to}\;\; \forall x \mathop. \lnot \alpha(x) \lor \lnot\varphi(x) $$
