By P. B Andrews
Read or Download A Transfinite Type Theory with Type Variables PDF
Similar logic books
A lucid, stylish, and whole survey of set idea, this quantity is drawn from the authors' massive instructing event. the 1st of 3 components specializes in axiomatic set concept. the second one half explores the consistency of the continuum speculation, and the ultimate part examines forcing and independence effects.
This ebook grew out of my curiosity in what's universal to 3 disciplines: arithmetic, philosophy, and historical past. The origins of Zermelo's Axiom of selection, in addition to the debate that it engendered, definitely lie in that intersection. because the time of Aristotle, arithmetic has been involved alternately with its assumptions and with the gadgets, akin to quantity and area, approximately which these assumptions have been made.
This can be the single monograph dedicated to the expressibility of finitely axiomatizable theories, a classical topic in mathematical common sense. the quantity summarizes investigations within the box that experience led to a lot of the present development, treating systematically all confident effects touching on expressibility.
- Dynamic Worlds: From the Frame Problem to Knowledge Management
- The Is-Ought Problem: An Investigation in Philosophical Logic
- Logic Synthesis and Verification Algorithms
- Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies
Extra info for A Transfinite Type Theory with Type Variables
E. [[Qocoo, coo,[nxoxo]] axiom of Q, but is a theorem, as we shall see in Chapter I1 (Theorem 100). Hence Rule R cannot be dispensed with. We can also show the independence of certain axioms and axiom schemata of Q. We outline these proofs below, leaving most of the details for the reader to verify. AXIOM 1 We construct a model Vt’ for Q which is similar to the model Vt described in Section 3, except that Q, now contains three objects. For a complete description of the model ‘B’and the interpretation of Q in W, simply replace the sentences “We first choose three distinct objects t, f and r which are not functions.
2 If W,[xa = yb] = f, then WzP0 = t by Lemma 5. 2 If W,[xa = yb] = t, then from the definition of W,Qozzit is clear that WG,, = w,yb . Now W,xa is in BWna ,where W,a = 7ca is in K'. Similarly w,y, is in %W,b, where W,b = xb is in K'. The domains By,where y is in K', are disjoint, so evidently W,a = W,b. Hence W,[a = b] = t, so W,Po = t by Lemma 5. This completes the proof of Theorem 7. THEOREM 8: The system Q is consistent. Proof: We first remark that assignments do indeed exist"). Indeed, we can describe certain assignments explicitly.
Note that no trouble arises when A . Qoaay,] y, were derivable in Q . I. Qoaaya] ya would also be derivable, so by Rule R and the axiom Ja(oa)[Qoaay,]2 C, (an instance of 4,) we would obtain C, & y, as a theorem of Q'. It is clear that Theorem 7 applies to Q' with respect to any principal interpretation of Q, in particular with respect to a principal interpretation in which the domain 5Dl of the model (and hence each domain) contains at least two elements. However for such an interpretation WJC, 3 ya] is not always t, since we can always choose x so that W,ya is not the same as W,C,.