Difference between revisions of "Rewriting for-all and exists within set theory"
From Maths
(Created page with "{{Stub page|grade=A*|msg=Flesh out, check, link to formal logic}} __TOC__ ==Statement== Let {{M|\varphi(x,a_1,\ldots,a_n)}} be any "predicate" or {{link|formula|FOL}} where {{...") |
(No difference)
|
Latest revision as of 17:26, 8 March 2017
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