First Order
Logic: In
logic:
Quantified predicate logic where the quantified terms are only
subject terms and no
predicates. A standard abbreviation in mathematical logic is FOL. It
is a fairly interesting fact that First Order Logic (and Propositional
Logic) sort of chrystallized out of considerably more powerful and complicated systems (of
Frege and of Russell and Whitehead) as systems that were interesting in their own
rights.
There are a number of interesting results about FOL, notably by Lindström,
that show that FOL is in some  technical  senses optimal given its means and
restrictions.
Also, it is an interesting fact that standard
settheory is a firstorder theory (but
not pure predicate logic, since it is based on the
primitive "is an element of").
This also means that in set theory one has a considerable amount of
something much like higher order logic, since one has something like the
equivalent for any predicate P(x1 .. xn) by defining p = x1 .. xn : P(x1 ..
xn) and using (x1 .. xn)(p)( (x1 .. xn) e p > .... ) ) where ( (x1 .. xn) e p
> .... ) ) will be a formula about all nary predicates. Or briefly, because
in 'x e z' one can use 'z' much as if it is a predicate of 'x' and definable
by abstraction.
Likewise, having Higher Order Logic one can set up in it equivalents of set
theory (without using the settheoretical primitive 'is element of' or by
defining it).
