engleski

Formal approach to stratification in NF/NFU

New foundations for mathematical logic (sometimes called Quine’s New Foundations and often abbreviated by NF) was introduced in order to eliminate some of the annoying consequences of Russell–Whitehead’s type theory, most notably, the one that some classes appear in every type. NF solves this problem by introducing the notion of stratification and stratif ied formulas, while retaining all positive aspects of Principia like the possibility of developing the arithmetic and forbidding paradoxes. In a way, NF is simple type theory in disguise. We formally define stratification and prove some intuitive claims about it. Because the notion of stratification is concerned only with variables, in order to simplify further theory development, we extend its notion to encompass abstraction terms. This extension enable us to check whether some complex formula is stratified without rewriting it in the basic language. For every additional term we give a rule what type can be assigned to it, and in what circumstances. We will provide few examples in order to demonstrate the benefits of our formalization. By formalizing the stratification in full, NF becomes easier to read and comprehend and its exposition becomes more clear.

Quine’s New Foundations ; stratification ; stratified formulas

nije evidentirano