Rewriting for-all and exists within set theory

Stub grade: A*

This page is a stub

This page is a stub, so it contains little or minimal information and is on a to-do list for being expanded.The message provided is:

Flesh out, check, link to formal logic

Statement

Let $\varphi(x,a_1,\ldots,a_n)$ be any "predicate" or formula where $x$ is a free variable and the $a_i$ are at most finitely many parameters, we will write $\varphi(x)$ for short but note any parameters are implied to be present. Then:

1. $\forall x[x\in S\rightarrow\varphi(x)]\iff \forall x\in S[\varphi(x)]$ and
2. $\exists x[x\in S\wedge\varphi(x)]\iff \exists x\in S[\varphi(x)]$

Some authors define the RHS of these as an abbreviation or short hand for the left expression, such as.

Proof

• 1)
  • $\implies$
    • Suppose there is no $x\in S$, by the nature of logical implication we see $x\in S\rightarrow\phi(x)$ holds, thus $\forall x\in S[\varphi(x)]$ holds
    • Let $x\in S$ be given, by the left hand side and the nature of implication, $\varphi(x)$ must hold.
  • $\impliedby$
    • Let $x$ be given. Note there is always something to be given here
      • if $x\notin S$ then by the nature of logical implication we consider the statement sated whether or not $\varphi(x)$ holds and we're done
      • if $x\in S$ then as $\forall x\in S[\varphi(x)]$ we see $\varphi(x)$ holds in this case
• 2)
  • $\implies$
    • Choose $x$ posited to exist such that $x\in S$ and $\varphi(x)$, then - as stated - $x\in S$, so this is a valid choice, and $\varphi(x)$ holds
  • $\impliedby$
    • Choose $x\in S$ posited to exist by the RHS, then $x$ exists, $x\in S$ and $\varphi(x)$ holds for it