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