🚀 go-pugleaf

dzik@access.digex.com (Joseph Dzikiewicz) writes:
: I have come across two uses of the term "type theory" in logic that seem
: to be referring to different things.
: 
: In one, Type Theory seems to relate to the rules for higher-order-logics
: (ie, second order logic and up).  This is discussed in Peter Andrews'
: book "An Introduction to Logic and Type Theory: To Truth through Proof."
: I have also seen it referred to as "Church's Type Theory."
: 
: In the other, types are sets of formulas in first order logic.  This
: is discussed in some detail in Chang and Keisler's book "Model Theory."
: 
: Am I correct in thinking that these are two different things with the same
: name, or are they the same thing presented differently by two
: different groups of authors?

Type theory *is* higher-order logic, where the types are used to
avoid the paradoxes. One version -- the one Andrews explains --
is Church's Simple Theory of Types. There are others -- the Ramified
Theory of types (Ramsey) and the original, Russell's type theory.

The Simple Theory of Types is just Predicate Calculus 
enriched with typed lambda calculus. 

Types themselves can be thought of as sets, with a little care, 
depending on how you want to give the *semantics*. Chang and Kreisler
deal with models, Andrews with the logic. 

But, ahem, types pitch up all over the place: they just prevent certain
things (eg. applying a function to the wrong arguments) from happening.
Eg. types of variables in computer languages.

Gavan Tredoux
UCT