Implementation of mathematics in set theory: Difference between revisions

Content deleted Content added
Line 250:
For any set <math>A \in Fin</math>, define <math>|A|</math> as <math>\{B \mid A \sim B\}</math>.
Define N as the set <math>\{|A| \mid A \in Fin\}</math>.
 
The Axiom of Infinity of [[NFU]] can be expressed as <math>V \not\in Fin</math>: this is enough
to establish that each natural number has a nonempty successor (the successor of <math>|A|</math> being
<math>|A \cup \{x\}|</math> for any <math>x \not\in A</math>) which is the hard part of showing
that the Peano axioms of arithmetic are satisfied.
 
The operations of arithmetic can be defined in a style similar to the style given above
(using the definition of successor just given). They can also be defined in a natural
set theoretical way: if A and B are disjoint finite sets, we can define |A|+|B| as <math>|A \cup B|</math>. More formally, define m+n for m and n in N as
*<math>\{A \mid (\exists BC.B \in m \wedge C \in n \wedge B \cap C = \emptyset \wedge A = B \cup C\}</math>
(But note that this style of definition is feasible for the [[ZFC]] numerals
as well, but more circuitous: the form of the [[NFU]] definition facilitates set manipulations
while the form of the [[ZFC]] definition facilitates recursive definitions, but either theory
supports either style of definition).
 
The two implementations are quite different. In [[ZFC]], we choose a representative of
each finite cardinality to represent that cardinality (the equivalence classes themselves
are too large to be sets); in [[NFU]] the equivalence classes themselves are sets, and are thus
an obvious choice for objects to stand in for the cardinalities. However, the arithmetic
of the two theories is identical: the same abstraction is implemented by these two superficially
different approaches.