engleski

Alternative axiomatization of NFU

The main notion of theory NF(U) is that of stratification. In order to show that a formula is stratified, one must assign types to its variables and check whether they satisfy certain conditions. Assigning types is a rather straightforward procedure, and continues to be so when a language is extended by introducing abstraction terms and it is specified how to assign types to them. However, types of some terms have certain undesirable properties. The most prominent example are Kuratowski’s ordered pairs, where the type of the ordered pair is two types higher than the types of its projections (ordered pairs, as defined by Kuratowski, are not type-leveled). Our goal is to explicitly define type-leveled ordered pairs. In order to do that, we suggest adding, along with the axiom of infinity, a specific version of the axiom of choice to the theory NFU. Namely, Tarski’s theorem about choice, which we call Tarski’s axiom. Tarski’s axiom cannot be stated right away, so we first need to introduce few notions using Kuratowski’s ordered pairs. After that, we are able to state Tarski’s axiom and can directly use it to define type-leveled ordered pairs. Then the theory NFU + Inf + Tarski’s axiom can be developed further using type-leveled ordered pairs, which is a big simplification in comparison to the theory NFU +Inf+AC with Kuratowski’s ordered pairs.

New Foundations with atoms ; Axiom of choice ; Axiomatization

nije evidentirano