Extending the first-order theory of combinators with self-referential truth
Andrea Cantini · Journal of Symbolic Logic · 1993
Abstract The aim of this paper is to introduce a formal system STW of self-referential truth, which extends the classical first-order theory of pure combinators with a truth predicate and certain approximation axioms. STW naturally embodies the mechanisms of generalpredicate application/abstractionona par withfunction application/abstraction; in addition, it allows non-trivial constructions, inspired by generalized recursion theory. As a consequence, STW provides a smooth inner model for Myhill's systems with levels of implication.