We investigate a theory of Frege structures extended by the Myhill-Flagg hierarchy of implications. We study its relation to a property theory with an approximation operator and we give a proof theoretical analysis of the basic system involved. MSC: 03F35, 03D60.

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 general predicate application/abstraction on a par with function 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.

We present a model of computation for string functions over single-sorted, total algebraic structures and study some basic features of a general theory of computability within this framework. Our concept generalizes the Blum-Shub-Smale setting of computability over the reals and other rings. By dealing with strings of arbitrary length instead of tuples of fixed length, some suppositions of deeper results within former approaches to generalized recursion theory become superfluous. Moreover, this gives the basis for introducing computational complexity in a BSS-like (...) manner. Relationships both to classical computability and to Friedman's concept of eds computability are established. Two kinds of nondeterminism as well as several variants of recognizability are investigated with respect to interdependencies on each other and on properties of the underlying structures. For structures of finite signatures, there are universal programs with the usual characteristics. For the general case of not necessarily finite signature, this subject will be studied in a separate, forthcoming paper. (shrink)