Can a predicate imply another predicate? I have studied sentential calculus(propositional logic) carefully, but not predicate logic. My questions is: can we prove(not just simply writing it down, I mean to prove) "predicate implying another predicate"? (i.e. prove $P(x)\Rightarrow Q(x)$, without referring to any quantifiers $\forall$, $\exists$)
For example, can we formally prove something like $x>3\Rightarrow x-3>0$? In my previous experience, it can not; unless writing it in a quantified manner, such like (1) and (2) below.
(1)$\forall x\in\mathbb{R},~(x>3\Rightarrow x-3>0)$
Proof: Let $x$ be any real number, and suppose $x>3$, then $x-3>0$, hence $\forall x\in\mathbb{R},~(x>3\Rightarrow x-3>0)$"

(2)$\exists x\in\mathbb{N},~(x>3\Rightarrow x-3>0)$
Proof: Let $x=1$, then $1>3$ is false, hence $1>3$ implies anything, so we get $\exists x\in\mathbb{N},~(x>3\Rightarrow x-3>0)$

I came up with this question while I was studying analysis. I want to prove a very easy theorem in a metric space chapter.
Let $(X,d)$ be a metric space, $E\subseteq X$, and $a\in X$.
Then $(\exists r>0,~B_r(a)\cap E=\phi)\Longleftrightarrow(\exists r>0,~B_r(a)\subseteq X-E)$.
If we are allowed to directly play with "predicates", not referring to any quantifier matters, then we can just prove that $B_r(a)\cap E=\phi\Longleftrightarrow B_r(a)\subseteq X-E$, then we put a $\exists$ symbol in the front, and we get the result. But if we cannot doing this, then we should prove it as follows:
Proof: Suppose $\exists r>0,~B_r(a)\cap E=\phi$, then let $x\in B_r(a)$, if $x\in E$ then $x\in B_r(a)\cap E$, thus $B_r(a)\cap E\neq\phi$, a contradiction, so $x\not\in E$. Hence $x\in X-E$. Therefore, this $B_r(a)\subseteq X-E$. So we get $\exists r>0,~B_r(a)\cap E=\phi$ implies $\exists r>0,~B_r(a)\subseteq X-E$. And the proof of the inverse implication is similar and omitted. $\square$
I think this proof is lengthy, due to concretely operate the EI/EG rules.
 A: Typically, when a formula that we prove has free variables, what we are really proving is the so-called universal closure of that formula. If you try to prove $\phi(x_1,\ldots,x_n)$, what you're really proving is $\forall x_1 \cdots \forall x_n \phi(x_1,\ldots,x_n)$. You notice this when you try to prove "without quantifiers" that $x > 3 \implies x - 3 > 0$. You just start with the assumption, $x > 3$, and argue that we can subtract 3 from both sides without changing the inequality, and conclude $x - 3 > 0$. Hence, $x > 3 \implies x - 3 > 0$. What you've "really" proved is, indeed, $\forall x (x > 3 \implies x - 3 > 0)$.
When you give your "shorter" proof of your statement about metric spaces, what you are really proving is
$$
\forall r>0(B_r(a)\cap E=\emptyset\Longleftrightarrow B_r(a)\subseteq X-E),
$$
which is, strictly speaking, different from what you are asked to prove, which is
$$
(\exists r>0,~B_r(a)\cap E=\emptyset)\Longleftrightarrow(\exists r>0,~B_r(a)\subseteq X-E).
$$
In fact, what you have proved is stronger, in the sense that whenever you can prove for formulas $\phi(r),\psi(r)$ that $\forall r(\phi(r) \iff \psi(r))$, then you can also prove $\exists r\phi(r) \iff \exists r \psi(r)$ quite easily. But it does take a few more steps, which is how you get your "longer" proof.
