LOGICAL FRAMEWORKS FOR TRUTH AND ABSTRACTION

From M.Bunder,'s review in MathSciNet: "This book deals with type-free logical systems based on combinatory logic with a truth predicate. While it is highly impressive in the range of material that can be represented in the formal systems developed here, it is interesting that the author, who claims to be influenced by the tradition of illative combinatory logic in the sense of Curry and Fitch, refers to virtually none of this work and uses quite a different approach, which leads to far more complex systems with often quite similar results. A clear advantage of the author's approach is that throughout the book he is able to find models for his formal systems, which are therefore consistent. Consistency proofs in illative combinatory logics, on the other hand, are very rare and cover far less powerful systems. One of the attractions of combinatory logic is that with only three primitive symbols (`=' and the combinators K and S) and a few simple postulates all recursive functions can be defined. The Curry school's illative combinatory logic, obtained by adding one or two more primitive symbols, such as a subclass relation (Curry's "restricted generality'') and a few more postulates, allows the development of higher-order predicate logics, first-order arithmetic, and much of set theory and category theory. The author's basic system MF−, developed in Part A, has the combinators, various arithmetical concepts, the connectives ¬ and ∧, and the universal quantifier as primitive notions. Equations formed using these form the atomic formulas of a classical predicate calculus which also includes the predicate symbols N (natural numbers) and T (truth). Various additions lead to 59 formal systems, 144 axioms and 312 symbols as given in a very useful, but by no means complete, list at the back of the book! The aim of the author's study is to distinguish the notions of property and set and predicate application and set-theoretic membership. This contrasts with the Curry-style systems where, at least, property and class and predicate application and class membership are identified. In these systems the paradoxes are avoided because theorems of logic hold only for a class of propositions. Interestingly this class behaves very similarly to the class of propositions defined by the author, provided his T is identified with the identity combinator I (an option that makes MF− inconsistent). Another interesting fact is that while both the Curry-style illative combinatory logics and the author's extensions of MF− are type-free, terms in these systems can be shown to be elements of classes which can be interpreted as types. The remainder of Part A of the book is taken up with developing a theory of classes and predicates that has many desirable features. Included is a proof that MF− with a form of induction is stronger than Peano arithmetic. Part B introduces a conservative extension PWC+GID of MF− that includes induction over classes as well as a generalised induction scheme. Separation and reduction principles are proved, as well as an analogue of the Myhill-Shepherdson theorem for operations that are extensional with respect to the predication relation and a boundedness theorem for inductive sets. In Part C it is shown that the type-free logic of Myhill with multiple levels of implications and that of Aczel and Feferman with definitional equivalence relations can be interpreted in PWC+GID. Part D concerns a logic TLR which, instead of just T, has various levels of truth Ti. TLR allows the interpretation of the subsystem ATR0 of second-order arithmetic, which allows the proof of the comparability of well-orderings, the Luzin-Sierpiński theorem, the Gale-Stewart theorem and the Ulm structure theorem for countable reduced abelian p-groups. Systems related to TLR are also discussed. As in illative combinatory logic, tautologies are valid in MF− only under conditions involving the class of properties and propositionally can only be determined by the finite application of elementary rules. In Part E the author considers a system VF− that is not finitely based in this way and contains all of the classical first-order logic with equality. VF− is shown to be consistent and is related to the systems discussed in Part B. Extensions of VF− are considered that include truth principles suggested by modal logic. Finally, applications of the logical theories of Part D to the calculus of constructions and possible future uses in areas such as artificial intelligence and theoretical linguistics are discussed."