The syntax semantics interface

This was a comment on  "The syntax semantics interface" but it ended up too large to be a comment.

My earlier comment applies here too, so you have to reword my observation to admit "syntactic entailment" as "derivability".

Thomas Forster seems to me to have things the wrong way round, for often enough once the semantics is in place you are scuppered on getting a complete notion of derivability within the usual constraints (essentially that proofhood is decidable and hence the set of theorems effectively enumerable).

If the true sentences are effectively enumerable then people will expect to see a complete deductive system and hence "|-" = "|=", and noone would think of that as "cooking the books".

The way to cook the books is to debase the semantics.
The best known example of this is second order logic.
Under its traditional (or "standard") semantics this logic is necessarily incomplete, since the truths are not enumerable (and there is a categorical finite axiomatisation of arithmetic, which would make arithmetic truth decidable if the logic were complete).

Then there was the Henkin semantics for second order logic, relative to which the usual deductive system is complete.  This works by admitting more models, so that every sentence which is not derivable has a counterexample, and hence is not logically valid, and we pretend it doesn't matter that we can't prove it.

This apparent gerrymandering becomes institutionalised in what I call "analytic semantics" (because I don't know that there is a term for it).
Which is what semantics became in mathematical logic.

This is a part of the process of formalisticisation of mathematical logic, in which logicians decouple from problems which cannot be dealt with formally.
The easiest examplar of this is the idea that questions in set theory are completely resolved if one knows which of the following three possibilities is the case:

A a positive answer is provable in ZFC
B a negative answer is provable in ZFC
C the problem is shown (in ZFC) to be independent of ZFC

In the case of the Continuum Hypothesis (CH) case C holds, so the problem (many think, including Thomas Forster) is solved.  But some of us think that we ought to interpret set theory relative to a semantics in which it makes sense to say, "OK, we know its independent of ZFC, but is it true?" and who suspect that Cantor would not have been satisfied by the independence result.

Going back to "analytic semantics", the formalistic turn in mathematical logic (which probably dates from mid 20th century) means that they are not interested in prescribing a semantics for languages like higher order logic.  Their interest is exclusively in the analysis of the kinds of things which the logic could be about.  Semantics then is not the assignment of meaning to a language, but rather the analysis of what meanings it could have and the deductive system still be sound.  If you do this analysis correctly then you end up, whatever the deductive system, with a "semantics" relative to which the deductive system is sound and complete.

Of course, this kind of semantics is a million miles from Grice, purely mathematical, no place for intentions (not even in the semantics of an intensional language).  Its also a long way from Carnap, who was into prescriptive semantics, even if these things were only "proposals".

A next entertaining step is to deny that second order logic (with the standard semantics) is a logic at all.
This is a redefinition of the term "Logic" which defines out the possibility of an incomplete logic.
There have been extended debates on FOM on whether (standard) second order logic is a logic, with Harvey Friedman leading the party for its rejection (which is not supposed to be a choice, but an objective fact, "standard second order logic" is not actually a logic, it is a semantics which lacks a deductive system).

Thomas does point out (in an odd way which probably results from his consorting with the theoreticians in the computer lab) that you can't always fix it up.
You should probably understand his reference to "rectype" as admitting that the required deductive system might not be effectively enumerable.

RBJ