On Aug 19, 2011, at 4:30 PM, Pat Hayes wrote:
On Aug 19, 2011, at 2:56 PM, Christopher Menzel wrote:
...There is Stewart Shapiro's excellent "Foundations without Foundationalism," an extended defense of the thesis that second-order logic is indeed logic.)
Ah, but Stu *defines* HO logic as any logic which quantifies over properties, so on his criterion CL would be a higher-order logic.
Yes but IIRC he also defends full second-order logic as deserving of the name, which was the thesis that got John's dander up.
In fact, he refers to the Henkin model theory "for second-order logic", which would be an oxymoron if one takes the view (as you do, and I do on even-numbered days of the month) that Henkin logic is essentially first-order.
True, I have been known to say that, even on odd-numbered days of the month, but I have to admit it is too ham-handed. Pretty clearly, what Stewart means there by "second-order logic" is a certain language + proof theory — propositional logic + the usual axioms for predicate quantification + comprehension principles (+ optional identity theory). That is a perfectly legitimate thing to call "second-order logic". At the same time, there is another legitimate target, namely a certain language + model theory (for which there is no consistent, complete proof theory). I myself tend to reserve the name for the latter, for a variety of (mostly aesthetic and pragmatic) reasons.
All of which goes towards my point, that one has to be very careful, when talking about the 'order' of a logic, to know exactly what one means. I have been taken to task by some very competent logicians for calling CL first-order, as they are using a purely syntactic criterion of order. Nobody is right in debates like this, but clearly the terminology lacks precision.
As you suggest in your sign-off, there really isn't a significant debate here, just a quibble about how to use the term "second-order logic".
OK, no more from me on this fascinating, but ultimately purely historical/terminological discussion.
Perhaps the best thing to do is scotch "second-order logic" altogether and simply use the terms "second-order proof theory" and "(full) second-order model theory".