Gödel operation

In mathematical set theory, a set of Gödel operations is a finite collection of operations on sets that can be used to construct the constructible sets from ordinals. introduced the original set of 8 Gödel operations ?₁,...,?₈ under the name fundamental operations. Other authors sometimes use a slightly different set of about 8 to 10 operations, usually denoted G₁, G₂,...

Definition

used the following eight operations as a set of Gödel operations :

The second expression in each line gives Gödel's definition in his original notation, where the dot means intersection, V is the universe, E is the membership relation, denotes range and so on.
uses the following set of 10 Gödel operations.
The reason for including the functions and which permute the entries of an ordered tuple is that, for example, the tuple can be formed easily from and since it equals, but it is more difficult to form when the entries are given in a different order, such as from and.^{p. 63}

Properties

Gödel's normal form theorem states that if is a formula in the language of set theory with all quantifiers bounded, then the function of,, is given by a composition of some Gödel operations. This result is closely related to Jensen's rudimentary functions.
Jon Barwise showed that a version of Gödel's normal form theorem with his own set of 12 Gödel operations is provable in, a variant of Kripke–Platek set theory admitting urelements.^{p. 64}