Introduction

In Chapter 2, Leary develops a deductive system. The aim here is to develop a deductive system that is independent of the semantics developed in chapter 1. A deductive system will specify the conditions under which a sequence of formulas in a language counts as a deduction (also known as a derivation or a proof).

Leary's system is different in a number of ways from Barwise and Etchemendy's (or those in other basic symbolic logic texts written by philosophers). Some of the differences of detail will emerge below, as we examine Leary's system. But a few points are worth mentioning immediately.

1. Unlike B&E's system, Leary offers an axiomatic system. That is, in addition to rules of inference, Leary has axioms which count as part of the formal system.

2. Like most mathematicians, and unlike most philosophers who write about logic, Leary is not much concerned with evaluating natural-language arguments. Philosophers are typically interested in determining under what conditions a conclusion can be said to follow from a collection of premises. In general, these premises will be contingent truths, things that may be true but could have been false. For instance, we may want to know whether the sentence Tet$(a)$ is a consequence of the premises $(\forall x)($Large$(x) \to$ Tet$(x))$ and Large$(a)$. Now, it is certainly not necessary in any sense that either of these premises is true, but we can still investigate whether the conclusion can be deduced from the premises. Mathematicians tend not to worry about cases like this. Their concern is mathematics, where all the sentences of interest are either necessarily true or necessarily false. Thus, when Leary discusses the notion of a deduction of $\phi$ from $\Sigma$, written $\Sigma \vdash \phi$, he describes $\Sigma$ as a set of ``nonlogical axioms". This is a good term to describe, say, the axioms of set theory or number theory, or even sentences such as $(\forall x)(\forall y)($Larger$(x,y) \to$ Smaller$(y,x))$. But it's not a good term to describe the premises of an argument if these premises are not necessary truths.

   This is only a terminological point, however; the system will work fine whether $\Sigma$ consists of nonlogical axioms or of other sentences we might want to use as premises. It's just that a class of cases that is extremely important to philosophers seems to rather drop out of view for mathematicians.

3. Also, Leary develops a system within which we can talk about deductions of or from formulas that are not sentences. Most logic texts in philosophy limit themselves to discussing deduction as a relation between sentences. (I'm not sure the added generality of including nonsentential formulas is worth the trouble, any more than I'm sure it's worth the added complication it causes in the semantics to define validity and logical implication for nonsentential formulas. But hey, who am I to argue?)

We can begin with Leary's formal definition of a deduction in terms of axioms and rules of interence, and then investigate which specific axioms and rules of inference we will need. Here, then, is Leary's Definition 2.2.1:

Definition: If $\Sigma$ is a set of -formulas and $D$ is a finite sequence $\langle \phi_1, \phi_2, \ldots, \phi_n \rangle$ of -formulas, then $D$ is a deduction from $\Sigma$ if and only if for each $i$, $1 \leq i \leq n$, either

1. $\phi_i \in \Lambda$ ($\phi_i$ is a logical axiom), or
2. $\phi_i \in \Sigma$ ($\phi_i$ is a nonlogical axiom), or
3. There is a rule of inference $\langle \Gamma, \phi_i \rangle$ such that $\Gamma \subseteq \{\phi_1, \phi_2, \ldots, \phi_{i-1} \}$.

So $\Sigma$ will be a set of premises (which may or may not be usefully called "nonlogical axioms"; see earlier comment) and $\Lambda$ will be a set of logical axioms. Notice that rules of inference are characterized as ordered pairs $\langle \Gamma, \phi \rangle$, where $\Gamma$ is a set of formulas and $\phi$ is a formula. So for instance, in Barwise and Etchemendy's version of propositional logic, $\langle \{\phi, \phi \to \psi \}, \psi \rangle$ would be the rule of inference Conditional Elimination, and $\langle \{\phi\}, \phi \vee \psi \rangle$ would be the rule Disjunction Introduction.

Some of B&E's rules are difficult to fit into this format. Leary's deductive system does not include the idea of subproofs, so rules like Conditional Introduction and Disjunction Elimination are tricky to state. For Disjunction Elimination the following legitimates the same inferences as B&E's rule: $\langle \{\phi \vee \psi, \phi \to \theta, \psi \to \theta \}, \theta \rangle$. I don't think that there is a way to squeeze B&E's rule of Conditional Introduction into this format. (One way to express their rule is to say that if $\Sigma \cup \Lambda \cup \{\phi\} \vdash \psi$, we may write down $\phi \to \psi$. But this does not fit the $\langle \Gamma, \phi \rangle$ format.) However, we could replace their rule by another that accomplishes the same thing and can be expressed in the desired format; for instance, the rule $\langle \{\neg \phi \vee \psi \}, \phi \to \psi \rangle$. Alternatively, we could do the same sort of thing Leary does when specifying propositional rules: we could say that if $\Sigma \cup \Gamma \cup \phi \vdash \psi$, then $\langle \Gamma, \phi \to \psi \rangle$ is a rule of inference.