First, I have to give a little background about free logic; the point of this post comes towards the end. In model theory for classical logic, every name (= individual constant) is interpreted by exactly one object (in the domain of quantification); colloquially: the name ‘Chicago’ picks out exactly one thing -- the spatiotemporal object Chicago. Free logic relaxes this assumption, by allowing individual constants to be associated with no objects (in the domain of quantification). The rationale here is that some names do not successfully pick out anything in the world (think about ‘Santa Claus’, ‘Pegasus’, or ‘Planet Vulcan’), and since we don’t always know which of our terms are genuinely referential and which ones fail to refer, perhaps we should not build it into our logic that every name in fact refers. (There is another motivation for free logic as well: that we should allow models whose domain of quantification has cardinality zero, since it’s not a matter of logic that at least one thing exists in the universe.)
When we allow names that can refer to nothing into our language, the usual deduction rules have to be modified. In particular, the following (classically valid) argument form is invalid (where a is an individual):
All x are F
Thus, a is F
If a is a non-denoting name, then the premise can be true and the conclusion false or truth-valueless (depending on your preferred semantics for sentences containing non-denoting names). So in short: allowing non-denoting names forces us to give up the usual ‘All’-elimination rule (a.k.a. ‘Universal Instantiation’) just above.
I have recently been thinking about languages in which we relax the classical univocality assumption for names in the ‘other direction’: that is, languages containing terms that refer to more than one thing. (I gave them the uninspired tag ‘Multiply-Referring languages.’) The point of the formal exercise is to model ambiguous or confused terms. I have already developed a family of model theories for such languages (published in JPL last year), and am currently thinking about proof systems.
Back to free logics for a moment. There are three species of semantics for free logics: negative, neutral, and positive. They are distinguished by how they treat atomic sentences containing non-referring names. Negative: all false; neutral: all truth-valueless; positive: at least one atomic sentence with a non-referring name is true. For example, consider ‘Pegasus=Pegasus’: negative semantics declares this false, neutral semantics declares it truth-valueless, and positive semantics declares it true. I take this tripartite characterization straight over into multiply-referring languages.
Now here, finally, is my point. In positive multiply-referring languages without identity, the above rule of Universal Instantiation is valid. And, as far as I can see, all the other classical rules are valid (=truth-preserving) as well. Which means, surprisingly (to me), that the classical introduction and elimination rules for FOL without identity all are also valid rules for positive multiply-referring langauges. More simply, allowing ambiguous names into an otherwise classical language without identity makes no difference to validity. (At least in the sense of truth-preservation; it does mess up ‘backwards-falsehood-preservation,’ for reasons I won't detail here.)
But things change once an identity predicate is introduced into the language. Universal instantiation becomes invalid: ‘Everything is not identical to a’ is true if a is multiply-referring, but ‘a is not identical to a’ is not true. This raises a question for me about the best way to construct the proof system here: put roughly, is the problem with universal instantiation, or with identity? Both of them have to be present to generate the invalid argument form, so which is the one that should be altered? I’ve never tried to make my own proof theory before, so I don’t know how one should proceed under such circumstances. Any thoughts?