Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
set_theory [2014/12/08 09:56] nikolaj |
set_theory [2015/10/08 13:53] nikolaj |
||
|---|---|---|---|
| Line 110: | Line 110: | ||
| Moreover, we have "$d=\{a,b,c\}$", expressing a similar statement about //three// mathematical object and so on. The set $\{a\}\cup\{b,c\}$, which can for example be build by taking the union of the pair of pairs $\{\{a,a\}\cup\{b,c\}\}$ then also happens to fulfill exactly that defining formula, i.e. $\{a\}\cup\{b,c\}=\{a,b,c\}$ etc.. Terms which are estabilished equal in the "$=$"-sense can be replaced for each other in a deduction. | Moreover, we have "$d=\{a,b,c\}$", expressing a similar statement about //three// mathematical object and so on. The set $\{a\}\cup\{b,c\}$, which can for example be build by taking the union of the pair of pairs $\{\{a,a\}\cup\{b,c\}\}$ then also happens to fulfill exactly that defining formula, i.e. $\{a\}\cup\{b,c\}=\{a,b,c\}$ etc.. Terms which are estabilished equal in the "$=$"-sense can be replaced for each other in a deduction. | ||
| - | The axioms replacement/comprehension/collection/specification tell us to which extend the deduction of "$x\in X\Leftrightarrow P(x)$" and the associated set construction is possible within our theory. If we can specify a set by a predicate $P$, then a like sentence $X=\{x|P(x)\}$ just denotes that $X$ is the set containing the sets (in the whole domain of discourse) for which $P$ is true: | + | The axioms replacement/comprehension/collection/specification tell us to which extent the deduction of "$x\in X\Leftrightarrow P(x)$" and the associated set construction is possible within our theory. If we can specify a set by a predicate $P$, then a like sentence $X=\{x|P(x)\}$ just denotes that $X$ is the set containing the sets (in the whole domain of discourse) for which $P$ is true: |
| | @#EEEE55: predicate | @#EEEE55: $X=\{x|P(x)\} \equiv \forall x.\ (x\in X\Leftrightarrow P(x))$ | | | @#EEEE55: predicate | @#EEEE55: $X=\{x|P(x)\} \equiv \forall x.\ (x\in X\Leftrightarrow P(x))$ | | ||
| Line 137: | Line 137: | ||
| ==== Discussion ==== | ==== Discussion ==== | ||
| + | === New symbols === | ||
| + | Most of what follows is concerned with demonstrating existence and uniqueness statements from the axioms and then introducing new symbols ($\emptyset, \omega_{\mathbb N}$, etc.) enabling us to use those propositions more concisely. We understand them as particular terms with particular properties, expressed by the corresponding propositions. | ||
| + | |||
| === Regarding axiom systems and their strengths === | === Regarding axiom systems and their strengths === | ||
| If a logical framework (e.g. first order predicate logic, modus ponens as derivation rule) to work with has been chosen, a collections of axioms for set theory determine how to work with the binary //set membership predicate// "$\in$". | If a logical framework (e.g. first order predicate logic, modus ponens as derivation rule) to work with has been chosen, a collections of axioms for set theory determine how to work with the binary //set membership predicate// "$\in$". | ||
| Line 148: | Line 151: | ||
| === Reference === | === Reference === | ||
| Wikipedia: | Wikipedia: | ||
| - | |||
| [[http://en.wikipedia.org/wiki/Implementation_of_mathematics_in_set_theory|Implementation of mathematics in set theory]], | [[http://en.wikipedia.org/wiki/Implementation_of_mathematics_in_set_theory|Implementation of mathematics in set theory]], | ||
| [[http://en.wikipedia.org/wiki/List_of_first-order_theories#Set_theories|Set theories in first order logic]], | [[http://en.wikipedia.org/wiki/List_of_first-order_theories#Set_theories|Set theories in first order logic]], | ||
| Line 154: | Line 156: | ||
| [[http://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory|Zermelo–Fraenkel set theory]], | [[http://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory|Zermelo–Fraenkel set theory]], | ||
| - | Metamath: [[http://us.metamath.org/mpeuni/grothprim.html|grothprim]] (Grothendieck-Tarski axiom using primitive symbols) | + | Metamath: |
| + | [[http://us.metamath.org/mpeuni/grothprim.html|grothprim]] (Grothendieck-Tarski axiom using primitive symbols) | ||
| ==== Parents ==== | ==== Parents ==== | ||
| === Requirements === | === Requirements === | ||
| [[Predicate logic]] | [[Predicate logic]] | ||
