Naslov
Alternative axiomatization of NFU

Autori
Adlešić, Tin ; Čačić, Vedran

Vrsta, podvrsta i kategorija rada
Sažeci sa skupova, sažetak, znanstveni

Izvornik
Logic and Applications LAP 2022-Book of Abstracts / - , 2022, 5-6

Skup
Logic and Applications LAP 2022

Mjesto i datum
Dubrovnik, Hrvatska, 26.09.2022. - 29.09.2022

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Nije recenziran

Ključne riječi
New Foundations with atoms ; Axiom of choice ; Axiomatization

Sažetak
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.

Izvorni jezik
Engleski

Znanstvena područja
Matematika

POVEZANOST RADA