“So the question you asked me last time was, ‘Why does anyone bother with first-order logic at all, if second-order logic is so much more powerful?’”
For what it’s worth, mathematicians care about first-order logic because it satisfies nicer theorems than second-order logic, in the same way that mathematicians care about Lebesgue integration because it satisfies nicer theorems than Henstock-Kurzweil integration. The statements that mathematicians talk about in many contexts are first-order anyway, so we might as well figure out what there is to say about first-order statements so we can apply it to the relevant situation (in the same way that the functions that mathematicians want to integrate in many contexts are Lebesgue integrable anyway, so...).
In mathematics there is usually a tradeoff between generality and power: the more general a theory is, the less it can say. That’s why abstract algebra textbooks generally talk about groups instead of monoids even though the latter are more general: there are lots of nice theorems about, say, finite groups that just fail miserably for finite monoids, and so it’s much harder to say nontrivial things about finite monoids than it is to say nontrivial things about finite groups.
And first-order logic is a surprisingly powerful tool in pure mathematics: in the guise of model theory it has lots of interesting applications, e.g. Hrushovski’s proof of the Mordell conjecture over function fields.
I do not think the situation is as simple as you claim it to be. Consider that a category is more general than a monoid, but there are many interesting theorems about categories.
As far as foundations for mathematical logic go, any one interested in such things should be made aware of the recent invention of univalent type theory. This can be seen as a logic which is inherently higher-order, but it also has many other desirable properties. See for instance this recent blog post:
http://golem.ph.utexas.edu/category/2013/01/from_set_theory_to_type_theory.html#more
That univalent type theory is only a few years old is a sign we are not close to fully understanding what foundational logic is most convenient. For example, one might hope for a fully directed homotopy type theory, which I don’t doubt will appear a few years down the line.
Sure. It has of course been the case that careful increases in generality have also led to increases in power (hence the weasel word “usually”). There is something like a “production-possibilities frontier” relating generality and power, and some concepts are near the frontier (and so one can’t generalize them without losing some power) while some are not.
For what it’s worth, mathematicians care about first-order logic because it satisfies nicer theorems than second-order logic, in the same way that mathematicians care about Lebesgue integration because it satisfies nicer theorems than Henstock-Kurzweil integration. The statements that mathematicians talk about in many contexts are first-order anyway, so we might as well figure out what there is to say about first-order statements so we can apply it to the relevant situation (in the same way that the functions that mathematicians want to integrate in many contexts are Lebesgue integrable anyway, so...).
In mathematics there is usually a tradeoff between generality and power: the more general a theory is, the less it can say. That’s why abstract algebra textbooks generally talk about groups instead of monoids even though the latter are more general: there are lots of nice theorems about, say, finite groups that just fail miserably for finite monoids, and so it’s much harder to say nontrivial things about finite monoids than it is to say nontrivial things about finite groups.
And first-order logic is a surprisingly powerful tool in pure mathematics: in the guise of model theory it has lots of interesting applications, e.g. Hrushovski’s proof of the Mordell conjecture over function fields.
I do not think the situation is as simple as you claim it to be. Consider that a category is more general than a monoid, but there are many interesting theorems about categories.
As far as foundations for mathematical logic go, any one interested in such things should be made aware of the recent invention of univalent type theory. This can be seen as a logic which is inherently higher-order, but it also has many other desirable properties. See for instance this recent blog post: http://golem.ph.utexas.edu/category/2013/01/from_set_theory_to_type_theory.html#more
That univalent type theory is only a few years old is a sign we are not close to fully understanding what foundational logic is most convenient. For example, one might hope for a fully directed homotopy type theory, which I don’t doubt will appear a few years down the line.
Sure. It has of course been the case that careful increases in generality have also led to increases in power (hence the weasel word “usually”). There is something like a “production-possibilities frontier” relating generality and power, and some concepts are near the frontier (and so one can’t generalize them without losing some power) while some are not.