Naturalizing Natural Deduction

Abstract

A simplified and improved system of natural deduction for classical predicate logic is presented. The inference rules of existential instantiation EI, existential elimination ($\exists$ E), and universal generalization UG ($\forall$ I) are not employed in this system. Instead, a new proof-theoretic role for the quantifiers is introduced, which we call commonizing quantifiers. We argue that the commonizing quantifiers exemplify one of Frege’s basic insights by making explicit, in the context of natural deduction, the fundamental difference between the semantics of proper names and expressions of single or multiple generality. Arbitrary-object semantics, which is the best-developed philosophical justification of $\forall$ I and $\exists$ E and offers an explanation of the cumbersome restrictions placed on these inference rules, is discussed and criticized. It is argued that by looking at natural deduction in an intuitionistic rather than classical setting, it can be seen that the notion of an arbitrary object is not merely a harmless manner of speaking or notational variant, but a philosophical commitment that has consequences that are disguised if the discussion is framed only in terms of classical logic. In the system on offer, the notion of an arbitrary object is entirely dispensed with; in addition to considerations of simplicity, elegance, and parsimony, philosophical considerations decidedly favour the naturalized natural deduction system presented here.

Mathematics Subject Classification (2000). Primary 03A05 ⋅ Secondary 03B10

¹

For a philosopher teaching a first logic class to undergraduates, natural deduction systems for the standard, extensional sentential connectives are a beautiful thing. The standard introduction and elimination rules either represent patterns of inference of a familiar sort (as, for instance, modus ponens and conditional proof undoubtedly do), or are easily justified in terms of the “intended meaning of the connective” (as with “or introduction”). The rules are readily mastered by most students willing to put in a modicum of effort. The few simple rules are readily shown to be surprisingly powerful. And while the rules are usually introduced in a classical version alongside some version of two-valued truth functional semantics that purports to provide the meanings of these connectives, the introduction/elimination pairs make it easy to introduce alternative theories that spell out the meaning of logical particles in terms of their use, i.e., their inferential role.

Things are less happy when discussion turns to predicate logic. Partly, of course, this results from the increasing power of the system, which is paid for with increased complexity and the loss of certain nice properties (decidability, for instance). Some of the problems, though, do not have the same payoff. Standard versions of natural deduction extend the pattern of introduction/elimination pairs from the sentential operators to the quantifiers. While two of the resulting rules share the appealing features of familiarity and easy useability, two others involve complicated restrictions that make them difficult to use and to teach. Moreover, the benefits of preserving the pattern of intro/elim pairs for each operator are outweighed by substantial philosophical difficulties this approach involves.

Or so we shall suggest. In this paper we will introduce a modified system of natural deduction for classical predicate logic.² We offer this system for consideration and claim two advantages for it. While the system includes the familiar rules for existential introduction and universal elimination, the problematic rules of universal introduction and existential elimination are replaced. The first advantage of the system is that it is easier to use and to teach, at least based on the experience of one author over many years teaching the system to undergraduates after many prior years teaching standard natural deduction systems. The second advantage is philosophical. For one thing, giving up the easy intro/elim parallelism avoids the philosophical difficulties that come with it, and so restores the naturalness of the system by better reflecting unformalized but rigorous reasoning. For another, the usual explanations for the standard rules (but not our replacements for them) is philosophically dubious, requiring appeal to philosophically dubious arbitrary objects.

We will proceed as follows. First, we briefly indicate the aspects of standard natural deduction systems that create philosophical complications, describe some approaches offered as solutions to the problems, and describe some reasons for being unsatisfied by the solutions. We then describe some of the key features of the modified system, and give a few examples that illustrate its naturalness and ease of use. We conclude by indicating how the modified system “solves” the philosophical difficulties—by simply failing to raise them.

Problems of Standard Systems

In 1999, Jeffry Pelletier could quite plausibly say that natural deduction “is by now the most common way to teach elementary logic by far, and indeed is perhaps all that is known in any detail about logic by a number of philosophers (especially in North America)” [17, p. 1]. While in the intervening years, especially in texts that present a range of non-classical logical systems, trees, semantic tableaux and sequent calculi have perhaps become more common, natural deduction systems remain the first encounter with logic for many philosophy students. The virtues of natural deduction systems, at least for the classical propositional and predicate systems that are the centerpieces of most introductory formal logic courses for philosophers, are many. The basic rules of inference are, indeed, “natural” ones that are readily seen to reflect argument patterns in ordinary discourse; especially for systems that stick to Gentzen’s ideal of systems where the basic deductive behaviour of each logical operator is governed by introduction/elimination rules, students are well set up to understand subsequent discussions in philosophy of logic, while other common inference patterns are readily seen to be correct “derived rules”; and the systems are easy for students to learn, and easy for instructors to motivate.

Of course, these virtues are all only comparative, and involve trade-offs. It is easier for students to learn to do proofs in natural deduction than in axiomatic systems, but proving meta-theorems tends to be messier; compared to proof trees or semantic tableaux, natural deduction proofs are harder—though they look more like ordinary language arguments than trees do—while the meta-proofs are trickier. What we want to compare is not the usual presentations of natural deduction and other proof systems, but the usual presentations of natural deduction and our alternative version of natural deduction.

The teachability and transparent philosophical virtues of standard natural deduction systems decline markedly when one moves from propositional to predicate logic, as most who have taught the material will attest. The Universal Elimination ($\forall$ E) and Existential Introduction ($\exists$ I) rules share the virtues—seemingly obvious correctness, ease of application—possessed by most of the standard propositional rules.³ The same cannot be said for the partner rules. The restrictions and conditions for the application of universal introduction and existential elimination in the systems one finds in logic textbooks are unnatural and complicated, making them difficult to teach.

The complications are perhaps most evident in the existential case. While there are many differences of detail in the systems of natural deduction presented in various textbooks, differences small enough for us to ignore here, one must distinguish two quite different styles of treating existential elimination. We shall distinguish the styles by assigning different names to each.

The first approach, which following Pelletier we shall call “Quine systems,” uses the rule we shall call existential instantiation (EI, not to be confused with $\exists$ I). When applying this rule, one infers $\varphi (a)$ from $\exists x\varphi (x)$, provided certain restrictions, including that a be suitably “new” at that point of the derivation (e.g., that it does not occur in any assumption “active” at that point in the proof), are satisfied:

(1)

The first difficulty here is that the rule of inference is not actually valid. More precisely, the other rules of natural deduction systems satisfy the property that what is inferred by the application of a rule must be true in any interpretation that makes all the “active assumptions” at that point in the derivation true. Since a is new, we have no such guarantee. One of the supposed virtues of natural deduction is in danger here—lack of logical correctness makes a claim of “obviously correctness” hard to sustain. Quine’s approach is to adopt a method of flagging variables introduced by application of EI and declaring derivations “unfinished” if any such variable is free in the last line of the proof or any premise of that last line. Pelletier detects “a note of desperation” in Quine’s description of his approach [17, p. 13]. Desperation or not, the easy parallel to ordinary patterns of reasoning seems broken.

In the second approach, employed by what Pelletier calls “Fitch systems,” the term that is introduced when the existential quantifier is eliminated is introduced in an assumption that starts a new sub-proof. The rule requires that, under certain conditions designed to ensure that a is “new” and that it does not figure in unacceptable ways in ψ,

(2)

This rule perhaps matches ordinary language reasoning more closely. One readily imagines someone saying “Somebody has the property $\varphi$; let’s suppose it’s Bob …,” and so long as the conclusion drawn isn’t about Bob, we will, other steps in the argument being correct, accept the conclusion. Relatedly, this pattern of inference is valid in the sense in which EI was said above to be invalid.

Nevertheless, this approach has a further problematic feature, one shared with $\forall$ I and reflected in the complicated conditions for correct application of these rules. The role played by the term that is introduced in the existential elimination or replaced in a universal introduction is philosophically puzzling. Depending on the details of the system, the term is a variable or a name and the conditions ensure that it is “arbitrarily chosen.” As the normal semantic role of a variable or a name is to refer to an individual (under an assignment, in the case of a variable), the semantic role of an “arbitrarily chosen” term, especially when described, as it often is, as an arbitrary object, is problematic. The idea is that, one way or another, when a represents an arbitrary object in its occurrence in $\varphi (a)$, its role is not to designate a particular individual but to somehow stand in for the whole set of individuals with the property $\varphi$, which in the case where $\forall$ I is applicable, turns out to be the entire universe of discourse.

That there are philosophical problems in this neighbourhood should be of no surprise, as some of major figures in the history of philosophy have considered the matters carefully, and some have detected serious problems. One argument against arbitrary objects goes back at least to [4]. Berkeley quotes Locke’s description of the general idea of a triangle, which “must be neither oblique nor rectangle, neither equilateral, equicrural, nor scalenon, but all and none of these at once. In effect, it is something imperfect that cannot exist, an idea wherein some parts of several different and inconsistent ideas are put together,” pointedly adding the emphasis and asking the reader whether she can really imagine it. His point seems well captured with the slightly simpler example of an arbitrary integer:

In short, the notion of an arbitrary object, at least prima facie, leads to contradiction.

Moving forward a couple of centuries, Frege, for instance in [13], rejected the view that the variables of mathematics and logic have indefinite objects as their meanings analogous to the way proper names have definite objects as their meanings.

But are there indefinite numbers? Are numbers to be divided into definite and indefinite numbers? Are there indefinite men? Must not every object be definite? But is not the number n indefinite? I do not know the number n. ‘n’ is not the proper name of some number, definite or indefinite. And yet one sometimes says ‘the number n.’ How is that possible? Such an expression must be considered in context. … One writes the letter ‘n,’ in order to achieve generality. …

Naturally one may speak of indefiniteness here; but here the word ‘indefinite’ is not an adjective of ‘number,’ but an adverb of, for example, to ‘signify.’

Frege wishes to sharply distinguish the semantic relation involved in such expressions as

$$\displaystyle{ 5 + 7 = 7 + 5, }$$

(3)

from the semantic relation involved in expressions such as

$$\displaystyle{ x + y = y + x. }$$

(4)

Expression (3) does not express a universally general claim because the numeral expressions are names of their corresponding objects. The universal generality achieved in (4) is not, however, achieved by replacing definite objects with indefinite ones, that is, by regarding the variables ‘x’, ‘y’ as naming indefinite or arbitrary numbers. The semantic relation of expression (3) is one of “naming,” that of expression (4) is one of indefinitely signifying, indicating or referring. Frege suggests that there is a fundamental difference between the semantics of standard referring terms and the semantic account one must give of sentences containing multiple expressions of generality. The latter, but not the former, requires the notion of a domain of individuals over which an expression of generality ranges and the scope of such an expression of generality. Generality cannot be achieved, according to Frege, simply by an extension of the semantics of standard referring terms through an introduction of indefinite or arbitrary objects that are referred to by the variables of an expression.

Many subsequent philosopher-logicians have also argued against arbitrary-object semantics: for instance, [26, pp. 90–91], [28, pp. 4–5], [5, p. 13], [24, pp. 69–71], [25, pp. 134–137].⁴

Of course, arbitrary objects are not entirely without defenders. Kit Fine has presented a detailed account of an arbitrary object semantics, and provided a robust philosophical defense for it in [8–10]. According to Fine, arbitrary-object semantics is motivated by two things: First, it provides an explanation and justification of the various restrictions that must be imposed on the application of $\forall$ I and $\exists$ E. Without an explicit explanation and justification, Fine says, we would be left with a purely instrumental justification of these restrictions. Secondly, arbitrary-object semantics provides the underlying rationale for these problematic rules by providing us with an account of why they are truth preserving. At its very simplest, the idea is as expressed above: if a represents an arbitrary object in $\varphi (a)$, then it is associated with, i.e., refers to, the entire set of individuals that have a, rather than with any particular individual.

So construed, instantial terms appear not to function as individual terms at all, but instead seem to be expressions of generality. Echoing Frege, in his critique of Fine’s arbitrary–object semantics, King [18, pp. 254–255] observes:

In introducing new objects for quantifier expressions to refer to one assimilates the semantics of expressions of generality to that of standard names. …Surely, if anything, the introduction of referents for quantifiers obscures the differences between genuine names and expressions of generality by construing both sorts of expressions as referring terms.

However, the role these terms play in usual presentations of natural deduction leave them with certain deficiencies as quantifiers. If the term in question appears in the formula $\varphi (a)$, we are to suppose that a refers to something about which we know only that it is $\varphi$. But while the syntax of first-order languages clearly delineates, in a context-independent manner, the scope and force of ordinary quantifiers, the formulas containing instantial terms involved in applications of $\forall$ I and $\exists$ E do not provide any information, syntactic or otherwise, about the relative scope and force of these quantifier-like expressions of generality. Because of this, King refers to them as context-dependent quantifiers.

What is on offer here is a reformulation of natural deduction that learns the lesson of King’s Fregean critique of arbitrary-object semantics.⁵ That is, what this paper tries to achieve is a reformulation of natural deduction which makes explicit Frege’s basic insight by using rules which highlight the difference between the semantics of singular terms and expressions of generality. No instantial terms of the problematic sort, that is, no quantifier-like expressions in King’s sense, ever appear in a derivation. Instead, what are used are variables bound by what we call commonizing quantifiers in their stead. The result is that the scope and force of expressions of generality within a proof or subproof are syntactically transparent, thus answering King’s concern about the context dependence of the instantial terms of standard systems.

It may appear that we are simply accepting that King (and Frege) are right to reject Fine’s arbitrary object semantics, without a detailed investigation. However, with the system on offer, Fine’s case for arbitrary objects is undercut—neither of the rules that requires an arbitrary-object semantics for its legitimation occurs in the system. What motivates the claim of necessity for arbitrary-object semantics in the first place is the presence of the rules of $\forall$ I and $\exists$ E. Since the rules are not required for a satisfactory natural deduction system, and given the philosophically problematic nature of arbitrary objects, arbitrary object semantics lacks motivation.

The System

We focus here on the distinctive features of the system on offer. While there are differences of detail between systems in the literature that might make some of our proofs look odd to some, we doubt this will prove an obstacle for most readers. When displaying proofs, we will employ the method developed by Fitch [11], which is used in many popular texts and which we presume will be familiar to most readers.

Some of what we have to say applies equally to both the existential and universal quantifiers. To prevent unnecessary repetition, we shall use the symbol ∐ when a statement or rule holds for both the universal and existential quantifier.

The terms that are taken to designate arbitrary objects in standard presentations of natural deduction will here be replaced by bound variables. What allows a bound variable to play the role required is that they will not be bound by quantifiers that are part of the formulas in the proof. Rather, they will be bound by what we shall call commonizing quantifiers. Like the normal quantifiers, a commonizing quantifier has a well-determined scope. Unlike the normal quantifiers, the scope is not a formula, but a proof (or subproof).

To indicate the scope of a commonizing quantifier, we employ the familiar Fitch bar, which is standardly used to indicate that an assumption is made and how long the assumption is in force (or open). A commonizing quantifier ∐ v, can be placed where an assumption would normally occur in a Fitch-style proof—i.e., alongside a newly drawn vertical line and above a horizontal line. Of course, since what is being placed is merely a quantifier and not a formula, the Fitch bar is clearly being used for different purposes. We note the following:

• 1. The length of the vertical bar indicates the scope of the commonizing quantifier.

• 2. While it is a “legal” move to assume any formula at any time, there are some general conditions constraining when a commonizing quantifier can be introduced.

Graphically, the diagram below indicates that the scope of the commonizing quantifier ∐ v includes (the displayed occurrences of) $\varphi _{1},\varphi _{2},\ldots,\varphi _{n}$. The intended meaning is that, under the assumptions open at that point in the derivation, $\varphi _{1},\varphi _{2},\ldots,\varphi _{n}$ all hold for all/some v ∈ UD, respectively, if ∐ is $\forall /\exists$.

(5)

We say that the proofs in this system are such that no variable occurs freely, but this needs to be understood correctly. In general there will be open formulas occurring at various lines in the proof. But in all cases, all the free occurrences of variables on that line must be bound by a commonizing quantifier. It is useful to make a Local/Global Distinction.

• All variables in a proof are in the scope of either an ordinary quantifier or a commonizing quantifier.

• If the variable v lies in the scope of an ordinary quantifier ∐ v, then it is said to be locally bound by ∐ v, whose scope is a formula or subformula in the usual way. We may correspondingly say that the ordinary quantifier ∐ v is a local quantifier.

• If a locally free occurrence of v occurs in the scope of a commonizing quantifier ∐ v, then it is said to be globally bound by ∐ v, the scope of which is the proof or subproof as indicated above. We may correspondingly say that the commonizing quantifier ∐ v is a global quantifier.

• The system is designed so that in a correct proof if a variable v is locally free, that is, v is not captured by a local quantifier ∐ v, then v is globally bound, while if an occurrence of v is locally bound by ∐ v then it cannot be globally bound by a commonizing quantifier.

This has implications for the statement of the universal instantiation rule:

Universal Instantiation (UI)

We allow for the instantiation of any term t (constant, variable, or function term), provided that any free variable in t lies within the scope of some commonizing quantifier ∐. (As a result, genuine universal quantifier elimination occurs only in the case of universal instantiation with an individual constant.) Thus, we present the rule UI as follows, where t is a term:

(6)

provided that:

Universal Instantiation Conditions

• 1. If t has variables in it then all of the variables in t must be substitutable for v in $\varphi (v,v_{1},\ldots,v_{k})$, and

• 2. Each variable in t must be in the scope of some commonizing quantifier ∐ (to which reference should be made in the justification for universal instantiation).

It is worth taking a bit of care to make clear the conditions under which a commonizing quantifier may be introduced, and incidentally where the name “commonizing” comes from. Let’s begin with the universal quantifier. The idea of the commonizing quantifier is that it will pick out the class of objects in the domain which satisfy all the assumptions open at the point in the proof at which that quantifier is introduced. That is, any member of this class will have all the properties which the open assumptions require every object to have, but otherwise they can differ as much as you please. The general constraint for introducing a universal commonizing quantifier therefore is as follows:

Introducing a Universal Commonizer (UC)

(7)

We must of course prevent unwanted variable capture in the course of our proofs, and so adopt the following

Universal Commonization Conditions

• 1. v must not occur freely in $\forall v_{i}\varphi _{i}(v_{i})$, for all i ∈ { 1… k}.

• 2. v is substitutable for v _i in $\varphi _{i}(v_{i})$, for all i ∈ { 1… k}.

The idea here is, we hope, clear. We have ensured that v is available for “relabeling” the bound variable in any universal claim that has been shown to follow from the open assumptions at the point the universal commonizer is introduced. Hence in the scope of the commonizing quantifier we can make any of the universal claims of v. (Strictly speaking, the inclusion of the lines justified by UC _n are merely a convenience, since $\varphi _{n}(v)$ could be derived at that point using reiteration and universal instantiation.)

Note that if $v_{1} = \cdots = v_{k} = v$ then conditions (1) and (2) are automatically satisfied. Moreover, there need not be any universal claims $\forall v_{i}\varphi _{i}(v_{i})$ (i.e., k may be zero), in which case we may commonize as follows:

(8)

Given this description of the conditions governing the introduction of a commonizing universal quantifier, the conditions for existential commonization will be no surprise.

Introducing an Existential Commonizer (EC)

(9)

Existential Commonization Conditions

• 1. u must not occur freely in $\forall v_{i}\varphi _{i}(v_{i})$ (for all i ∈ { 1… k}) nor $\exists v\varphi (v)$.

• 2. u is substitutable for v _i in $\varphi _{i}(v_{i})$, for all i ∈ { 1… k}, and substitutable for v in $\varphi (v)$.

• 3. One cannot existentially commonize on u within the scope of a existential commonizer $\exists u$—roughly, one cannot existentially quantify on the same variable twice.

Once again, if $v_{1} = \cdots = v_{k} = v$ then conditions (1) and (2) are automatically satisfied, in which case one may existentially commonize on v.

As in the case of universal commonization, it is of course possible that there not be any $\varphi _{i}(v_{i})$ (that is, k = 0) or $\varphi (v)$, so the following is an allowable pattern of commonization.

(10)

Of course, just as rules that begin with assumptions also must specify the conditions under which the assumption is discharged, our rules must specify the conditions under which the commonized variable is “discharged.” We call this step “decommomization.” We state the general form of the rule, then note the special case that very often is the one applied in practice.

Universal Decommonization (UD) and Existential Decommonization (ED)

(11)

We display this proof with a single conclusion, but the system allows more than one formula to be inferred by decommonization from a single subproof.

More importantly, it may be that v does not in fact occur freely in ψ, in which case the quantifier attached by commonization is vacuous. In such cases, we allow as a special case of the decommonization rules that ψ may be inferred without attaching the vacuous universal/existential quantifier.⁶

(12)

Instantiating a Universal Commonizing Quantifier

It would clearly be problematic if the following proof were correct.

(13)

We clearly don’t want a system in which one can derive, for example, “For any integer n, if n is even, then 3 is even.”

The reason such proofs are not correct in this system have to do with the scope of commonizing quantifiers, and the requirement of uniform substitution. Just as we may not infer from $\forall x(P(x) \Rightarrow Q(x))$ that $P(a) \Rightarrow Q(x)$, but instead must uniformly replace x by a when applying $\forall$ E, similarly when we instantiate on a universal commonizer we must uniformly replace all occurrences of the variable bound by the commonizer. In general, since the scope of a commonizing quantifier is a proof or subproof rather than a formula, the result of a uniform substitution will be a proof or subproof and not a sentence.

In practice, universally instantiating on a commonizing quantifier will not often be of much use. However, we can illustrate its application with a simple example⁷ in which we may prove $\varphi (a_{2}) \Rightarrow \varphi (a_{2})$ in either of the following two ways:

(14)

(15)

In (15) we have used a universal instantiation for the commonizing quantifier $\forall v$; paying attention to the requirement of uniform substitution, the subproof 5–7 is an instance of 2–4. We then can infer line 8 by UD.

Discussion of Examples

We turn now to presenting a few examples that will allow us to illustrate some features of the system on offer, and contrast it to other systems. Let us start with a very simple example. In most textbooks the proof of

$$\displaystyle{ \{\forall x(F(x) \Rightarrow G(x)),\exists xF(x)\} \vdash \exists xG(x) }$$

(16)

would look something like the left side of (17), in which the third line introduces an auxiliary assumption which says that an arbitrarily selected object a has F. On the other hand, thanks to the introduction of a commonizing quantifier on line 3, the derivation on the right of (17), does not invoke the notion of an arbitrary object.

(17)

We next look at a proof of

$$\displaystyle{ \neg \forall x\neg P(x) \vdash \exists xP(x) }$$

(18)

The proof in [1, p. 358] appears to share similarities to ours, but the philosophical story behind it is problematic. They place [c] on the Fitch bar, and interpret it as follows: “Let c denote an arbitrary object satisfying P(c)”.

(19)

Given what we have said above, it will not surprise anyone if we say we find this problematic. We find the words of Rescher [25, p. 137] apt:

When one introduces random individuals, one can do so meaningfully only subject to the self-denying ordinance represented by the convention that: Nothing is to be said about a random individual that is not intended about ALL of the individuals of the domain at issue. A random individual is therefore not a thing but a linguistic principle, a shorthand device for presenting universal statements.⁸

We agree. The universal commonizing quantifier is just the tool to make this intention clear, and for the case in question it does so as follows:

(20)

One sometimes hears logicians defend or explain the role of an appeal to arbitrary objects in natural deduction reasoning by reference to the frequency with which one will hear mathematicians say things like “since x was arbitrarily chosen, …” in the course of a proof. Whatever one thinks of the tendency to defer to mathematical practice in other domains such as the philosophy of mathematics, we find it unpersuasive as a general rule in logical matters. It doesn’t take much familiarity with some parts of the mathematical literature to realize that many mathematicians routinely ignore the use/mention distinction. Not many logicians would use this as a reason to embed such disregard in logic. It’s therefore unclear why we should embed arbitrary object semantics into a system of natural deduction based on a mathematical manner of speaking, especially when examples like the one above show that it is quite avoidable.

As a final example, we will show a proof in this system of the theorem that Pelletier focuses on in [17], his informative historical study of natural deduction. It is a useful example because it involves appeal to “arbitrary objects” in both their universal and existential forms in a single short proof. It thus provides an illuminating contrast of the various attempts to implement arbitrary object reasoning in a number of systems, including the “flagging” methods introduced by Quine and Suppes, Fitch’s and Copi’s systems, and so on.

$$\displaystyle{ \emptyset \vdash \exists x\forall yR(x,y) \Rightarrow \forall y\exists xR(x,y). }$$

(21)

(22)

Our inclination is to find this proof perspicuous compared to those in the other systems, and we invite readers to compare it with those for other systems presented in Pelletier’s paper.

Hilbert’s Epsilon Operator and Ambiguous Names

We find the case made above, based on arguments offered by Frege, Rescher, King et al., persuasive. It suggests that one should adopt the naturalized version of natural deduction described here, even if it were harder to teach. Coupled with the need for complicated restrictions in order for natural deduction systems involving arbitrary objects to be correct, which seems to make the present system easier to teach and to learn, there is much to recommend the system we offer. We turn now to a different sort of objection to natural deduction systems that rest on the idea of arbitrary objects.

The objections to arbitrary objects given above can be broadly regarded as metaphysical. The present objection strikes us as perhaps even more important in a logical context. The objection appeals to some results, well known in the specialist literature but not as widely known to non-specialists as they should be, which show that, even apart from philosophical justification, using bound variables and invoking arbitrary objects are not mere notational variants of one another—there are differences in logical potency between the two. Discussing the difference against the background of classical logic disguises this fact, as the differences of potency are masked by the extra logical power provided by indirect proofs (or, equivalently, accepting double negation elimination or excluded middle). Instead, we will look at intuitionistic logic.

As a preamble to our argument, we again refer to Pelletier’s useful history of natural deduction. Pelletier notes that Patrick Suppes, in his presentation of natural deduction, employs what he calls ambiguous names as a “technical device” to aid in the statement of the quantifier rules. While Suppes takes the notion of ambiguous names to be “apparently new” in the literature on first-order logic, he says “the central idea of this approach is related to Hilbert’s $\varepsilon$ symbol.” The basic idea of the epsilon symbol was that for any predicate F(x), “ ‘$\varepsilon xF(x)$’ was to designate ‘an arbitrary or indefinite F’ about which nothing was known other than that it was an F” [17, p. 22]. Rather than introducing Hilbert’s term-forming, variable binding operator $\varepsilon$, Suppes introduces orthographically distinct “names”⁹ to play this role.

Hilbert’s symbol was introduced in an axiomatic presentation of logic. Suppressing some details, the fundamental axiom governing its behaviour is:

$$\displaystyle{\exists xF(x) \Rightarrow F(\varepsilon xF(x))}$$

The epsilon term $\varepsilon xF(x)$ has no free variables, so this axiom scheme picks out a class of sentences, one for each formula F(x) with at most one free variable. Suppes’ orthographically distinct “ambiguous names” are introduced when an existential quantifier is eliminated, and a name new to the proof is selected each time. Now, the syntax does not make explicit that α is an arbitrary F in the way the syntax of $\varepsilon xF(x)$ does. However, in the context of the proof, when α appears in F(α) due to the application of EI to $\exists xF(x)$, it is clear that α functions no less as an arbitrary F than $\varepsilon xF(x)$ would.

Next, we want to say a few words about why pointing to the effects of including arbitrary objects in intuitionistic logic is not unnatural in a discussion of natural deduction. As [17] notes, if one looks back to one of the two pioneering works of natural deduction, [14], one sees that the basic system Gentzen develops is the one he calls LJ, i.e., a natural system for intuitionistic predicate calculus. To get classical logic from LJ Gentzen considers two approaches, each of which requires giving up some nice feature of LJ—either its axiom-free nature, or the uniform intro/elim pairs for each logical operator. Gentzen opts for the former, adding the law of excluded middle as an axiom scheme.¹⁰ Right from the inception of natural deduction, then, one can see good reasons for regarding intuitionistic logic as the most natural version of natural deduction. Arguments to this effect do not go away in philosophy. One sees, for example, kindred claims in [7] that the rules of intuitionistic logic are harmonious in a way that classical rules are not. We do not want to wade into those deep waters here. We merely claim that considering the effects of arbitrary objects in intuitionistic logic is not “changing the subject.”

Thirdly, as is well known, while the addition of Hilbert’s $\varepsilon$ operator to classical logic is conservative—that is, it does not allow us to prove anything that was not already provable, other than formulas that include epsilon terms—the addition of epsilon terms is a non-conservative extension of intuitionistic logic. It obviously allows the derivation, for instance, of $\exists y(\exists xF(x) \Rightarrow F(y))$. Starting with some interesting papers written by J.L. Bell, some less obvious and more interesting non-conservativeness results have been proved for the addition of $\varepsilon$ in intuitionistic logic. For instance, given certain modest assumptions, the intuitionistically invalid form of De Morgan’s law is provable if epsilon is present, but not when it is absent. For discussion of such results, see [2, 3, 6].

Putting some pieces together, the non-conservativeness does not depend on the specific presence of epsilon terms. For instance, $\exists y(\exists xF(x) \Rightarrow F(y))$ is clearly also provable if we adopt “ambiguous names,” as described by Suppes, in an intuitionistic system: assuming $\exists xF(x)$, one may infer F(α), so by $\Rightarrow$ I arrive at $\exists xF(x) \Rightarrow F(\alpha )$. By $\exists$ I, we have the result. Indeed, the result is likely to be provable in any Quine system of natural deduction, i.e., any system that incorporates a version of EI, barring the addition of significant additional constraints on the use of the rule.

The lesson here, we think, is that the metaphysical language in which talk of arbitrary objects is couched is not logically inert, and so is no mere philosophical façon de parler. The addition of excluded middle to intuitionistic logic greatly strengthens the logic—it turns it into classical logic. The extra power conferred by the addition of excluded middle masks the extra-power conferred by the addition of arbitrary objects. Moreover, what is hidden is something of considerable philosophical significance—by assuming the existence of arbitrary objects, we are making an assumption that increases logical power. Talk of arbitrary objects does not explain correct quantificational reasoning, because it implies more than correct quantificational reasoning alone implies. We think that this is good reason, when teaching logic to new philosophers, to dispense with this dispensable and misleading way of speaking.

Of course, our system is equivalent to what Pelletier says “could be called ‘Gentzen systems,’ ” [17, p. 12], i.e., those systems which include $\exists$ E instead of EI. Gentzen systems, starting with LJ, yield intuitionistic logic, and so no such non-conservativeness results are in the offing. The crucial feature that makes this so is that the terms that seem to refer to arbitrary objects occur only in assumptions and in formulas within the scope of those assumptions. Such systems, at least with respect to the existential quantifier, seem closer in spirit to what we suggest here. When we know $\exists xFx$, we can interpret the rule as merely allowing us to “give a name” to one of the Fs as a convenience. It seems, then, that the commitment to the existence of “an arbitrary F” is less robust than in a Quine system. For the universal quantifier, though, terms seeming to refer to arbitrary objects are not always in the scope of an assumption in this way, even in Gentzen systems, so let us turn to consideration of the universal quantifier.

It is probably a familiar thought among those who have taught standard natural deduction systems that the instantial terms in $\exists$ E and $\forall$ I behave quite differently, and so it may not mean the same thing when we call each sort of object “arbitrary.” We think that this suspicion is quite right, and think that considering Hilbert’s epsilon operator together with another operator sometimes discussed by Hilbert and his collaborators, viz., the τ-operator, in intuitionistic logic helps make the point clear. The τ operator is governed by the axiom dual to epsilon,

$$\displaystyle{F(\tau x.F(x)) \Rightarrow \forall x.F(x).}$$

Once again, the extra strength of classical logic paints over an important difference. In classical logic, the two operators are interdefinable. For instance, one can set

$$\displaystyle{\tau xF(x) =\varepsilon x\neg F(x).}$$

In intuitionistic logic, this is no longer so. Not only are the two operators no longer interdefinable, but while they are both non-conservative over intuitionistic logic, they give rise to different logics. For a simple example, [2] shows that τ makes provable the “infinite De Morgan’s law”

$$\displaystyle{\neg \forall xP(x) \Rightarrow \exists x\neg P(x),}$$

while epsilon does not. We see, then, that the assumption of “arbitrary objects” of the relevant sort for the two quantifiers are both non-conservative assumptions over intuitionistic logic, but each in different ways. This justifies the suspicion that there is an important difference between the two types of arbitrary object.

Once again, of course, the Gentzen rules for the existential quantifier must be weaker than τ, since after all LJ is intuitionistic logic. The fact that commitment to arbitrary objects as seen in Quine systems is non-conservative in intuitionistic logic seems to us a strong objection to such systems. How, though, do the considerations above add up to a justification for adopting the natural deduction system on offer here, rather than the Gentzen systems equivalent to it that include the usual $\exists$ E and $\forall$ I rules? If $\varepsilon$ and τ are indeed reasonable mechanisms for indicating “an arbitrary F” (in two different senses), then the uses of instantial terms in Gentzen style $\exists$ E and $\forall$ I do not accurately reflect the idea of arbitrary objects. Since the only reasonable story on offer for the use of those terms in natural deduction systems, whether classical or intuitionistic, is in terms of arbitrary objects, we conclude that there is no good philosophical story to justify using a system with such terms.

Conclusion

We have presented a modified version of natural deduction which we suggest has a number of virtues. One of us has used the system for years in introductory logic classes, and finds it easier for students to learn than standard natural deduction systems for classical logic. It is, we think, a more accurate reflection of rigorous but informal reasoning, and in this sense restores some of the naturalness that is supposed to be one of the selling points of natural deduction in the first place. Finally, it is a system that does not require a philosophical story that conflates the semantics of singular terms and general expressions, nor does it require appeals to the dubious entities sometimes called “arbitrary objects.” The arbitrary object justification is problematic, among other reasons, because seriously supposing the existence of such objects increases the number of valid inferences beyond standard quantifier rules (though this effect is disguised in the presence of excluded middle), so they are not a suitable tool to justify standard quantificational logic.