🚀 go-pugleaf

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?

Any enlightenment would be greatly appreciated.

Joe Dzikiewicz