A Quick Guide to my Notes on Logic written around 1999, with a gentle disclaimer: There may be mistakes in these notes, and these mistakes are my fault. I strongly encourage those interested to read the original sources.

Notes on Automated Theorem Proving

History

von Heijenoort From Frege to Godel is a collection of early papers on logic.

The Collected Works of Gerhard Gentzen contains a historical account of Gentzen's work along with his papers (including his paper on cut-elimination).

Basic Logic

Ebbinghaus, Flum, Thomas argue that first order logic is the best possible logic.

Andrews builds up from propositional and first order logic to higher order logic.

Type Theory

Russell created Ramified Type Theory and Wiener simplified it by reducing relations to predicates.

In 1940, Church introduced his type theory based on simply typed lambda calculus.

Andrews proved cut elimination for a sublogic of Church's Type Theory called Elementary Type Theory

Andrews' book studies Church's Type Theory in the formulation Q_0.

Miller extended Herbrand's Theorem to Elementary Type Theory using expansion trees.

Leivant surveys results in higher order logic using Schutte's relational formulation (using comprehension instead of lambda calculus).

Lambda Calculus

Barendregt is the standard reference for the untyped lambda calculus.

Huet discovered a preunification algorithm for the simply typed lambda calculus.

Hindley studied simply typed lambda calculus using Curry-style type assignments.

Prehofer's book includes unification results.

Category Theory

Dana Scott used cartesian closed categories to interpret lambda-theories and topoi to conservatively extend those lambda-theories to intuitionistic higher-order theories.

McLarty and Goldblatt both have books introducing categories and topoi in an elementary fashion (i.e., delaying the use of functors).

Lambek and Scott give a quick overview of portions of category theory from a more functorial point of view.

Polymorphic Lambda Calculus

Reynolds 89 gives a quick introduction. Reynolds 83 discusses what a parametric model should satisfy (the Abstraction/ Logical Relations Theorem).

Notes on Cognitive Science

Notes on Machine Learning