engleski

Formalizing assignment of types to terms in NFU.

Quine’s New Foundations for mathematical logic from 1937 (upgraded later in 1951) was originally meant as a theory for rigorously formalizing classes: collections of objects satisfying certain predicates. In order to avoid the usual paradoxes, Quine stipulated that objects be stratified— divided according to types, so that a class is of a higher type than its elements. In search of consistency proof, proper classes were expelled (to metatheory) leaving only the theory of sets, the theory was reworded so stratification became syntactic (the assignment of natural numbers to variables in the formula expressing the defining predicate), and also urelements (“atoms” without elements, while not being equal to the empty class) were added. The resulting theory, NFU, was shown to be consistent by Jensen in 1969. In a way, working in NFU seems a lot like working in any “usual” set theory—until it comes to the point where it’s necessary to justify the existence of a certain set. And there are a lot of such situations: for example, proving a claim by mathematical induction amounts to showing that a certain set is inductive—but first we must ensure it is a set. Checking that a formula is stratified is a straightforward, if boring, task in the basic {;∈, =};-language of set theory, but it becomes much more challenging when we add abstraction terms, functional and new relational symbols. To help us work, we have programmed a framework in Coq which can be used to establish whether the formula is stratified, find the least typization, and use that fact in establishing new notions.

New Foundations ; Formalization ; Coq

nije evidentirano