From wild mathematical universes back to nothing much at all: the question of empty domains in first-order logic. Not that I have anything very insightful to say: but I want to get my mind clearer before committing myself to a line in IFL2.
In his nice book Logic (1977), Wilfrid Hodges introduces a tableau system with the following four rules for dealing with quantifiers. Two rules allow us to push a negation past a quantifier — so given 
on a branch you add 
, and dually. Then the rules for dealing with bare quantifiers are as follows. Given 
on a branch, you can add 
for any 
already featured on the branch. While given 
on a branch, you can add for some which is not already used on the branch.
Compared with the standard rules for tableaux as in e.g. Jeffrey’s Formal Logic: Its Scope and Limits (1967/1981), Hodges’s quantifier instantiation rules are a tad neater, indeed elegantly symmetric — simply: instantiate universals with old names, existentials with new names.
Using ‘
’ for provability in Hodges’s system, we notably do not get 
. But that is all to the good, Hodges thinks. That inference fails if we allow the empty domain. “Many logicians add one further derivation rule, which has the effect of decreeing that every domain of quantification has at least one individual in it. From our point of view this would be a mistake. A domain of quantification can perfectly well be empty — as it well may be if the conversation turns to discussing intelligent life on other planets.”
At first blush this is very neat — a more inclusive logic and more elegant rules. What’s not to like? But there’s a price to pay, though. As David Bostock points out in his Intermediate Logic (OUP 1997), in Hodges’s system we do get e.g. 
and 
so transitivity of derivability fails; and there are other nasty effects. Such consequences do seem pretty unhappy. Bostock diagnoses the source of the trouble to be Hodges’s half-way-house position of wanting to accommodate empty domains while his logic requires that names have denotations. Allow empty names too and of course both and fail, and transitivity can be restored.
And indeed, leaving aside nasty effects like transitivity failure, it is difficult to see why it should be a desirable feature of a logic that it allows empty domains but not empty names. After all, if “the conversation turns to discussing intelligent life on other planets” it could equally (back in the nineteenth century) turn to discussing the intramercurial planet Vulcan, or (later) turn to discussing Ern Malley (among poets) or Nat Tate (among painters) or Frederick R. Ewing (among novelists). And if our logic has functions, then we can find ourselves unwittingly discussing partial functions so using more terms which fail to have references. If we want to avoid the mishap of talking of things that don’t exist, then surely we’ll want to avoid not just wholesale foul-ups (empty domains) but local foul-ups (empty terms). If we push Hodges’s rationale for allowing empty domains to its natural conclusion, then, it seems that seems we have to go the full revisionary hog and be free logicians. But free logics — while not horrendous — haven’t the elegant simplicity of Hodges’s system. Do we really have to end up there? Not in an introductory book, that’s for sure! To be continued …
Footnote: what is the natural deduction analogue of Hodges’s system? I think this works: take the usual sort of 
-elimination rule (given start a subproof with with new …), let the 
-elimination rule allow just instantiation with respect to names already appearing (not in finished subproofs), and add the two rules, from 
infer 
and its dual. But I guess this isn’t an entirely natural presentation of a natural deduction system, if we like thinking Gentzen-style of introduction rules as more fundamental, as meaning-fixing, and elimination rules to be justified as being in harmony with them.
What does Hodges do in his Model Theory (or in the Shorter version)?
I have a vague memory that he allowed empty domains, but I don’t have even that about how he handled names.
Since I don’t have copies handy, I resorted to looking online. In both versions of the book, Hodges allows empty domains, and in the definition of a structure, the constants (constant symbols) name elements of the domain (so those names, at least, aren’t empty).
I agree with Bruno Whittle in finding this very natural. I don’t think it makes sense to have empty names, and I don’t see the failure of
as a price. Instead, it should fail.
That does leave a question of how to account for seemingly empty names in natural language (such as Vulcan, etc above), but I don’t think they have to be treated as empty names in our formal logic.
Yes, I was wondering about what Hodges does in his Model Theory, and as you say he allows empty domains but not empty names there. I’ll need to think some more about the significance of this. For the moment, just one point. I realise I misleadingly expressed myself: I didn’t mean that, by itself, the failure of
by itself is an issue — I meant that the failure of that in the presence of 
and 
in Hodges’s system gives us failure of transitivity, and that is a price we may be unhappy to pay. I’ve moved a sentence to make that clear.
So what’s your line, I wonder, about dropping transitivity of deducibility? Or about failures of modus ponens: we have, in Hodges’s system
, 
), but not 
. Do you bite those bullets?
I’m not sure how you or Bostock get
. Since 
doesn’t let you introduce a new name, 
, it must be something else plus 
that gets you to 
and thence to 
.
However, I don’t think it matters very much whether a tableaux system that Hodges happens to use in a popular-level introduction to logic has such problems. That’s one reason why I wondered what he did with names and domains in his Model Theory books. I don’t think he specifies any particular formal proof system in those books, though, so it might be difficult to work out whether the way he conducts proofs runs into any similar problems.
We have A proves C in Hodges’s system if the tableau starting A, ¬C closes. Start a tableau
and we have a name now available on the branch at the point where we want to instantiate the quantifier and thereby close the tree. Giving the result Bostock and I note.
Without a pretty close read, I wouldn’t like to take a bet on whether what Hodges actually does in reasoning about mathematical structures empty domains in his Model Theory requires deviating from standard logic (any more than doing set theory and reasoning about the empty set requires requires deviating from standard logic!).
I don’t seem to be able to reply directly to your reply, so I’ll reply to my own post instead.
To me, the questionable part is including
at the start, so that it appears that an 
exists even if one doesn’t. But I don’t know what else might have to change if that isn’t allowed.
Hodges’ position seems very natural to me. Indeed, I think that while there is an analogy between empty names and a type of quantifier, it is not the one that you (Peter) suggest—and it seems to point in a quite different direction.
Thus, on a plausible way of thinking about things, to give the meaning of a name is to provide it with a referent. So to ban empty names is simply to restrict attention to those which have been given meanings. On the other hand, to give the meaning of a quantifier is to provide a domain, where this can be thought of as providing a property, or perhaps a set. But then, since there are of course empty properties and sets, banning empty domains amounts to ruling out quantifiers which have apparently been given perfectly legitimate meanings.
The analogue of an empty name does not seem to be a quantifier with an empty domain, it seems rather to be one without a domain.
But then there is no good reason why admitting empty domains should lead one to admit empty names.
There is also of course the case of partially interpreted function symbols, but, again, these seem to be analogous not to quantifiers with empty domains, but rather to quantifiers whose domains are partial sets (i.e. sets whose characteristic functions are partial).
The position that the analogy between names and quantifiers seems to put pressure on is not Hodges’s but that of the free logician who countenances empty names, without extending the same courtesy to domainless quantifiers.
What would doing the latter look like? Well, if one thinks that all atomic sentences with empty names are false, for example, then perhaps one should think the same about all universal or existential sentences whose initial quantifier is domainless. So the quantifiers would no longer be duals, etc.!
Interesting! “To give the meaning of a quantifier is to provide a domain, where this can be thought of as providing a property, or perhaps a set.” Wouldn’t it be more natural to say, in the spirit of your remark about the meaning of a name, that to give the meaning of a quantifier involves providing a domain, where this can be thought of a providing some objects for the quantifiers to run over. (“Everyone is ready to start!” Who? “Those guys”, “The people lined up at over there”, “The candidates”.) A property F might get into the story because we very often use a plural description The Fs to pick out the relevant objects. Sets get into the story because of our singularist prejudices or because sets are our standard way of regimenting talk about many things at once (take your pick!). But neither properties nor sets are what domains are — they are objects, plural.
If you think of fixing the semantic significance of a name as providing it an object to refer to, and fixing the semantic significance of a quantifier as providing it with some objects to run over, then — it would seem — treating the empty cases analogously is natural.
So if I’m to jump in your direction, and reject that parallel, I guess I need a good reason for thinking of fixing the semantic significance of quantifiers your way.
I would be happy to do things plurally—I don’t think it affects the point.
In those terms, I would say that to give the meaning of a quantifier—to ‘provide it with a domain’—is to specify zero or more objects for it to range over. To insist that one specify at least one seems barely more natural than insisting that one provide at least two (i.e. that one really does provide objects plural!)
However one thinks about domains, it seems to me that the analogue of failing to provide a name with a referent is to fail to determine which objects a quantifier ranges over. And that is hardly something one can be accused of, if one has made quite clear that it does not range over any!
Perhaps you have not gone the whole hog. If one wishes to accommodate the empty domain and to allow empty terms, then one might find it natural to relax bivalence for those formulae that contain constants or free occurrences of variables, while retaining it for other formulae. Of course, one is then left with the problem of handling the failures of bivalence appropriately in the tree decompositions, and I imagine that there would be a number options, each with its particular warts.