Quantified predicate logic where the quantified terms are only
subject terms and no
predicates. A standard abbreviation in mathematical logic is FOL.
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
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
Also, it is an interesting fact that standard
set-theory is a first-order 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 n-ary predicates. Or briefly, because
in 'x e z' one can use 'z' much as if it is a predicate of 'x' and definable
Likewise, having Higher Order Logic one can set up in it equivalents of set
theory (without using the set-theoretical primitive 'is element of' or by