From ProofWiki
Jump to navigation Jump to search

Generalized sums

NBG, Gödel-style

Point of very substantial annoyance: Gödel and PW have opposite senses of function. That is, he says $f(x) = y$ iff $\langle y, x \rangle \in f$. He similarly inverts the sense of the "domain" of a relation, and its image (which he calls its "domain of values"). I'm not sure if it makes sense to do as he did, or if it is better to flip everything around as needed to match the PW way. This runs into all sorts of things, such as the "axiom of domain", where either the axiom or its name would have to change to match PW's approach. Simply using PW names for the concepts would be entirely unworkable, with everything he calls a function being called instead a one-to-many right-total relation and confusing the heck out of everyone. Obviously, this whole matter is ultimately trivial, but the details are not pretty.

Primitive predicates:

  • $\mathfrak{Cls}(A)$: $A$ is a class.
  • $\mathfrak{M}(A)$: $A$ is a set.
  • $X \in Y$, $X \in y$, $x \in Y$, $x \in y$: express membership

Convention: capital letters are variables whose range consists of all classes; lower case letters are variables ranging over all sets. That is, $\forall x: P(x)$ should be read as $\forall x: (\mathfrak M(x) \implies P(x)$.

Gödel uses the convention that previously unmentioned free variables are considered universally quantified. Not sure how I want to handle that—it's sometimes convenient, but it can get confusing.


Group A

Every set is a class:

$1 \quad \mathfrak{Cls}(x)$

An element of a class is a set:

$2 \quad X \in Y \implies \mathfrak{M}(X)$

Axiom of Extensionality:

$3 \quad \left({ \forall u: (u \in X \iff u \in Y) }\right) \implies X = Y$

Axiom of Pairing:

$4 \quad \forall x: \forall y: \exists z: (u \in z \iff u = x \lor u = y)$

Definition 1:

  • $\mathfrak {Pr}(X) \iff \lnot \mathfrak M(X)$: $X$ is a proper class.


Pairing is unique, by extensionality. That is:

  • $\forall x: \forall y: \exists! z: (u \in z \iff u = x \lor u = y)$

Definition 1.1:

Given sets $x$ and $y$, the unique $z$ proven to exist by axioms 3 and 4 is the non-ordered pair of $x$ and $y$, denoted $\{x,y\}$ (actually, he denotes it $\{xy\}$, but I don't think we will be following that.

Definition 1.11:

$\{x\} := \{x, x\}$ (singleton, but not named that here)

Definition 1.12:

$\langle x, y \rangle = \bigl\{ \{x\}, \{x, y\} \bigr\}$ ordered pair

Theorem 1.13:

$\langle x, y \rangle \implies x = u \land y = v$

Proof (omitted, but we already have one or two).

Definition 1.14:

$\langle x, y, z \rangle = \langle x, \langle y, z \rangle \rangle$ Ordered triple

Definition 1.15:

Inductively: $\langle x_1, x_2, \dots, x_n \rangle := \langle x_1, \langle x_2, \dots, x_n \rangle \rangle$

Theorem 1.16:

NOTE: Gödel uses "ordinal" and "ordinal number" in precisely the same way that Kelley used them 15 years later.

Natural Numbers

NBG Set Theory

Note: these three theorems about power sets don't actually require the power set axiom.

Simple bits useful for various things; some left out or glossed over as trivial; some may be present but I haven't gotten to them yet.

Order and Lattice

Group Theory


Usual Topology

Properties of Compatible Relations

Properties of Ordered Groups

Systematic development of positivity

The names are made up, but the stories are real.

So far I believe I've established the equivalence of the theories of transitive relations compatible with group operations and of "cones" compatible with group operations. There is more to flesh out in this realm, as below. I have just started working on the ring stuff.

Discussion point: the notion of a "cone" compatible with an operation can be defined for any magma and closed ringoid. However, without a group structure, I'm not sure if there's a way to link such to compatible relations. Does anyone else see a way to do so?

Proofs sketched out reasonably well; cleanup work appreciated

Unstarted/Unfinished Ideas/Conjectures

Properties of Ordered Rings

Lexicographic Orderings


Useful links

Axiom of Foundation at NLab