Books

# Books

A Book is a longer document written as a set of notes in the form of a book, and most are intended for publication in some form or other. One of these, Derivation and Computation, has been published already, but I don't have that in electronic form. Some of these books are in good shape, but still need a little polishing. One is little more than a random set of notes.

Here is a description of the contents of these documents in approximately in reverse chronological order of writing, that is with the latest at the top and the earliest at the bottom. I give a link to each document where it is a fit state to be let loose.

If you think any of these documents are worth completing and releasing, let me know and I will see what I can do.

• An introduction to lambda calculi and arithmetic
These notes are used as part of the course LINK TO BE INSERTED and cover about 10 to 15 hours of material. There are four chapters
• The untyped lambda-calculus lambda0
• The basic syntax
• The reduction mechanism
• Fixed point and other combinators
• Final remarks
• Simulation of arithmetic in lambda0
• The church numerals
• Simulation of functions
• Closure under primitive recursion
• Closure under unbounded search
• Final remarks
• The simply typed lambda calculus lambda1
• Types, terms, and reductions
• The typing discipline
• Simulation of arithmetic
• Product types and pairing gadgets
• Final remarks
• An applied lambda calculus
• The basic facilities
• Capturing numeric gadgets
• Closure under recursion
• Way beyond
each with a decent selection of exercises with solutions available.

The notes are in decent shape, but at present do get modified each time they are used for a course. They are available from lcalculus.dvi or lcalculus.ps.gz or lcalculus.pdf , but if you want the solutions you will have to ask me directly.

• An introduction to Category theory in four easy movements
These notes are used as part of the course LINK TO BE INSERTED and cover about 10 to 15 hours of material. They are designed to introduce the student to the basics through the study of many different examples without development much theory. There are four chapters
• Categories
• Categories defined
• Categories of structured sets
• Categories of posets
• Some other categories
• Some simple notions
• Functors and natural transformations
• Functors defined
• Some power set functors
• Some section functors
• Some other functors
• Natural transformations defined
• Examples of natural transformations
• Limits and colimits; a universal solution
• Products and sums
• Equalizers and coequalizers
• Pullbacks and pushouts
• Limits and colimits
• Inverse and direct limits
• Cartesian closed categories
• Cartesian closedness
• Some simple examples
• Monoid actions
• Developing sets
each with a decent selection of exercises with solutions available.

The notes are in decent shape, but at present do get modified each time they are used for a course. They are available from CatTheory.dvi or CatTheory.ps.gz or CatTheory.pdf , but if you want the solutions you will have to ask me directly.

• An introduction to Good old fashioned model theory
A few years ago I was asked to give a an introductory course in Model Theory to the postgraduates in a reasonably large Mathematical Logic group. (Not in Manchester, I might add.) At the time I couldn't find a suitable text to use, so I wrote my own notes. The course lasted about 20 hours, but I tried to put more into the notes than covered in that time. The idea of the course was to cover the basics, stuff from before about 1965, before stability got its grip on the subject.

One of the slight novelties of the notes is that I treat the `1-quantifier-block' case. For instance, I discuss existentially saturated structures as well as the usual fully saturated structures.

The parts that have been written (mainly those parts that I needed for the course) are in a reasonable shape. However, they do need another seeing to. I was hoping to do this by teaching the course again some time, but I have not yet had that opportunity.

I have tried to make the notes suitable for self-study. Often these days departments do not have the manpower to put on such courses for small groups.
• Syntax and semantics
• Signature and language
• Basic notions
• Satisfaction
• Consequence
• Compactness
• The effective elimination of quantifiers
• The generalities of quantifier elimination
• The natural numbers
• Lines
• Some other examples
• Basic methods
• Some semantic relations
• The diagram technique
• Restricted axiomatization
• Directed families of structures
• The up and down technique
• Model complete and submodel complete theories
• Model complete theories
• The amalgamation property
• Submodel complete theories
• Companion theories and existentially closed theories
• Model companions
• Companion operators
• Existentially closed structures
• Existence and characterization
• Theories which are weakly complete
• Pert and buxom structures
• Atomicity
• Existentially universal structures
• A companion operator
• Existence of e. u. structures
• A hierarchy of properties
• Splitting with Good formulas
• Splitting with not-Bad
• Countable existentially universal structures
• Categoricity properties
• Existence of e. u. structures
• The construction of canonical models
• Omitting types
• The back and forth technique
• Homogeneous-universal models
• Saturation
• forcing techniques
• Ultraproducts
Each section (that has been written) has a decent selection of exercises with solutions available.

The current version is available from ModelTheory.dvi or ModelTheory.ps.gz or ModelTheory.pdf .

• Cut elimination in first order number theory
Chat to be written.

• The second order lambda calculus
When I was writing Derivation and Computation I intended to include something about the second order lambda-calculus. So I wrote myself a set of notes on the topic, something over 150 pages of development, exercises, and solution. These notes were not included in the book (for who needs a book that begins with propositional calculus and ends with the second order lambda calculus). However, I found by writing these notes I learned a lot, and they may be useful to other people. They are written using a judgemental style, influenced by the methods of Pure Type Systems. There is no macho stuff (like a proof of strong normalization) but they concentrate on how the system is used.

Some topics included are
• The typing disciple using a derivation system
• Derivation checking versus derivation generation
• Substitution into terms and under context (into derivations)
• Reduction of terms an computation
• Subject reduction
• Generating normal terms
• Simulation of the missing connectives (of conjunction, disjunction, and negation)
• An implementation of Godel's T within the calculus
• Natural number arithmetic within the calculus
• An implementation of ordinal arithmetic (the term calculus of Howard's system) within the calculus
• Ordinal notations within the system
each with a variety of exercises.

I haven't looked at these for several years, the parts are of variable quality, and some of the LeTeXing is a bit dodgy (and not in a fit state to be let off its leash). However, with encouragement I could be persuaded to knock up a decent version of these notes.
Harold Simmons