KP
&
Admissible Sets
by Matt Belcher
Introduction
A Brief History of Admissible Sets
Gödel, in 1939, introduced a class L of constructible sets. This class was defined recursively as follows.
L0 = 0.
Lb = N{Lc | cPb } for a limit ordinal b.
Lb+1 = {u | uRLb & u in closure (LbN{Lb} }.
The purpose of this class was to collect all sets which could be constructed from only the empty set by means of Gödel's set operations: pair, difference, product, domain, projection and permutation. After doing so, one could attempt to prove a simpler version of the continuum hypothesis. Are there any sets in L that are also in the interval l0 to l1? Also, Gödel proved that the statement "all sets are constructible" is consistent with ZFC, but impossible to prove or disprove within it. Thus, mathematicians were free to add the statement, now called the Axiom of Constructibility, to ZF creating a new field of study, Constructible Set Theory.
Later, Kripke introduced the idea of an admissible ordinal by means of an equation calculus. Platek defines an ordinal Ñ as admissible differently. Suppose an idealized computer capable of performing operations involving less than Ñ steps. Then a function F computed by the machine is Ñ-recursive. The ordinal Ñ is then admissible if
ŽF (F is Ñ-recursive & ÒPÑ & F(Ò) is defined } F(Ò)PÑ).
The first such ordinal is è. Kripke and Platek's contribution allowed the study of recursion theory on ordinals which are not necessarily cardinals, such as the recursive analogue of è1.
These results complemented those of Gödel, resulting in a definability theory for all sets constructible up to an ordinal Ñ. Barwise then strengthened the theory to consider not just ordinals, but admissible sets, those in which closure conditions hold, and thus insure a reasonable definability theory. To do this, he readmitted urelements into the KP, allowing him to consider general definability, not just definability on transitive sets.
Motivation for KP
KP is largely concerned with issues of constructibility, as its history would suggest. ZF was unsuitable for this purpose for several reasons. First, ZF makes no distinction in the logical complexity of sets. For example, consider these subsets of è.
A = {x+xsxiè} and B = {xs x is even and x = y+z where y,z are primes}
Clearly, B is more logically complex than A, yet ZF makes no distinction between them. KP on the other hand, will make a distinction in the way they are constructed.
Second, ZF violates the principle of parsimony. That is, making only those assumptions necessary to prove a given theorem. Barwise (1975) gives the example of using the power set axiom to prove the existence of the cartesian product of two sets. This can be shown in KP using only the axioms of Ço - separation and Ço - collection, which are considered weaker than the power set axiom.
Finally, ZF requires that every model and mathematical object be realized as a set, since ZF is built entirely of sets. The variant of KP I will be most concerned with in this paper, KPU, allows urelements, i.e. those objects appearing to the left of an i, but not on the right. This allows one working in KPU to consider objects as being isomorphic to sets, something mathematicians already do in practice. KPU loses nothing by readmitting urelements, since one obtain results about sets without urelements simply by assuming the class of urelements is empty.
Axioms and Elementary Results
Language
The structure of a language L which expresses KP and KPU must have several properties. First it must consist of a non-empty class A of all sets, and a class M of all urelements. (In KP, M=Ÿ) It must also have a relation ia(MNA) D A, which represents the property of containment. It must also contain any other relations or operations that act on the whole of (MNA), such as the power set or transitive closure operations.
Two axioms of KP and KPU use a type of formula called Ço. A Ço formula in L is one in the collection defined by the following.
all atomic formulas of L are in the collection
if î is in the collection, then î is in the collection
if î,ç are in the collection, then îœç is in the collection
if î,ç are in the collection, then îç is in the collection.
if î is in the collection, then Žxiy î is in the collection.
if î is in the collection, the jxiy î is in the collection.
Axioms
Standard Axioms
The axioms of Kripke-Platek set theory come in three varieties. The first two are about the nature of sets. The next three allow for ways to construct new sets from old ones. The last, Ço - collection, is the most important, and ensures that in recursively defined sets, there will always be enough steps in the construction to define it. These axioms originally appeared in [Platek 1966].
Extensionality: Two sets are equal if they contain all the same elements.
i.e. Žx (xia 3 xib) } a = b.
Foundation: If î is a formula in which y is not free, and there is an x which satisfies the formula, then no y in x satisfies the formula î.
i.e. jx î(x) } jx [î(x) œ Žyix î(y)], where î is a formula in which y is not free.
Pair: If x,y are sets, then there is a set containing both x and y. This is different than the Pair Axiom in ZF, which asserts that a set exists which contains only x and y. In symbols, jA (xiA œ yiA).
Union: There is a set which contains the elements of the elements of any set.
i.e. jC ŽBiA ŽxiB (xiC)
Ço - Separation: There is a set containing those elements that in one set that satisfy a Ço formula. i.e. ŽA jB Žx [xiB 3 xiA œ î(x)] where î is a Ço formula.
Ço - Collection: If there is a set y, which for all x in some set, y satisfies a Ço - formula with x, then there is a set which contains y. In symbols, this is
Žxia jy î(x,y) } jb Žxia jyib î(x,y).
These six axioms make up the theory KPU. Since we defined our language with urelements, one additional axiom is necessary for KP. Simply, it states that every object is a set. Symbolically, Žx ja (x = a œ a is a set).
Additional Axioms
There are many variants of KP, one of which KPU, we have described already. In addition, some mathematicians add the following axioms to KP.
Infinity: Simply, there is a limit ordinal. The negation of this axiom asserts that all ordinals are finite. This taken with KP, implies that all sets are finite. KPU, however, does not have this restriction. Barwise mentions this in his case for readmitting urelements to KP.
Full Separation & Full Collection: These axioms are identical to Ço - Separation and Collection, except any formula in L may be used.
Beta Axiom: For every well-founded relation R a ADA, there is a function F and Dom(F) = A. This is similar to the first formulation of the axiom of choice, except it is restricted to well-founded relations.
Some Standard Set Theoretic Results
Set Existence
This section demonstrates KP's ability to model the same types of objects as ZF, such as ordered pairs, relations, and functions.
Proposition: There exists a unique set Ÿ, with no elements.
Proof: From our language, we know that the class of all sets is non-empty. Then we can get a witness b s.t. B is a set. Then, we can use Ço - Separation on b, where our formula is x@x. Since no element can satisfy this formula, we have Ÿ. Suppose another Ÿ' exists with no elements. Then by extensionality, Ÿ=Ÿ'.
Proposition: For any set a, there is a unique set Na such that xiNa iff
jyia (xiy).
Proof: By the union axiom, we know there is a set b s.t. jb ŽCiA ŽxiC (xib). Then, by separation, we can get Na = {xib | jyga (xiy)} Again, uniqueness follows from extensionality.
Proposition: For any sets a,b there are unique sets c = a O b and d = a N b.
Proof: As in class c = {xia | xib} by separation and d = N{a,b} by pair and union. They are also unique by extensionality.
For the next proof, we need to define an ordered pair in KPU the same way we need in class. <a,b> = {a,{a,b}.
Proposition: For any a,b aDb is a set. aDb = {<x,y> | xia and yib}.
Proof: Fix xia. Also, let yib be arbitrary. Then by the pair axiom, we get {x,y} and applied again, get {x,{x,y}}. Now, for all y, some x exists s.t. {x,{x,y}} is a set. So, we can now apply Ço - Collection to put all these ordered pairs in a set cx where Žy, <x,y>gc. Now, we apply Ço - Collection again, over x. Thus, we now have a set d where Žx Žy [<x,y>gc for some cid. Thus, Nd = aDb.
Ordinals
Since KP and KPU are used primarily to study recursively defined sets and ordinals, it is important to see how one can model ordinals in KP.
Definitions: A set a is transitive iff Žyia Žziy (zia). In KPU, urelements are not transitive, but a set of all urelements is transitive. Ÿ is transitive. A set is an ordinal Ñ iff it is transitive and ŽxiÑ x is transitive.
Proposition: Ÿ is an ordinal.
Proof: Ÿ is defined as transitive, and since it contains no elements, is trivially an ordinal.
Proposition: If Ñ is an ordinal, so is S(Ñ). S(Ñ) = ÑN{Ñ}.
Proof:
Claim 1: S(Ñ) is transitive. Let xgS(Ñ) and yix. By def. of union, x is either an element of Ñ or {Ñ}. If xiÑ, then yiÑ since Ñ is transitive. Then, by def. Of union, ygS(Ñ). If xi{Ñ}, then x=Ñ, since {Ñ} contains only one element. Then any elements of x are in S(Ñ), by def. of union. So S(Ñ) is transitive.
Claim 2: Every element of S(Ñ) is transitive. Let xgS(Ñ). Then, by def. of union, x is either an element of Ñ or {Ñ}. If xiÑ, then x is transitive, since Ñ is an ordinal. If xi{Ñ}, then x=Ñ, so x is transitive, since it is an ordinal.
Therefore, by claims 1 and 2 S(Ñ) is an ordinal.
Proposition: Every member of an ordinal is an ordinal.
Proof: Let Ñ be an ordinal. Suppose xgÑ is arbitrary. Then x is transitive by def. of ordinal. Now, let yix be arbitrary. Then, ygÑ since Ñ is transitive. So, x is transitive and every member of x is transitive, so x is an ordinal. Since x was arbitrary, this holds for all x.
Thus, we see that familiar properties for ordinals in ZF also hold in KP and KPU.
Applications
Admissible Sets
Barwise, in his Admissible Sets and Structures, uses KPU to define an admissible set. He then uses these sets to explore problems in recursion. I will give a few definitions to demonstrate how admissible sets are modeled in KPU. The universe VM of admissible sets in KPU over the class of urelements M will be defined recursively as follows.
VM(0) = 0
VM(ÑA1) = Power set of (MN VM(Ñ))
VM(Û) = NÑPÛVM(Ñ), where Û is a limit ordinal.
VM = NÑ VM(Ñ).
See the figure below for a graphical representation of this universe.
An admissible set over M is a model MM of KPU where MM = (M; A,i) and the set MNA is transitive in VM . For KP, we assume M=Ÿ. We call models in KP pure admissible sets, since they are constructed only from the empty set. The collection of all pure admissible sets contained within an admissible set MM is called the pure part of MM . Pure admissible sets correspond to those of constructible set theory.
An ordinal of an admissible set AM , denoted o(AM), is the least ordinal not in AM. An ordinal Ñ is admissible if Ñ=o(AM) for some M and AM. As I mentioned above, the first admissible ordinal is è. Since ordinals are closed under ordinal arithmetic in KPU, the next admissible ordinal Ñ>è is greater than èèè.
In order to construct some of the more important admissible sets, those in which Barwise develops his definability theory, he invokes Gödel's hierarchy of sets to build a class L of constructible sets in KPU via a list of operations. Many of Gödel's operations also appear in Barwise's list. These are pair, union, set difference, cartesian product, domain and permutation. The list also differs, in that KPU contains urelements, and thus the operations must take those into consideration. Barwise also adds range, picking out the second element from each pair in a relation. Finally, he adds three operations that correspond to atomic formulas. These are:
ºN={zix | z is an urelement}
º=={<v,u>iyDx | u=v}
ºi={<v,u>iyDx | uiv}
Barwise uses these operations of construction to build a set he calls HYPM and shows that any relation on the natural numbers is hyperarithmetic if that relation is a member of HYPM. Also, Barwise proves that HYPM is the smallest admissible set above M, the set of all urelements. Also, HYPM contains all constructible objects in some ordinal Ñ steps. Barwise showed how KP and even more KPU can be used to study constructibility, definability, and recursion theory, filling what he saw as an imaginary gap between those fields.
Proof Theory
Gerhard Jäger, in his Theories for Admissible Sets, demonstrates how the notion of admissible sets can be used in proof theory, extending their application to yet another field. Admissible sets are particularly useful in exploting connections between proof theory and definability theory. His basic approach follows.
Let Th be an arbitrary theory. First, find the least ordinal Ñ s.t. the class of objects constructible in Ñ induces a model on Th. Next, find a theory Th0 which formalizes the constructible class from the last step. Then, restrict the induction principles of Th0 to get the weakest subtheory Th1 of Th0 such that any sentence provable in Th0 is provable. Embed Th1 into ramified set theory. Then sThs=sTh1s. Based on this idea, he goes on to say that the proof-theoretic strength of a theory is determined by the number of admissibles and the amount of induction available.
Jäger's use of admissibles in proof theory further extended the scope of applicability for both KP and admissible sets. Other current applications of KP include commonsense theory for artificial intelligence, group theory, and computability theory.
References
Admissible Sets and Structures, Jon Barwise
Springer-Verlag, 1975
Theories for Admissible Sets, Gerhard Jäger
Bibliopolis, 1986
"Issues in Commonsense Theory" Müjdat Pakkan and Varol Akman
Artificial Intelligence Review, 1994-95
http://www.cs.bilkent.edu.tr/~akman/jour-papers/air/air.html
"Around Gödel's Theorem" Karlis Podnieks
http://www.ltn.lv/~podnieks/index.html