First of all, Hi Pierluigi. How are you? I miss those cog sci discussions with you, Todd, and the rest of the crew (: Okay, you're a good philosopher, so here's a philosopher's argument, contra your position, Adam's, etc about the putative failures of the logicist camp (hope that term will work for you).
Allow me a brief detour here so that I might make my case a bit more clearly later. Call a 'Type-A' construct Bill's axiom:
(=> (and (parentOf ?x ?y)
(age ?x ?x-age)
(age ?y ?y-age))
(> ?y-age ?x-age))
Call a 'Type-B' construct any procedure coded in a standard programming language (I'm abstracting away from details about code here-OOP principles or not, language variations, interpreted versus compiled expressions.) Since it would be silly to paste in some huge chunk of source code, here's a ridiculously simple example that will do just fine for our purposes:
While (i < 100) {
Cout << "Hello SUO!\n";
++i;
}
Now, I take it that your claim is that Type-A constructs either haven't been conclusively discounted as valuable to the 'Real People' (RP) community, or that they in fact are valuable, and it will all be revealed in due course. I'll argue against both disjuncts.
For starters, the obvious thing to note here is that the burden of proof ought to lie with the Type-A proponents. That is a no-brainer: remember we're talking about the RP-community. They regard Type-B stuff as the lingua franca of their field--and it is. So Type-B is (trivially) valuable to their field (i.e., their field is constituted by Type-B constructs).
Now consider Type-A. What can be said in its defense? We can start with what's already been proffered by you and Adam Pease. What is that? A host of practical considerations: Type-A proponents have suffered from lack of focus on RP problems, insufficient funds, poor marketing, and even inadequate processor speeds (my favorite). This position isn't so much immune to argument as it is immune to conclusive argument-but that is all that's required for your purposes. I might claim that I have the genetics to run a marathon in three and a half hours. When someone points out that, well, it's been a year and I still weigh 240 pounds, had asthma as a child, and have never successfully run more than 5 miles without stopping since I was thirteen, I just need my list of practical excuses. No one can give me anything like a counterexample, because my whole training regimen thus far has really been just a string of partial successes, and anyway I'm working in it! W!
hen I get enough money to get that new sports drink, and the sneakers...
Okay, you get the point. The upshot is: it's a burden of proof argument, and all evidentiary considerations point away from the viability of the Type-A program for assisting the RP crowd. Demanding "proof" of this negative claim, or acting as if the onus lies on the RP crowd or the Type-A critics is just abdicating the real responsibility and obfuscating where the real problems lie.
What else can be said in defense of Type-A? One thing I hear often is that a FOL axiom will give you new facts you may not immediately want, but that you just might need later. You show a little of this spirit, when you offer that:
Ah! But isn't that the point: that the statement (the
rule) could be_used_ in any of a great variety of ways, most of
which having nothing to do with the original intent of the asserter?
All well and good, but count on the RP crowd to be mighty skeptical. For one, the very reason they love Type-B so much is that there's a way of consistently solving the class of problems they need solved. To put it more directly still, the RP crowd needs to get consistently and reliably from some input M to some output O. That's just the way it is when you're a "real person." What motivates the Type-A proponents to bear down and keep going in spite of this simplicity (and hence increased visibility with failure) is not that the Type-A construct will beat Type-B at its own game-getting to N from M in demonstrably better fashion, that is. Rather, it is this faith in the superior expressivity of declarative approaches, embodied in Type-A constructs, that keeps it all going. This expressivity is a noetic notion; it allows one to say much more stuff about a domain (and hence at least humans will know more about the domain by inspection of formalisms). That is, ip!
so facto, a great thing. But for the purposes of the RP community, it's apples instead of oranges.
And therein lies the rub: what is the connection between declarative power and inference? How exactly is superior expressivity supposed to solve practical inference problems for the RP crowd? The Type-A crowd acts as if by the fact of declaration alone, we all ought to be excited about the inferential possibilities. But no one has bothered to show exactly how this is so. Maybe it's because they can't. And this is where the history of failures becomes relevant: it's not for lack of trying, is it? (Is it really just for lack of trying?). Prima facie, If I told you that the way to get more Y (inference) is to throw all your time at X (FOL declaration), but gave no recipe for how X relates to Y and couldn't demonstrate this recipe over time, wouldn't you be sceptical? (Well, maybe I forget myself).
So I conclude that the Type-A proponents are missing a crucial premise in their argument, namely: "The Type-A construct really is suited for a computer (Turing machine) to turn its expression of facts into a powerful set of problem solving inferences, reliably and usably, for the RP crowd." This case hasn't been made. And given the evidentiary considerations to the contrary, and therefore the shift of the onus of proof onto the shoulders of the Type-A proponent, this argument is practically dead, or at least on life-support. Maybe someone can revive it. It will take more than additional talk about expressiveness.
cheers
Erik