Logical Frameworks for Truth and Abstraction: An Axiomatic StudyThis English translation of the author's original work has been thoroughly revised, expanded and updated. The book covers logical systems known as type-free or self-referential. These traditionally arise from any discussion on logical and semantical paradoxes. This particular volume, however, is not concerned with paradoxes but with the investigation of type-free sytems to show that: (i) there are rich theories of self-application, involving both operations and truth which can serve as foundations for property theory and formal semantics; (ii) these theories provide a new outlook on classical topics, such as inductive definitions and predicative mathematics; (iii) they are particularly promising with regard to applications. 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. A number of significant developments, techniques and results have been discovered. Academics, students and researchers will find that the book contains a thorough overview of all relevant research in this field. |
Contents
| 1 | |
| 11 | |
Truth and recursion Theory | 83 |
Selected Topics | 149 |
Levels of Truth and Proof Theory | 213 |
Alternative Views | 349 |
| 425 | |
| 441 | |
List of Symbols | 453 |
Other editions - View all
Logical Frameworks for Truth and Abstraction: An Axiomatic Study Andrea Cantini No preview available - 1996 |
Common terms and phrases
abstraction AD(U AD(V apply arbitrary arity assume atoms axiomatic axioms basic bounded chapter choose Church–Rosser theorem clauses closed term closure combinatory logic conclusion consistent COROLLARY cut elimination define derivation e-atom encodes extended Feferman finite fixed point formal formula free variables GID H hence holds i-class implies impredicative In(X induction schema inductive definitions inference infinitary interpretation Jíb language LEMMA monotone Moschovakis n e w N-induction natural numbers notations notion number-theoretic induction O(JMb obtain operator ordinal Peano arithmetic primitive recursive primitive recursive function PROOF proof-theoretic properties PROPOSITION provably proves quantifiers recursion theory reflective truth relation rules second-order arithmetic semantics sequent sequent calculus STLR structure subsets subsystems supervaluation T-dense T-imp T-positive theorem theory transfinite induction transfinite recursion trivial truth predicate type-free verify whence X C M yields
Popular passages
Page 1 - typical ambiguity" is a step in this direction. Since, however, it only adds certain simplifying symbolic conventions to the theory of types, it does not de facto go beyond this theory. It should be noted that the theory of types brings in a new idea for the solution of the paradoxes, especially suited to their intensional form. It consists in blaming the paradoxes not on the axiom that every propositional function defines a concept or class, but on the assumption that every concept gives a meaningful...
Page 1 - ... types, it does not de facto go beyond this theory. It should be noted that the theory of types brings in a new idea for the solution of the paradoxes, especially suited to their intensional form. It consists in blaming the paradoxes not on the axiom that every propositional function defines a concept or class, but on the assumption that every concept gives a meaningful proposition, if asserted for any arbitrary object or objects as arguments. The obvious objection that every concept can be extended...
Page 14 - Here as usual, p[t/x] stands for the result of substituting t for the free occurrences of x in p.
Page v - PREFACE This book is concerned with logical systems, which are usually termed typefree or self-referential and emerge from the traditional discussion on logical and semantical paradoxes. We will consider non-set-theoretic frameworks, where forms of type-free abstraction and self-referential truth can consistently live together with an underlying theory of combinatory logic. However, this is not a book on paradoxes; nor we aim at a grand logic a la Frege- Russell, inspired by a foundational program.
Page v - Russell, inspired by a foundational program. We shall rather investigate type-free systems, in order to show that: (i) there are rich theories of self-application, involving both operations and truth, which can serve as foundations for property theory and formal semantics; (ii) these theories give new outlooks on classical topics, such as inductive definitions and predicative mathematics; (iii) they are promising as far as applications are concerned.
Page 14 - V; (iii) the individual constants K (constant function combinator), S (composition combinator), SUC (successor), PRED (predecessor), PAIR (ordered pair operation), LEFT (left projection), RIGHT (right projection), 0...
Page 15 - As usual, a numeral is any term obtained from the constant zero by means of a finite number of successor applications; if n...
References to this book
Low-Power Wireless Infrared Communications Rob Otte,Leo P. de Jong,Arthur van Roermund No preview available - 1999 |
One Hundred Years of Russell's Paradox: Mathematics, Logic, Philosophy Godehard Link Limited preview - 2004 |