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 [ilmath]\varphi(x,a_1,\ldots,a_n)[/ilmath] be any "predicate" or formula where [ilmath]x[/ilmath] is a free variable and the [ilmath]a_i[/ilmath] are at most finitely many parameters, we will write [ilmath]\varphi(x) [/ilmath] for short but note any parameters are implied to be present. Then:

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

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

Proof

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