Nonexistence Identity and existence
Partial functions
We have already enriched our logical language by adding function symbols, and consequently relaxed the ALLE and SOMEI rules slightly to allow arbitrary terms to be substituted for the variables. However, it is built into the natural deduction calculus in this form that all terms succeed in referring to something. The introduction rule for the existential quantifier, for instance, allows us to argue in one step from F(f(a)) to SOMEx F(x), on the grounds that what is true of f(a) is thereby true of something. However, in many circumstances, we may want to use function symbols without the assumption that the functions they denote have values for every possible argument. In the domain of persons, for example, "spouse_of" may be useful for specifying relationships, but some people have no spouse so we don't want to regard it as picking out a spouse for everybody. A function is total if it is required to have a value for every possible argument, or n-tuple of arguments, and partial otherwise. For a partial function, like the square root function in rational arithmetic for example, we cannot apply SOMEI as above, since this would allow the inference from a true statement such as "There is no rational number equal to √ 2 " to the clearly false "There exists a rational number x such that there is no rational number equal to x". Something has to change.
We have seen that definite descriptions can be accommodated in first order logic, by introducing a new symbol "" in one of two ways. It can be taken to form genuine singular terms, so we can write
(x. x2 = 2) > 1.3
for instance, where the expression in the parentheses stands for "the number whose square is 2" and functions like a name. Alternatively, it can be taken to form quantifiers, in which case we rather write
(x : x2 = 2) (x > 1.3)
to say "For the number, x, whose square is 2, ...". Either of these formulae might represent the claim that the square root of 2 is greater than 1.3. It is reasonable to expect our treatment of function symbols, especially if we allow these to stand for partial functions, to be essentially the same as that of the corresponding definite descriptions. Definite descriptions as quantifiers will not be explored further in these notes: for present purposes, we follow standard mathematical practice by regarding function symbols as producing singular terms, syntactically similar to names.
The most convenient way to amend the natural deduction calculus in order to accommodate partial functions, along with non-referring definite descriptions if these are taken to be terms, is to restrict the SOMEI and ALLE rules to the case where the term involved does have a referent, and the simplest ways to achieve this are either to restrict the rules to names only or to require an extra input line on which the object in question is asserted to exist.
We examine the latter option first. It is easy enough to enrich the language with an existence predicate 'EST', meaning "there Exists Such a Thing as..." and to use this to make the required extra assertions. The elimination rule for the universal quantifier now reads:
| ALLv A | EST(t) | ALLE | |
| Atv |
The extra condition prevents us from proving that the President of Australia exists (i.e. is identical with something in the domain of discourse):
SP { ⊢ SOMEx (p(a) = x)} PL { } {1} {a = a} {=I} PL { } {2} {SOMEx (a = x)} {1 SOMEI} PL { } {3} {ALLy SOMEx (y = x)} {2 ALLI} PL { } {4} {SOMEx (p(a) = x)} {3 ALLE} EPThis derivation is fine as far as line 3, which records the theorem that everything in the domain is identical with something in the domain. However, line 4 is not correct: obviously it is not a theorem of logic that the President of Australia is identical with something that actually exists. The inference step from line 3 to line 4 is not allowed unless we have the additional premise that p(a) exists.
The existential introduction rule has to be refined similarly:
| Atv | EST(t) | SOMEI | |
| SOMEv A |
This blocks the even shorter proof:
SP { ⊢ SOMEx (p(a) = x)} PL { } {1} {p(a) = p(a)} {=I} PL { } {2} {SOMEx (p(a) = x)} {1 SOMEI} EPNames, unlike other function symbols, are still guaranteed to refer, so for this version of logic we must add one more rule of EST-introduction, similar in style to =I. For any name m:
| EST-I | |
| EST(m) |
There is no need for a partner elimination rule, as the amended ALLE and SOMEI rules fill that role. Note that m has to be a name: for obvious reasons, it is not legitimate to substitute a term like p(a) for m in an application of EST-I.
With these rules, it is easy to prove, for any term t, that EST(t) is logically equivalent to SOMEx(x = t). Note, however, that F(t) does not entail EST(t), and consequently NOTEST(t) does not entail NOTF(t). In general, this version of our logic makes no assumptions about the truth values of formulae containing symbols for partial functions or non-denoting definite descriptions. In particular, we take no side in any debate over whether things have to exist to have properties. We allow that arbitrary atomic formulae involving compound singular terms may be true, or may be false, independently of whether those terms denote anything. If we wish to go along with Russell and mark all atomic formulae containing non-denoting terms as false we can do so, but the logic itself does not force us in that direction.
Somewhat surprisingly, the alternative approach, of restricting ALLE and SOMEI to names only rather than arbitrary terms, is entirely equivalent to adding an existence predicate as above. As noted, EST(t) is provably equivalent to SOMEx (x = t). If EST is not added to the language, therefore, we might still hope that it could be emulated by using this equivalent formula instead. To see that indeed it can, we only need to show that EST-I is not required and that the versions of ALLE and SOMEI involving EST are derivable anyway using SOMEx(x = t) in place of EST (t).
The effect of EST-I is easily obtained: the theorem SOMEx(x = m) is an immediate consequence of m = m by SOMEI restricted to names. To mimic the rule
| Atv | EST(t) | SOMEI | |
| SOMEv A |
we need to derive SOMEvA from Atv and SOMEx(x = t). This is quickly done. Suppose the premises of the rule are derivable from X and Y respectively, and that m does not occur in X. Then:
SP {Atv, SOMEx (x = t) ⊢ SOMEv A} PL {X} {1} {Atv} {supposed} PL {Y} {2} {SOMEx (x = t)} {supposed} PL {3} {3} {m = t} {A} PL {X,3} {4} {Amv} {1, 3 =E} PL {X,3} {5} {SOMEv A} {4 SOMEI} PL {X,Y} {5} {SOMEv A} {2, 5 [3] SOMEE} EPSecuring the effrect of ALLE with EST is similar. The upshot is that it does not really matter whether we take EST as a new predicate and use it in the rules or whether we simply restrict the rules to apply to names only. Either way, partial functions can be accommodated along with whichever theory of definite descriptions we prefer.
Free Logic
Among function symbols, names still have special status in logic as outlined above. Each name is guaranteed by the definition of interpretations to refer to something in the domain, whereas in general singular terms may fail to do so. Such names are sometimes called "logically proper names" in the literature of philosophical logic, and contrasted with ordinary proper names in natural languages, which may fail to refer in some circumstances. In the present section, we consider relaxing this stipulation about names.
There are several reasons why we might want to do this. In the first place, many theorems of ordinary predicate logic have as their main operator an existential quantifier. For example: SP { ⊢ SOMEx (Fx IMP Fx)} PL {1} {1} {Fa} {A} PL {} {2} {Fa IMP Fa} {1 [1] IMPI} PL {} {3} {SOMEx (Fx IMP Fx)} {2 SOMEI} EP
Thus it is provable, as a matter of sheer logic, that something or other exists, that the universe is not empty. Well, it is true that the universe is not empty, and we might look for metaphysical arguments for supposing this truth a necessary truth. What is unsettling about the logical guarantee of existence, however, is that logic delivers only bare existence, telling us nothing about what exists. Metaphysical arguments for the necessity of existence are usually attempts to prove that there must be things of some special kind: physical objects, spacetime points, minds, God, numbers, sets, René Descartes or whatever. Logic will have none of this; provably something exists, but nothing provably exists. This is odd.
Another oddity arises from the existential import of universal quantification. The provable sequent
ALLx Fx ⊢ SOMEx Fx
attests to the fact that 'all' implies 'some', that whatever is true of everything is, as a matter of logic, true of at least something. That might not be a bad claim for logic to make, but note that there is no analogous claim in cases of restricted quantification. We cannot validly argue from the assumption that all footballers are bipeds
ALL (x: Fx) Bx
to the conclusion that some footballers are bipeds
SOME (x : Fx) Bx
because logic (rightly) leaves open the possibility that there be no footballers at all. There is thus an awkward difference between the logic of 'footballers' and the logic of 'things' which is rather unpleasing.
Yet a third cause for concern is orthodox logic's unconvincing treatment of the problem known picturesquely as 'Plato's Beard'. This is the problem of how we can truly say of something that it does not exist. The standard example in the philosophical literature is Pegasus, the mythical flying horse. Pegasus does not exist, but in order to say so we need to use the name 'Pegasus'. Now if names get their meaning by referring to objects, this particular name must fail to get a meaning, and so it cannot be used meaningfully to say anything at all. The problem generalises to that of giving an account of the meaning and use of non-referring names (and hence, presumably, of all names) in arbitrary contexts, not just in the context '...does not exist'. Logically proper names are always guaranteed to pick out exactly one thing, so names like 'Pegasus' are taken by orthodox logical theory either to be unformalisable or to be short for descriptions (so 'Pegasus does not exist' really means 'There are no flying horses' or something like that). But there appears to be no ground other than sheer dogma for holding vacuous names to be unformalisable, while the view that they are translatable as descriptions runs into the problem that the descriptions can't be completely spelt out in practice—and even if they could be spelt out, there would be no principled choice of which of the many possible descriptions of flying horses or similar beasts is the phrase abbreviated by 'Pegasus'.
|
|
|||||||||||||
|
|
|||||||||||||
One way of addressing the above worries is to change orthodox logic a little, giving what is known as Free Logic. The amendments this time go further than those suggested in the last section. As before, we use the expression EST as a monadic predicate to say that things exist, but this time we do not have the rule EST-I, since we wish to allow names to be vacuous, just like any other terms. Then the quantifier rules are revised as shown (freeRules). The usual side conditions on occurrence of m for ALLIf and SOMEEf apply, as the name involved must be typical. The extra input lines for ALLE and SOMEI amount to the principle that they only apply to objects that exist. This is needed because free logic allows empty names like 'Pegasus' and we do not want to allow such arguments as
Pegasus is mythical
Therefore something mythical exists
Nor do we want to argue by ALLE
All horses are flightless
So if Pegasus is a horse, Pegasus is flightless
The rules ALLI and SOMEE, which rely on the special status of names, now need to be strengthened. They have an extra assumption of EST(t) which is discharged in the application of the rule. Again, this amounts to the point that the quantifiers only range over what exists. In order to conclude that all horses are flightless we need only know that a typical existing horse is flightless, since those are all the horses there actually are, Pegasus notwithstanding.
SP {ALLx (Fx IMP Gx), SOMEx Fx ⊢ SOMEx Gx} PL {1} {1} {ALLx (Fx IMP Gx)} {A} PL {2} {2} {SOMEx Fx} {A} PL {3} {3} {Fa} {A} PL {4} {4} {EST(a)} {A} PL {1,4} {5} {Fa IMP Ga} {1, 4 ALLEf} PL {1,3,4} {6} {Ga} {3, 5 IMPE} PL {1,3,4} {7} {SOMEx Gx} {4, 6 SOMEIf} PL {1,2} {8} {SOMEx Gx} {2, 7 [3,4] SOMEEf} EP
An example of their use in proofs is more useful than a
verbal explanation of the free logic rules. freeProof
should be compared with the usual classical proof of the
same sequent. We cannot just pick 'a' as the name
of an F and use it to show that a G
exists, for we also have to assume that it exists (line
(4)). The need to assume existence in order to make the
quantifier rules work means that one extra line number has
to be given in the annotation each time. Line (8) comes
from the two input lines (2) and (7) discharging
assumptions 3 and 4. Most standard proofs can be
reproduced in free logic by making similar small
modifications.
Most but not all: perhaps more interesting than the question of which ordinary sequents can still be proved is that of which cannot. Among the unprovable sequents are the following:
⊢ EST(a)
⊢ SOMEx EST(x)
⊢ SOMEx (x = x)
ALLx Fx ⊢ Fa
Fa ⊢ SOMEx Fx
ALLx Fx ⊢ SOMEx Fx
p OR SOMEx Fx ⊢ SOMEx(p OR Fx)
The unprovability of these reflects two features of free logic: that it allows the empty universe (witness the second, third and last sequents) and (consequently) that names may be used in true atomic sentences without referring to any existing thing. Notice that if nothing exists at all, then for any formula A containing a name m the universal ALLx Axmis true while the existential SOMEx Axmis false. This means that, for example, ALLx (Fx AND NOTFx) has a model in free logic!
The last sequent is worth another look. The key point is that p does not entail SOMEx(p OR Fx) in free logic, because in the empty domain p could be true while every existential formula is false. For essentially the same reason, ALLx(p AND Fx) does not entail p. The empty domain can be excluded by adding the assumption implying that something exists, so the sequent
p, SOMEx Gx ⊢ SOMEx(p OR Fx)
is valid, for instance, as is
ALLx(p AND Fx) ⊢ p OR ALLx Gx
Note that according to free logic everything exists: ALLx EST(x) is a theorem, even though EST(a) and SOMEx EST(x) are not. Make sure you understand why.
The motivating worries with which this section began are now less bothersome than they were. That something exists is no longer provable, so there is no longer a puzzle as to why this should be a logical truth when nothing in particular has to exist. The asymmetry between restricted and unrestricted quantification in respect of existential import has now vanished, also because the empty universe is tolerated. As for Plato's beard, well it has been trimmed at least. We can allow non-referring names into the language without getting obvious nonsense. We have a perfectly straightforward way of saying that Pegasus does not exist using the formula NOTEST(p). There is still some difficulty over the truth value of 'Pegasus is winged'. Since Pegasus is not part of the furniture, it looks as though he is winged or wingless not in virtue of the way the world is but in virtue of the contents of a myth. Note that free logic is neutral between the many views of this situation: it could be held that the name 'Pegasus' denotes nothing at all, and that some (not all) sentences containing it have their truth values fixed not by the mechanism of reference but by the myth, or it could be held that 'Pegasus' does denote something—it denotes a non-existent flying horse of which the myth is a true description. It could also be held, in the manner of Russell on definite descriptions, that nearly all atomic claims about Pegasus are actually false because there is no referent for the name. Free logic allows all of these views to be modelled, without adjudicating between them.
Notes and further reading
Free logic as presented here is one of several logical systems designed to allow for reference failure. Free logics differ from each other along two main axes: whether or not they allow the empty domain to count as a model, and whether their quantifiers range only over existing things. For an account of the field by one of its leading developers, see Karel Lambert's overview paper Lambert01 and collected essays Lambert03.
Fictional objects are particularly interesting from the point of view of their logic. We can reason logically about them in much the same way as we can about real objects, but they do not exist, and are unlike real objects in important respects. There are many attempts in the philosophical literature to describe the semantics of fiction, and some difficult puzzles which such attempts must face. The Stanford Encyclopedia article by Fred Kroon and Alberto Voltolini Kroon is a good entry to the literature and to some of the issues arising.
One of the views attacked by Russell when he introduced his theory of definite descriptions was that of Alexius Meinong jungle who held that objects can "be" without existing, and that names (and definite descriptions) refer to them in exactly the same way as they do to objects which exist in the real world. In the light of the existence of alternative accounts such as Russell's, there is no need for Meinongian semantic theory, so it has long appeared discredited. Some recent philosophers have tried to rehabilitate it, however, so it still makes appearances in the philosophical literature.