One of the comments at the discussion raging at Vallicella's site illustrates perfectly the 'translation problem' that I mentioned in an earlier post. The problem is that any attempt at 'proving' or 'disproving' an ordinary language statement by using the well-defined proof procedure of the modern predicate calculus is highly vulnerable to the process of interpreting the ordinary language statement in the calculus. If the interpretation is not correct, then the proof, though perfectly valid, may be proving the wrong thing.
Suppose we want to prove the validity of an ordinary language consequence having the following form.
(*) If it was the case that A was identical with B then it is the case that A is identical with B
We can try to do this by translating the placeholders A and B (which substitute for grammatically singular OL terms) into the 'a' and 'b' of the predicate calculus (which substitute for logically singular terms), and translating the tensed statements of OL into the 'nec' or 'necessary' of predicate calculus, as follows:
(1) a=b (Assumption for conditional proof)
(2) a=b -> (Fa -> Fb)
(4) a=b -> (Nec(a=a) -> Nec(a=b)) (Substitution Instance of (2))
(5) Nec(a=a) -> Nec(a=b) (Modus Ponens, 1&4)
(6) Nec(a=b) (Modus Ponens, 3&5)
(7) a=b -> Nec(a=b) (Conditional Proof, 1-6)
The problem is that the 'proof', if understood as a proof of the ordinary language consequence, can't possibly be valid. Substitute 'the president of the US' for 'A' and 'John F. Kennedy' for 'B' to give
(*) If it was the case that the president of the US was identical with John F. Kennedy then it is the case the president of the US is identical with John F. Kennedy
But ex vero nunquam sequitur falsum: the false cannot follow from the true. Whenever the antecedent is true and the consequent false, consequentia non valet, the consequence is not valid. But the antecedent is true - the president of the US was (in September 1963) identical with John F. Kennedy, and the consequent false - the president of the US is (in September 2010) not identical with John F. Kennedy. So the consequence is not valid. If the formalised part of the proof is valid (which I am not denying), it follows that the translation of our ordinary language consequence into the formal consequence (i.e. (7) above) is wrong. But that is just the place we forgot to look.
At this point, the formalist will object that the translation "would be accepted by just about anybody who knows how to translate from ordinary language to formal logic". And that is another problem: a cultural problem, not a logical or philosophical one. We were taught as students the 'correct' way to translate awkward and messy ordinary language statements into the clean language of MPC. I too was taught this (using what was only 10 years old then, but has since become a classic text) quite some time ago. Having learnt this, we 'know' how to translate from ordinary language to formal logic. And, proud of this knowledge, we are now 'anybody who knows', and we can put down anyone who does not know.
What a formidable barrier to progress.