3 Other axioms
3.1 Natural numbers
The four axioms above (ax_∅, ax_set2, ax_℘, ax_⋃) produce elementary sets but no infinite set.
von Neumann constructed the natural numbers by \(n+1=n\cup\{n\}\). In Mathelia it is natural to make the set of all natural numbers as follows.
word(,s) …
\(\mathbb{M}\)𝕄. …
\(\mathbb{M} = \{ n \mid \forall M \, ( \emptyset \in M , \forall x \in M . x \cup \{ x \} \in M \Longrightarrow n \in M ) \}\) ax_∞ …
\(\exists M ( \emptyset \in M , \forall x \in M . x \cup \{ x \} \in M )\) \(\blacktriangleleft\) 𝕄.3.2 Axiom of regularity (axiom of foundation)
The following axiom was introduced by von Neumann.
ax0 …
\(\forall X \neq \emptyset . \exists Y \in X . X \cap Y = \emptyset\) \(\mathbb{V}_0 = \mathbb{V}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax03.3 Axiom of replacement
\(! x P\) expresses "there is at most one x satisfying P".
abbr …
\(! x P\) ≈
\(\forall y , z \in \{ x \mid P \} . y = z\) The axiom of replacement requires that "the image of a set under a functional property is a set".
ax_r …
\(\forall \mathbin{p} ( \forall x \, ! y \, x \mathbin{p} y \Longrightarrow \forall X \, \dot\exists \{ y \mid \exists x \in X . x \mathbin{p} y \} )\) \(\mathbin{p}\) is a binary predicate variable. ZF's axiom of replacement is one axiom for each formula put into ??p^ (a collection of infinitely many axioms); ax_r writes them together as "for all ??p^".
Mathelia uses ax_r only as instances in which a formula is substituted for ??p^ (the same role as ZF's axiom schema).
When substituting a formula for ??p^ in ax_r, follow the
x ??p^ y in ax_r and write the 1st argument as x and the 2nd as y.
The axiom of separation is derived from ax_r, using the instance with "x∈_C_ and y=x" substituted for ??p^.
ax_s
\(\blacktriangleleft\) ax_rThe
ax_r[??p^:=`x ∈_ C_ and y = x`] in the sos of the first step is the instance of ax_r with "x∈_C_ and y=x" substituted for ??p^. Substituted instances can be written directly in the sos of a step like this. The last
ax_s ◀ ax_r h; puts it together into a Thm of the form "derived from ax_r". Both x and y need not appear in the substituted formula (e.g.
ax_r[??p^:=`y = ∅`] shows "the image sending each element of X to ∅ is a set").
The axiom of pairing is also derived from ax_r. First we show, from the empty set and the power set alone, that there is a set with two distinct elements (
\(\wp ( \wp \emptyset )\) has
\(\emptyset\) and
\(\wp \emptyset\) as elements, and since
\(\emptyset \in \wp \emptyset\) they differ; if they were equal,
\(\emptyset \in \emptyset\) would contradict ∅.).
le_set2 …
\(\exists C \, \exists^* s , t ( s , t \in C )\) \(\blacktriangleleft\) \(\mathbb{W}.\)For a set C with two distinct elements s, t, substituting the relation "send s to u and t to v" for ??p^ makes the image of C \(\{u, v\}\). The definition of the pair set, set2., is not used.
ax_set2
\(\blacktriangleleft\) ax_r ，le_set23.4 Image of a function
word+(s,s→s,c) …
\(\text{^}\)lower …
\(\stackrel{\text{^}}{\mathbin{{\sf f}}} A\) ≃
\(\{ \mathbin{{\sf f}} a \mid a \in A \}\) \(\stackrel{\text{^}}{{f}} X\) is the image \(\{?f(x) \mid x \in X\}\) of X under ?f. By the axiom of replacement, the image of a function is a set.
ax_im …
\(\forall X \, \dot\exists ( \stackrel{\text{^}}{{f}} X )\) ax_im
\(\blacktriangleleft\) ax_r3.5 Axiom of replacement for total functional relations
abbr …
\(\exists! x P\) ≈
\(\exists x P , ! x P\) ax_rt is ax_r with "at most one" (！) changed to "exactly one" (∃！). ax_r is equivalent to ax_rt together with ax_∅.
ax_rt …
\(\forall \mathbin{p} ( \forall x \, \exists! y \, x \mathbin{p} y \Longrightarrow \forall X \, \dot\exists \{ y \mid \exists x \in X . x \mathbin{p} y \} )\) \(\forall x \, \exists! y \, x \mathbin{q} y \Longrightarrow \forall X \, \dot\exists \{ y \mid \exists x \in X . x \mathbin{q} y \}\) \(\blacktriangleleft\) ax_r ax_s
\(\blacktriangleleft\) ax_rt ，ax_∅ \(\forall x \, ! y \, x \mathbin{q} y \Longrightarrow \forall X \, \dot\exists \{ y \mid \exists x \in X . x \mathbin{q} y \}\) \(\blacktriangleleft\) ax_rt ，ax_∅With this, the basics of writing and reviewing a Book (introducing words, props, Thms and prfs, backends, expansion by definitions) are in place.
As actual mathematics books, we recommend first looking at the books in articles1.