# Rewriting for-all and exists within set theory

From Maths

**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

## Contents

## 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:

- [ilmath]\forall x[x\in S\rightarrow\varphi(x)]\iff \forall x\in S[\varphi(x)][/ilmath] and
- [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^{[1]}.

## 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
^{[Note 1]}

- Let [ilmath]x[/ilmath] be given. Note there is always something to be given here

- [ilmath]\implies[/ilmath]
- 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

- [ilmath]\implies[/ilmath]

## Notes

- ↑ Note that by having [ilmath]x\in S[/ilmath] we know there is at least one [ilmath]x\in X[/ilmath], so [ilmath]\forall x\in S[\varphi(x)][/ilmath] is not vacuous

## References