Say we have some type
p over
A,M. Then
p is a collection of
formulas. What do these
sentences say? At the very
least, they are consistent with
ThA(M). In other words,
p says everything that
M does
about A.
In addition,
p may have some other
formulas. These
formulas use the
language LA, so they, too, may reference elements of
A. However, these
formulas also have free variables; for a
model to
satisfy p it must find a
satisfying tuple
v for these free variables. And elements of
v may lie outside of
A. Hence,
p is in essence a characterization of
v with respect to A.
I also have an example. Say
M=R and define the 1-type over
N
p(x)={x>1}∪{(n>1→x<n):n∈N}
this gives a characterization of a value
x that it is greater than 1 but less than every real greater than 1. Intuitively, we are characterizing
x to be the infinitesimal value
x+ε.
Doing so
really does require usage of types, or at
least 1-ary
LN-
formulas. It may seem like we could somehow characterize
1+ε with a plain 1-ary
L-
formula as follows:
p(x)=(x>1)∧(∀n)(n>1→x<n)
This fails, however, because
n ranges over the entirety of our domain, which is not what we want. For instance, in
R this
sentence is not
satisfiable because
R contains no infinitesimals. But
even in
R (ie,
R with infinitesimals), this
sentence is
still not
satisfiable because now
n ranges over the infinitesimals
as well as the reals.
In
order to characterize
x as an infinitesimal we want to ask for infinitesimals to be in the domain of the
satisfying model (so that
x exists) and want to ask for
x to
act a certain way
with respect to the reals but
not the new infinitesimals. Hence we need to work in
LN.