Abstract:
Suppose we have a language involving non-denoting singular terms.
(The language of everyday mathematics provides one example. Terms
like \(\frac{n}{m}\) and \(\lim_{x\to\infty} f(x)\) do not denote, for
appropriate choices of \(m\) and of \(f\).) It is not too difficult to
define inference rules for an appropriately free logic that incorporates
non-denoting terms. If \(t\) does not denote, then \(\phi(t)\) need not
entail \(\exists x\phi(x)\), and neither is \(\phi(t)\) entailed by
\(\forall x\phi(x)\). We now have a very good understanding of well-behaved
cut-free sequent calculi for a variety of different free logics, appropriate
for languages with non-denoting singular terms.
There is a tradition, in proof-theoretic semantics, of thinking of well-behaved
inference rules for some concept as defining that concept. If the rules are
well-enough behaved (whatever that notion of good behaviour might be—whether a
notion of harmony, or conservative extension and unique definability, or
something else—then we are tempted to take the concept that can be introduced
by such rules to be defined by them, and hence to be apt for introduction to
our vocabulary.
In this talk, I will show how, in a simple negative free logic, we are
nonetheless able to—in some sense—define “outer” quantifiers \(\Pi\) and \(\Sigma\)
where \(\phi(t)\) entails \(\Sigma x\phi(x)\), and is entailed by \(\Pi x\phi(x)\),
since the rules for such quantifiers meet all the strictures for defining
concepts in proof-theoretic semantics mentioned above. I will discuss the
significance of this result for proof-theoretic semantics and our understanding
of how inference rules might be used in definitions.
