Towards Proof-Theoretic Formulation of the General Theory of Term-Forming Operators

TL;DR

This paper develops a proof-theoretic framework for term-forming operators, unifying various approaches and demonstrating applications to set theory, thereby advancing the theoretical understanding of these operators in formal languages.

Contribution

It introduces a proof-theoretic formulation of term-forming operators, comparing multiple existing approaches and applying the theory to Quine's set theory NF.

Findings

Unified proof-theoretic framework for tfos

Comparison of different theoretical approaches

Application to Quine's set theory NF

Abstract

Term-forming operators (tfos), like iota- or epsilon-operator, are technical devices applied to build complex terms in formal languages. Although they are very useful in practice their theory is not well developed. In the paper we provide a proof-theoretic formulation of the general approach to tfos provided independently by several authors like Scott, Hatcher, Corcoran, and compare it with an approach proposed later by Tennant. Eventually it is shown how the general theory can be applied to specific areas like Quine's set theory NF.