Quote:
So, herbzet, when people say "second-order logic" these days they're
usually talking about what you get if you take first-order logic for a
two-sorted language and add full comprehension for the set variables.
Now, that's not semantically complete, there are sentences which are
valid with respect to the standard semantics but not provable in this
system. I think that first became clear with Gödel's work on the
incompleteness of arithmetic together with the categoricity of second-
order arithmetic.
Does that make things a bit clearer?