The Model Study Of Anti-founded Axioms

In the classic axiomatic system ZF of set theory, there is an axiom which char-acterizes sets. This axiom denoted by FA is called foundation axiom, well-founded axiom or regular axiom. Before adding FA into ZF, whether there are circular sets in ZF is not determined. After adding FA into ZF, it not only excludes Russell Para-dox but also confines all objects of classic set theory to be well-founded. In the same time, FA also exclude sets which satisfy the circular condition x∈x and the∈-infinite descent chain condition (these sets are called non-well-founded sets). The foundation axiom FA confined the universe of ZF in the range of well-founded sets. So, the classic axiomatic system ZF of set theory can not characterizes circular phenomenon. However, circular phenomenon are full of everywhere. For example, the circularity of day and night in nature; the circularity of the four season of spring, summer, fall and winter in year after year; the circularity of the red light, the yellow light and the blue light in traffic. For anther instance, the circularity of automata system and transi-tion system in computer science; the circularity of the structure of "know" of common knowledge in philosophy; the circularity of self-reference of the Liar Paradox in se-mantics. It is an important job for logician and mathematician in the later of 20 century to model the circular phenomenon or non-well-founded sets.Aczel proposed the anti-founded axiom AFA in 1988. He replaced the founda-tion axiom FA in ZF with the anti-founded axiom AFA and obtained the non-well-founded system of set theory ZFC-+AFA. Aczel built a model for ZFC-+AFA and created the theory of non-well-founded sets. Since the theory of non-well-founded sets can model circular phenomenon, they play a very important role in philosophy, mathematics, economics, logics, semantics and theoretic computer science.Based on studying home and abroad investigations, the dissertation sketches the theory of non-well-founded sets and discuss the extensionality of non-well-founded sets. What is more, in terms of the constructible model L of Godel, we use the method of Aczel to build constructible models for axiomatic system ZFC-+AFA which con- tains the anti-founded axiom AFA and for axiomatic system ZFCˉ+AFA~ which includes the anti-founded axiom family AFA~;In addition, based on the job of Lind-strom, we still use the method of Aczel to build constructive model for axiomatic sys-tem ZFCˉ+AFA~ which contains the anti-founded axiom family AFA~. These work makes certain sense in enriching the theory of sets and contributes to the devel-opment of logics.In general, the major work of this dissertation are the following.First, we argument the relation of the foundation axiom FA and the anti-foundation axiom AFA, shows the limit of FA, explains the reason of AFA replacing FA and introduces the process of producing AFA.Second, we propose the axiom of extensionality in set universe B by using canon-ical pictures and discuss the axiom of extensionality in set universe V~. At the same time, we take many examples to explain how to judge the equality of two non-well-founded sets. In addition, we provide a proof of the including relation among the five set universes, that is WF(?)A(?)S(?)F(?)B. This accounts for that the universes of non-well-founded sets are extensions of the universe of the standard set theory (iterative set theory W F).Third, on the basis of Godel's constructible axiom V=L, we redefine the concept of decoration, system maps, the regular bisimulation and so on under the constructible set universe. Utilizing the method of Aczel, we build respectively the constructible models of ZFCˉ+AFA and ZFCˉ+AFA~. When we take (?) and (?) as the regular bisimulations respectively, we get the constructible models of ZFCˉ+SAFA (the axiomatic system of non-well-founded sets after substituting the foundation axiom FA with the anti-founded axiom SAFA of Scott) and ZFCˉ+FAFA (the axiomatic system of non-well-founded sets after replacing the foundation axiom FA with the anti-founded axiom FAFA of Finsler) respectively.Forth, based on Lindstrom building constructive model for the anti-foundation ax-iom AFA, we build the constructive model for the axioms family by AF A~ using the Martin Lof type theory. When the regular bisimulation～takes(?) and(?) respec-tively, we obtain the constructive models of ZFCˉ+SAFA and ZFCˉ+FAFA respectively.