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

- 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

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

- 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
- Adjunctions
- 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

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**

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

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

- Cut elimination in first order number theory

- The second order lambda calculus

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

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 Last modified: Thursday 23 February 2006