Logical frameworks for truth and abstraction cantini a
Rating:
4,3/10
832
reviews

If we assume , , we can infer T c---,y , i. A number of notations are adopted in the whole text. {Alternatively, we might apply a cut to , and then 53. Unless it is unclear from the context, we keep using the same symbols i, k, j, n, m for level constants and their values. Last but not least, this work is dedicated to my children Giulia and Francesco.

Troelstra kindly suggested an English translation of the author's monograph Cantini 1983a about theories of partial operations and classifications in the sense of Feferman 1974. For bracketing, we adopt the usual conventions; V, 3, -~ bind stronger than the other symbols, while A, V bind more than ---, and ~. If F is an instance of A. We also define a canonical enumeration of the finite subsets of w: e n - { n o ,. In fact properties, given in intension, may apply to anything in a given realm, without type restrictions; and the same must hold of the functions underlying the properties themselves.

We shorten logical equivalence on the metalevel i. We end up the section by considering a natural question: is there any reasonable counterpart at the level of predication of the set-theoretic power set operation? Proof-theoretic considerations and conservative extension results play an important role in classifying the various systems: very loosely, we tend to stress the importance of frameworks not stronger than Peano arithmetic and Introduction 5 to distinguish predicative from impredicative systems. However, the present work is far from being comprehensive. The intuitive idea is that truth is the direct limit of local self-referential truth predicates, which are related one another by a directed pre-order of levels. Part D deepens the intuitions underlying the systems of parts A-C by use of prooftheoretic techniques and by relativizing the concept of truth.

However, the present work is far from being comprehensive. Ab being the underlying combinatory algebra. Let x be a class such that Vu urlx ~ urir. Academics, students and researchers will find that the book contains a thorough overview of all relevant research in this field. The most comprehensive treatment we are aware of, is the long paper of Richter-Aczel 1974 , which is our reference text below for all details not included here. In particular, we consider a logical theory of constructions, that has been investigated in Theoretical Computer Science and is strictly linked with the theories of part D.

Then we argue as in the previous case, with introduction and inversion lemmata 28. Simultaneous inductive definition of P O S n and N E G n. To this aim, we observe that internal truth yields a wellbehaved notion of general predicate application in short predication , and that the underlying combinatory structure grants a systematic notation for partial predicates defined by abstraction. If a is an U-atom and b is an U-atom, we have a - u b or a ~ u b, according to a - b or a b ; i f a i s an U-atom and bis an U-set or symmetrically , we get a ~ u b. As we previously explained, the starting point of the book is the need for an independent logical approach to the notions of predicate application, property, abstraction, truth.

Sets are well-founded, in the sense that they satisfy forms of E-induction and number-theoretic induction. Indeed, if we combine the fixed point theorem for operations and the abstraction schema, we get the simple and fundamental: 10. Abstract This English translation of the author's original work has been thoroughly revised, expanded and updated. According to the iterative conception, a set is always a collection of mathematical entities of a given type possibly, sets of lower rank ; thus it has its being in its members, and equality among sets is ruled by the extensionality principle. The first system, due to Myhill 1972, 1980 , relies on a logic with levels of implication. A final comment is left for the choice of non-extensional basic notions. We shorten logical equivalence on the metalevel i.

Clearly b is a V-set; if x E V Y and y E y a, it is immediate to see that there is a v - y x such that vy b l apply the definition of E V, 21. Connections with Definability Theory are also established. As a leading choice criterion for the present volume, we tried to combine papers containing relevant technical results in pure and applied logic with papers devoted to conceptual analyses, deeply rooted in advanced present-day research. Research arising from paradoxes has moved progressively closer to the mainstream of mathematical logic and has become much more prominent in the last twenty years. Provability and standard Tarskian semantics.

The typical structure essentially consists of a pair is a subset of M. Approximating properties by classes 17. The schema of level induction is derivable with A. The argument requires a number of separate steps and definitions; the essential point is to introduce the operation D e f in our language. How to use the book.

To give the reader a closer idea of what is in the book, we shall survey the content of the single chapters. We introduce the abbreviations: Vi -~ k. Then x - u Y follows from 21. In the second chapter, we inductively expand combinatory algebras with a notion of self-referential truth, which naturally generalizes the familiar Tarskian semantical clauses, in order to cope with a situation of partiality. If A is a conjunction or a negation, the conclusion is an immediate consequence of the induction hypotheses and T-logic. Sets are conceived as completed totalities, generated by language independent operations and iterations thereof. The infinitary sequent calculus I T ~ of n-iterated reflective truth 51.