Propositional Logic

Propositional logic, also known as sentential logic and statement logic, is the branch of logic that studies ways of joining and/or modifying entire propositions, statements or sentences to form more complicated propositions, statements or sentences, as well as the logical relationships and properties that are derived from these methods of combining or altering statements. In propositional logic, the simplest statements are considered as indivisible units, and hence, propositional logic does not study those logical properties and relations that depend upon parts of statements that are not themselves statements on their own, such as the subject and predicate of a statement. The most thoroughly researched branch of propositional logic is classical truth-functional propositional logic, which studies logical operators and connectives that are used to produce complex statements whose truth-value depends entirely on the truth-values of the simpler statements making them up, and in which it is assumed that every statement is either true or false and not both. However, there are other forms of propositional logic in which other truth-values are considered, or in which there is consideration of connectives that are used to produce statements whose truth-values depend not simply on the truth-values of the parts, but additional things such as their necessity, possibility or relatedness to one another.

Table of Contents

1. Introduction
2. History
3. The Language of Propositional Logic
   1. Syntax and Formation Rules of PL
   2. Truth Functions and Truth Tables
   3. Definability of the Operators and the Languages PL’ and PL”
4. Tautologies, Logical Equivalence and Validity
5. Deduction: Rules of Inference and Replacement
   1. Natural Deduction
   2. Rules of Inference
   3. Rules of Replacement
   4. Direct Deductions
   5. Conditional and Indirect Proofs
6. Axiomatic Systems and the Propositional Calculus
7. Meta-Theoretic Results for the Propositional Calculus
8. Other Forms of Propositional Logic
9. References and Further Reading

1. Introduction

A statement can be defined as a declarative sentence, or part of a sentence, that is capable of having a truth-value, such as being true or false. So, for example, the following are statements:

• George W. Bush is the 43rd President of the United States.
• Paris is the capital of France.
• Everyone born on Monday has purple hair.

Sometimes, a statement can contain one or more other statements as parts. Consider for example, the following statement:

• Either Ganymede is a moon of Jupiter or Ganymede is a moon of Saturn.

While the above compound sentence is itself a statement, because it is true, the two parts, “Ganymede is a moon of Jupiter” and “Ganymede is a moon of Saturn”, are themselves statements, because the first is true and the second is false.

The term proposition is sometimes used synonymously with statement. However, it is sometimes used to name something abstract that two different statements with the same meaning are both said to “express”. In this usage, the English sentence, “It is raining”, and the French sentence “Il pleut”, would be considered to express the same proposition; similarly, the two English sentences, “Callisto orbits Jupiter” and “Jupiter is orbited by Callisto” would also be considered to express the same proposition. However, the nature or existence of propositions as abstract meanings is still a matter of philosophical controversy, and for the purposes of this article, the phrases “statement” and “proposition” are used interchangeably.

Propositional logic, also known as sentential logic, is that branch of logic that studies ways of combining or altering statements or propositions to form more complicated statements or propositions. Joining two simpler propositions with the word “and” is one common way of combining statements. When two statements are joined together with “and”, the complex statement formed by them is true if and only if both the component statements are true. Because of this, an argument of the following form is logically valid:

Paris is the capital of France and Paris has a population of over two million.
Therefore, Paris has a population of over two million.

Propositional logic largely involves studying logical connectives such as the words “and” and “or” and the rules determining the truth-values of the propositions they are used to join, as well as what these rules mean for the validity of arguments, and such logical relationships between statements as being consistent or inconsistent with one another, as well as logical properties of propositions, such as being tautologically true, being contingent, and being self-contradictory. (These notions are defined below.)

Propositional logic also studies way of modifying statements, such as the addition of the word “not” that is used to change an affirmative statement into a negative statement. Here, the fundamental logical principle involved is that if a given affirmative statement is true, the negation of that statement is false, and if a given affirmative statement is false, the negation of that statement is true.

What is distinctive about propositional logic as opposed to other (typically more complicated) branches of logic is that propositional logic does not deal with logical relationships and properties that involve the parts of a statement smaller than the simple statements making it up. Therefore, propositional logic does not study those logical characteristics of the propositions below in virtue of which they constitute a valid argument:

1. George W. Bush is a president of the United States.
2. George W. Bush is a son of a president of the United States.
3. Therefore, there is someone who is both a president of the United States and a son of a president of the United States.

The recognition that the above argument is valid requires one to recognize that the subject in the first premise is the same as the subject in the second premise. However, in propositional logic, simple statements are considered as indivisible wholes, and those logical relationships and properties that involve parts of statements such as their subjects and predicates are not taken into consideration.

Propositional logic can be thought of as primarily the study of logical operators. A logical operator is any word or phrase used either to modify one statement to make a different statement, or join multiple statements together to form a more complicated statement. In English, words such as “and”, “or”, “not”, “if … then…”, “because”, and “necessarily”, are all operators.

A logical operator is said to be truth-functional if the truth-values (the truth or falsity, etc.) of the statements it is used to construct always depend entirely on the truth or falsity of the statements from which they are constructed. The English words “and”, “or” and “not” are (at least arguably) truth-functional, because a compound statement joined together with the word “and” is true if both the statements so joined are true, and false if either or both are false, a compound statement joined together with the word “or” is true if at least one of the joined statements is true, and false if both joined statements are false, and the negation of a statement is true if and only if the statement negated is false.

Some logical operators are not truth-functional. One example of an operator in English that is not truth-functional is the word “necessarily”. Whether a statement formed using this operator is true or false does not depend entirely on the truth or falsity of the statement to which the operator is applied. For example, both of the following statements are true:

• 2 + 2 = 4.
• Someone is reading an article in a philosophy encyclopedia.

However, let us now consider the corresponding statements modified with the operator “necessarily”:

• Necessarily, 2 + 2 = 4.
• Necessarily, someone is reading an article in a philosophy encyclopedia.

Here, the first example is true but the second example is false. Hence, the truth or falsity of a statement using the operator “necessarily” does not depend entirely on the truth or falsity of the statement modified.

Truth-functional propositional logic is that branch of propositional logic that limits itself to the study of truth-functional operators. Classical (or “bivalent”) truth-functional propositional logic is that branch of truth-functional propositional logic that assumes that there are are only two possible truth-values a statement (whether simple or complex) can have: (1) truth, and (2) falsity, and that every statement is either true or false but not both.

Classical truth-functional propositional logic is by far the most widely studied branch of propositional logic, and for this reason, most of the remainder of this article focuses exclusively on this area of logic. In addition to classical truth-functional propositional logic, there are other branches of propositional logic that study logical operators, such as “necessarily”, that are not truth-functional. There are also “non-classical” propositional logics in which such possibilities as (i) a proposition’s having a truth-value other than truth or falsity, (ii) a proposition’s having an indeterminate truth-value or lacking a truth-value altogether, and sometimes even (iii) a proposition’s being both true and false, are considered. (For more information on these alternative forms of propositional logic, consult Section VIII below.)

2. History

The serious study of logic as an independent discipline began with the work of Aristotle (384-322 BCE). Generally, however, Aristotle’s sophisticated writings on logic dealt with the logic of categories and quantifiers such as “all”, and “some”, which are not treated in propositional logic. However, in his metaphysical writings, Aristotle espoused two principles of great importance in propositional logic, which have since come to be called the Law of Excluded Middle and the Law of Contradiction. Interpreted in propositional logic, the first is the principle that every statement is either true or false, the second is the principle that no statement is both true and false. These are, of course, cornerstones of classical propositional logic. There is some evidence that Aristotle, or at least his successor at the Lyceum, Theophrastus (d. 287 BCE), did recognize a need for the development of a doctrine of “complex” or “hypothetical” propositions, that is, those involving conjunctions (statements joined by “and”), disjunctions (statements joined by “or”) and conditionals (statements joined by “if… then…”), but their investigations into this branch of logic seem to have been very minor.

More serious attempts to study statement operators such as “and”, “or” and “if… then…” were conducted by the Stoic philosophers in the late 3rd century BCE. Since most of their original works—if indeed, these writings were even produced—are lost, we cannot make many definite claims about exactly who first made investigations into what areas of propositional logic, but we do know from the writings of Sextus Empiricus that Diodorus Cronus and his pupil Philo had engaged in a protracted debate about whether the truth of a conditional statement depends entirely on it not being the case that its antecedent (if-clause) is true while its consequent (then-clause) is false, or whether it requires some sort of stronger connection between the antecedent and consequent—a debate that continues to have relevance for modern discussion of conditionals. The Stoic philosopher Chrysippus (roughly 280-205 BCE) perhaps did the most in advancing Stoic propositional logic, by marking out a number of different ways of forming complex premises for arguments, and for each, listing valid inference schemata. Chrysippus suggested that the following inference schemata are to be considered the most basic:

1. If the first, then the second; but the first; therefore the second.
2. If the first, then the second; but not the second; therefore, not the first.
3. Not both the first and the second; but the first; therefore, not the second.
4. Either the first or the second [and not both]; but the first; therefore, not the second.
5. Either the first or the second; but not the second; therefore the first.

Inference rules such as the above correspond very closely to the basic principles in a contemporary system of natural deduction for propositional logic. For example, the first two rules correspond to the rules of modus ponens and modus tollens, respectively. These basic inference schemata were expanded upon by less basic inference schemata by Chrysippus himself and other Stoics, and are preserved in the work of Diogenes Laertius, Sextus Empiricus and later, in the work of Cicero.

Advances on the work of the Stoics were undertaken in small steps in the centuries that followed. This work was done by, for example, the second century logician Galen (roughly 129-210 CE), the sixth century philosopher Boethius (roughly 480-525 CE) and later by medieval thinkers such as Peter Abelard (1079-1142) and William of Ockham (1288-1347), and others. Much of their work involved producing better formalizations of the principles of Aristotle or Chrysippus, introducing improved terminology and furthering the discussion of the relationships between operators. Abelard, for example, seems to have been the first to clearly differentiate exclusive disjunction from inclusive disjunction (discussed below), and to suggest that inclusive disjunction is the more important notion for the development of a relatively simple logic of disjunctions.

The next major step forward in the development of propositional logic came only much later with the advent of symbolic logic in the work of logicians such as Augustus DeMorgan (1806-1871) and, especially, George Boole (1815-1864) in the mid-19th century. Boole was primarily interested in developing a mathematical-style “algebra” to replace Aristotelian syllogistic logic, primarily by employing the numeral “1” for the universal class, the numeral “0” for the empty class, the multiplication notation “xy” for the intersection of classes x and y, the addition notation “x + y” for the union of classes x and y, etc., so that statements of syllogistic logic could be treated in quasi-mathematical fashion as equations; for example, “No x is y” could be written as “xy = 0”. However, Boole noticed that if an equation such as “x = 1” is read as “x is true”, and “x = 0” is read as “x is false”, the rules given for his logic of classes can be transformed into a logic for propositions, with “x + y = 1” reinterpreted as saying that either x or y is true, and “xy = 1” reinterpreted as meaning that x and y are both true. Boole’s work sparked rapid interest in logic among mathematicians. Later, “Boolean algebras” were used to form the basis of the truth-functional propositional logics utilized in computer design and programming.

In the late 19th century, Gottlob Frege (1848-1925) presented logic as a branch of systematic inquiry more fundamental than mathematics or algebra, and presented the first modern axiomatic calculus for logic in his 1879 work Begriffsschrift. While it covered more than propositional logic, from Frege’s axiomatization it is possible to distill the first complete axiomatization of classical truth-functional propositional logic. Frege was also the first to systematically argue that all truth-functional connectives could be defined in terms of negation and the material conditional.

In the early 20th century, Bertrand Russell gave a different complete axiomatization of propositional logic, considered on its own, in his 1906 paper “The Theory of Implication”, and later, along with A. N. Whitehead, produced another axiomatization using disjunction and negation as primitives in the 1910 work Principia Mathematica. Proof of the possibility of defining all truth functional operators in virtue of a single binary operator was first published by American logician H. M. Sheffer in 1913, though American logician C. S. Peirce (1839-1914) seems to have discovered this decades earlier. In 1917, French logician Jean Nicod discovered that it was possible to axiomatize propositional logic using the Sheffer stroke and only a single axiom schema and single inference rule.

The notion of a “truth table” is often utilized in the discussion of truth-functional connectives (discussed below). It seems to have been at least implicit in the work of Peirce, W. S. Jevons (1835-1882), Lewis Carroll (1832-1898), John Venn (1834-1923), and Allan Marquand (1853-1924). Truth tables appear explicitly in writings by Eugen Müller as early as 1909. Their use gained rapid popularity in the early 1920s, perhaps due to the combined influence of the work of Emil Post, whose 1921 work makes liberal use of them, and Ludwig Wittgenstein’s 1921 Tractatus Logico-Philosophicus, in which truth tables and truth-functionality are prominently featured.

Systematic inquiry into axiomatic systems for propositional logic and related metatheory was conducted in the 1920s, 1930s and 1940s by David Hilbert, Paul Bernays, Alfred Tarski, Jan Łukasiewicz, Kurt Gödel, Alonzo Church, and others. It is during this period, that most of the important metatheoretic results such as those discussed in Section VII were discovered.

Complete natural deduction systems for classical truth-functional propositional logic were developed and popularized in the work of Gerhard Gentzen in the mid-1930s, and subsequently introduced into influential textbooks such as that of F. B. Fitch (1952) and Irving Copi (1953).

Modal propositional logics are the most widely studied form of non-truth-functional propositional logic. While interest in modal logic dates back to Aristotle, by contemporary standards the first systematic inquiry into this modal propositional logic can be found in the work of C. I. Lewis in 1912 and 1913. Among other well-known forms of non-truth-functional propositional logic, deontic logic began with the work of Ernst Mally in 1926, and epistemic logic was first treated systematically by Jaakko Hintikka in the early 1960s. The modern study of three-valued propositional logic began in the work of Jan Łukasiewicz in 1917, and other forms of non-classical propositional logic soon followed suit. Relevance propositional logic is relatively more recent; dating from the mid-1970s in the work of A. R. Anderson and N. D. Belnap. Paraconsistent logic, while having its roots in the work of Łukasiewicz and others, has blossomed into an independent area of research only recently, mainly due to work undertaken by N. C. A. da Costa, Graham Priest and others in the 1970s and 1980s.

3. The Language of Propositional Logic

The basic rules and principles of classical truth-functional propositional logic are, among contemporary logicians, almost entirely agreed upon, and capable of being stated in a definitive way. This is most easily done if we utilize a simplified logical language that deals only with simple statements considered as indivisible units as well as complex statements joined together by means of truth-functional connectives. We first consider a language called PL for “Propositional Logic”. Later we shall consider two even simpler languages, PL’ and PL”.

a. Syntax and Formation Rules of PL

In any ordinary language, a statement would never consist of a single word, but would always at the very least consist of a noun or pronoun along with a verb. However, because propositional logic does not consider smaller parts of statements, and treats simple statements as indivisible wholes, the language PL uses uppercase letters ‘‘, ‘‘, ‘‘, etc., in place of complete statements. The logical signs ‘‘, ‘‘, ‘→’, ‘↔’, and ‘‘ are used in place of the truth-functional operators, “and”, “or”, “if… then…”, “if and only if”, and “not”, respectively. So, consider again the following example argument, mentioned in Section I.

Paris is the capital of France and Paris has a population of over two million.
Therefore, Paris has a population of over two million.

If we use the letter ‘‘ as our translation of the statement “Paris is the captial of France” in PL, and the letter ‘‘ as our translation of the statement “Paris has a population of over two million”, and use a horizontal line to separate the premise(s) of an argument from the conclusion, the above argument could be symbolized in language PL as follows:

In addition to statement letters like ‘‘ and ‘‘ and the operators, the only other signs that sometimes appear in the language PL are parentheses which are used in forming even more complex statements. Consider the English compound sentence, “Paris is the most important city in France if and only if Paris is the capital of France and Paris has a population of over two million.” If we use the letter ‘‘ in language PL to mean that Paris is the most important city in France, this sentence would be translated into PL as follows:

The parentheses are used to group together the statements ‘‘ and ‘‘ and differentiate the above statement from the one that would be written as follows:

This latter statement asserts that Paris is the most important city in France if and only if it is the capital of France, and (separate from this), Paris has a population of over two million. The difference between the two is subtle, but important logically.

It is important to describe the syntax and make-up of statements in the language PL in a precise manner, and give some definitions that will be used later on. Before doing this, it is worthwhile to make a distinction between the language in which we will be discussing PL, namely, English, from PL itself. Whenever one language is used to discuss another, the language in which the discussion takes place is called the metalanguage, and language under discussion is called the object language. In this context, the object language is the language PL, and the metalanguage is English, or to be more precise, English supplemented with certain special devices that are used to talk about language PL. It is possible in English to talk about words and sentences in other languages, and when we do, we place the words or sentences we wish to talk about in quotation marks. Therefore, using ordinary English, I can say that “parler” is a French verb, and “” is a statement of PL. The following expression is part of PL, not English:

However, the following expression is a part of English; in particular, it is the English name of a PL sentence:

“”

This point may seem rather trivial, but it is easy to become confused if one is not careful.

In our metalanguage, we shall also be using certain variables that are used to stand for arbitrary expressions built from the basic symbols of PL. In what follows, the Greek letters ‘‘, ‘‘, and so on, are used for any object language (PL) expression of a certain designated form. For example, later on, we shall say that, if is a statement of PL, then so is . Notice that ‘‘ itself is not a symbol that appears in PL; it is a symbol used in English to speak about symbols of PL. We will also be making use of so-called “Quine corners”, written ‘‘ and ‘‘, which are a special metalinguistic device used to speak about object language expressions constructed in a certain way. Suppose is the statement “” and is the statement ““; then is the complex statement ““.

Let us now proceed to giving certain definitions used in the metalanguage when speaking of the language PL.

Definition: A statement letter of PL is defined as any uppercase letter written with or without a numerical subscript.

Note: According to this definition, ‘‘, ‘‘, ‘‘, ‘‘, and ‘‘ are examples of statement letters. The numerical subscripts are used just in case we need to deal with more than 26 simple statements: in that case, we can use ‘‘ to mean something different than ‘‘, and so forth.

Definition: A connective or operator of PL is any of the signs ‘‘, ‘‘, ‘‘, ‘→’, and ‘↔’.

Definition: A well-formed formula (hereafter abbreviated as wff) of PL is defined recursively as follows:

1. Any statement letter is a well-formed formula.
2. If is a well-formed formula, then so is .
3. If and are well-formed formulas, then so is .
4. If and are well-formed formulas, then so is .
5. If and are well-formed formulas, then so is .
6. If and are well-formed formulas, then so is .
7. Nothing that cannot be constructed by successive steps of (1)-(6) is a well-formed formula.

Note: According to part (1) of this definition, the statement letters ‘‘, ‘‘ and ‘‘ are wffs. Because ‘‘ and ‘‘ are wffs, by part (3), “” is a wff. Because it is a wff, and ‘‘ is also a wff, by part (6), “” is a wff. It is conventional to regard the outermost parentheses on a wff as optional, so that “” is treated as an abbreviated form of ““. However, whenever a shorter wff is used in constructing a more complicated wff, the parentheses on the shorter wff are necessary.

The notion of a well-formed formula should be understood as corresponding to the notion of a grammatically correct or properly constructed statement of language PL. This definition tells us, for example, that “” is grammatical for PL because it is a well-formed formula, whereas the string of symbols, ““, while consisting entirely of symbols used in PL, is not grammatical because it is not well-formed.

b. Truth Functions and Truth Tables

So far we have in effect described the grammar of language PL. When setting up a language fully, however, it is necessary not only to establish rules of grammar, but also describe the meanings of the symbols used in the language. We have already suggested that uppercase letters are used as complete simple statements. Because truth-functional propositional logic does not analyze the parts of simple statements, and only considers those ways of combining them to form more complicated statements that make the truth or falsity of the whole dependent entirely on the truth or falsity of the parts, in effect, it does not matter what meaning we assign to the individual statement letters like ‘‘, ‘‘ and ‘‘, etc., provided that each is taken as either true or false (and not both).

However, more must be said about the meaning or semantics, of the logical operators ‘‘, ‘‘, ‘→’, ‘↔’, and ‘‘. As mentioned above, these are used in place of the English words, ‘and’, ‘or’, ‘if… then…’, ‘if and only if’, and ‘not’, respectively. However, the correspondence is really only rough, because the operators of PL are considered to be entirely truth-functional, whereas their English counterparts are not always used truth-functionally. Consider, for example, the following statements:

1. If Bob Dole is president of the United States in 2004, then the president of the United States in 2004 is a member of the Republican party.
2. If Al Gore is president of the United States in 2004, then the president of the United States in 2004 is a member of the Republican party.

For those familiar with American politics, it is tempting to regard the English sentence (1) as true, but to regard (2) as false, since Dole is a Republican but Gore is not. But notice that in both cases, the simple statement in the “if” part of the “if… then…” statement is false, and the simple statement in the “then” part of the statement is true. This shows that the English operator “if… then…” is not fully truth-functional. However, all the operators of language PL are entirely truth-functional, so the sign ‘→’, though similar in many ways to the English “if… then…” is not in all ways the same. More is said about this operator below.

Since our study is limited to the ways in which the truth-values of complex statements depend on the truth-values of the parts, for each operator, the only aspect of its meaning relevant in this context is its associated truth-function. The truth-function for an operator can be represented as a table, each line of which expresses a possible combination of truth-values for the simpler statements to which the operator applies, along with the resulting truth-value for the complex statement formed using the operator.

The signs ‘‘, ‘‘, ‘→’, ‘↔’, and ‘‘, correspond, respectively, to the truth-functions of conjunction, disjunction, material implication, material equivalence, and negation. We shall consider these individually.

Conjunction: The conjunction of two statements and , written in PL as , is true if both and are true, and is false if either is false or is false or both are false. In effect, the meaning of the operator ‘‘ can be displayed according to the following chart, which shows the truth-value of the conjunction depending on the four possibilities of the truth-values of the parts:

T T F F	T F T F	T F F F

Conjunction using the operator ‘‘ is language PL’s rough equivalent of joining statements together with ‘and’ in English. In a statement of the form , the two statements joined together, and , are called the conjuncts, and the whole statement is called a conjunction.

Instead of the sign ‘‘, some other logical works use the signs ‘‘ or ‘‘ for conjunction.

Disjunction: The disjunction of two statements and , written in PL as , is true if either is true or is true, or both and are true, and is false only if both and are false. A chart similar to that given above for conjunction, modified for to show the meaning of the disjunction sign ‘‘ instead, would be drawn as follows:

T T F F	T F T F	T T T F

This is language PL’s rough equivalent of joining statements together with the word ‘or’ in English. However, it should be noted that the sign ‘‘ is used for disjunction in the inclusive sense. Sometimes when the word ‘or’ is used to join together two English statements, we only regard the whole as true if one side or the other is true, but not both, as when the statement “Either we can buy the toy robot, or we can buy the toy truck; you must choose!” is spoken by a parent to a child who wants both toys. This is called the exclusive sense of ‘or’. However, in PL, the sign ‘‘ is used inclusively, and is more analogous to the English word ‘or’ as it appears in a statement such as (for example, said about someone who has just received a perfect score on the SAT), “either she studied hard, or she is extremely bright”, which does not mean to rule out the possibility that she both studied hard and is bright. In a statement of the form , the two statements joined together, and , are called the disjuncts, and the whole statement is called a disjunction.

Material Implication: This truth-function is represented in language PL with the sign ‘→’. A statement of the form , is false if is true and is false, and is true if either is false or is true (or both). This truth-function generates the following chart:

T T F F	T F T F	T F T T

Because the truth of a statement of the form rules out the possibility of being true and being false, there is some similarity between the operator ‘→’ and the English phrase, “if… then…”, which is also used to rule out the possibility of one statement being true and another false; however, ‘→’ is used entirely truth-functionally, and so, for reasons discussed earlier, it is not entirely analogous with “if… then…” in English. If is false, then is regarded as true, whether or not there is any connection between the falsity of and the truth-value of . In a statement of the form , we call the antecedent, and we call the consequent, and the whole statement is sometimes also called a (material) conditional.

The sign ‘‘ is sometimes used instead of ‘→’ for material implication.

Material Equivalence: This truth-function is represented in language PL with the sign ‘↔’. A statement of the form is regarded as true if and are either both true or both false, and is regarded as false if they have different truth-values. Hence, we have the following chart:

T T F F	T F T F	T F F T

Since the truth of a statement of the form requires and to have the same truth-value, this operator is often likened to the English phrase “…if and only if…”. Again, however, they are not in all ways alike, because ‘↔’ is used entirely truth-functionally. Regardless of what and are, and what relation (if any) they have to one another, if both are false, is considered to be true. However, we would not normally regard the statement “Al Gore is the President of the United States in 2004 if and only if Bob Dole is the President of the United States in 2004” as true simply because both simpler statements happen to be false. A statement of the form is also sometimes referred to as a (material) biconditional.

The sign ‘‘ is sometimes used instead of ‘↔’ for material equivalence.

Negation: The negation of statement , simply written in language PL, is regarded as true if is false, and false if is true. Unlike the other operators we have considered, negation is applied to a single statement. The corresponding chart can therefore be drawn more simply as follows:

T F	F T

The negation sign ‘‘ bears obvious similarities to the word ‘not’ used in English, as well as similar phrases used to change a statement from affirmative to negative or vice-versa. In logical languages, the signs ‘‘ or ‘-‘ are sometimes used in place of ‘‘.

The five charts together provide the rules needed to determine the truth-value of a given wff in language PL when given the truth-values of the independent statement letters making it up. These rules are very easy to apply in the case of a very simple wff such as ““. Suppose that ‘‘ is true, and ‘‘ is false; according to the second row of the chart given for the operator, ‘‘, we can see that this statement is false.

However, the charts also provide the rules necessary for determining the truth-value of more complicated statements. We have just seen that “” is false if ‘‘ is true and ‘‘ is false. Consider a more complicated statement that contains this statement as a part, for example, ““, and suppose once again that ‘‘ is true, and ‘‘ is false, and further suppose that ‘‘ is also false. To determine the truth-value of this complicated statement, we begin by determining the truth-value of the internal parts. The statement ““, as we have seen, is false. The other substatement, ““, is true, because ‘‘ is false, and ‘‘ reverses the truth-value of that to which it is applied. Now we can determine the truth-value of the whole wff, ““, by consulting the chart given above for ‘→’. Here, the wff “” is our , and “” is our , and since their truth-values are F and T, respectively, we consult the third row of the chart, and we see that the complex statement “” is true.

We have so far been considering the case in which ‘‘ is true and ‘‘ and ‘‘ are both false. There are, however, a number of other possibilities with regard to the possible truth-values of the statement letters, ‘‘, ‘‘ and ‘‘. There are eight possibilities altogether, as shown by the following list:

T T T T F F F F	T T F F T T F F	T F T F T F T F

Strictly speaking, each of the eight possibilities above represents a different truth-value assignment, which can be defined as a possible assignment of truth-values T or F to the different statement letters making up a wff or series of wffs. If a wff has n distinct statement letters making up, the number of possible truth-value assignments is 2ⁿ. With the wff, ““, there are three statement letters, ‘‘, ‘‘ and ‘‘, and so there are 8 truth-value assignments.

It then becomes possible to draw a chart showing how the truth-value of a given wff would be resolved for each possible truth-value assignment. We begin with a chart showing all the possible truth-value assignments for the wff, such as the one given above. Next, we write out the wff itself on the top right of our chart, with spaces between the signs. Then, for each, truth-value assignment, we repeat the appropriate truth-value, ‘T’, or ‘F’, underneath the statement letters as they appear in the wff. Then, as the truth-values of those wffs that are parts of the complete wff are determined, we write their truth-values underneath the logical sign that is used to form them. The final column filled in shows the truth-value of the entire statement for each truth-value assignment. Given the importance of this column, we highlight it in some way. Here, we highlight it in yellow.

			|				→
T T T T F F F F	T T F F T T F F	T F T F T F T F		T T T T F F F F	T T F F F F F F	T T F F T T F F	F T T T T T T T	F T F T F T F T	T F T F T F T F

Charts such as the one given above are called truth tables. In classical truth-functional propositional logic, a truth table constructed for a given wff in effects reveals everything logically important about that wff. The above chart tells us that the wff “” can only be false if ‘‘, ‘‘ and ‘‘ are all true, and is true otherwise.

c. Definability of the Operators and the Languages PL’ and PL”

The language PL, as we have seen, contains operators that are roughly analogous to the English operators ‘and’, ‘or’, ‘if… then…’, ‘if and only if’, and ‘not’. Each of these, as we have also seen, can be thought of as representing a certain truth-function. It might be objected however, that there are other methods of combining statements together in which the truth-value of the statement depends wholly on the truth-values of the parts, or in other words, that there are truth-functions besides conjunction, (inclusive) disjunction, material implication, material equivalence and negation. For example, we noted earlier that the sign ‘‘ is used analogously to ‘or’ in the inclusive sense, which means that language PL has no simple sign for ‘or’ in the exclusive sense. It might be thought, however, that the langauge PL is incomplete without the addition of an additional symbol, say ‘‘, such that would be regarded as true if is true and is false, or is false and is true, but would be regarded as false if either both and are true or both and are false.

However, a possible response to this objection would be to make note that while language PL does not include a simple sign for this exclusive sense of disjunction, it is possible, using the symbols that are included in PL, to construct a statement that is true in exactly the same circumstances. Consider, for example, a statement of the form . It is easily shown, using a truth table, that any wff of this form would have the same truth-value as a would-be statement using the operator ‘‘. See the following chart:

		|			↔
T T F F	T F T F		F T T F	T T F F	T F F T	T F T F

Here we see that a wff of the form is true if either or is true but not both. This shows that PL is not lacking in any way by not containing a sign ‘‘. All the work that one would wish to do with this sign can be done using the signs ‘↔’ and ‘‘. Indeed, one might claim that the sign ‘‘ can be defined in terms of the signs ‘↔’, and ‘‘, and then use the form as an abbreviation of a wff of the form , without actually expanding the primitive vocabulary of language PL.

The signs ‘‘, ‘‘, ‘→’, ‘↔’ and ‘‘, were chosen as the operators to include in PL because they correspond (roughly) the sorts of truth-functional operators that are most often used in ordinary discourse and reasoning. However, given the preceding discussion, it is natural to ask whether or not some operators on this list can be defined in terms of the others. It turns out that they can. In fact, if for some reason we wished our logical language to have a more limited vocabulary, it is possible to get by using only the signs ‘‘ and ‘→’, and define all other possible truth-functions in virtue of them. Consider, for example, the following truth table for statements of the form :

		|			→
T T F F	T F T F		T F F F	T T F F	F T T T	F T F T	T F T F

We can see from the above that a wff of the form always has the same truth-value as the corresponding statement of the form . This shows that the sign ‘‘ can in effect be defined using the signs ‘‘ and ‘→’.

Next, consider the truth table for statements of the form :

		|			→
T T F F	T F T F		F F T T	T T F F	T T T F	T F T F

Here we can see that a statement of the form always has the same truth-value as the corresponding statement of the form . Again, this shows that the sign ‘‘ could in effect be defined using the signs ‘→’ and ‘‘.

Lastly, consider the truth table for a statement of the form :

		|			→		→			→
T T F F	T F T F		T F F T	T T F F	T F T T	T F T F	F T T F	F F T F	T F T F	T T F T	T T F F

From the above, we see that a statement of the form always has the same truth-value as the corresponding statement of the form . In effect, therefore, we have shown that the remaining operators of PL can all be defined in virtue of ‘→’, and ‘‘, and that, if we wished, we could do away with the operators, ‘‘, ‘‘ and ‘↔’, and simply make do with those equivalent expressions built up entirely from ‘→’ and ‘‘.

Let us call the language that results from this simplication PL’. While the definition of a statement letter remains the same for PL’ as for PL, the definition of a well-formed formula (wff) for PL’ can be greatly simplified. In effect, it can be stated as follows:

Definition: A well-formed formula (or wff) of PL’ is defined recursively as follows:

1. Any statement letter is a well-formed formula.
2. If is a well-formed formula, then so is .
3. If and are well-formed formulas, then so is .
4. Nothing that cannot be constructed by successive steps of (1)-(3) is a well-formed formula.

Strictly speaking, then, the langauge PL’ does not contain any statements using the operators ‘‘, ‘‘, or ‘↔’. One could however, utilize conventions such that, in language PL’, an expression of the form is to be regarded as a mere abbreviation or short-hand for the corresponding statement of the form , and similarly that expressions of the forms and are to be regarded as abbreviations of expressions of the forms or , respectively. In effect, this means that it is possible to translate any wff of language PL into an equivalent wff of language PL’.

In Section VII, it is proven that not only are the operators ‘‘ and ‘→’ sufficient for defining every truth-functional operator included in language PL, but also that they are sufficient for defining any imaginable truth-functional operator in classical propositional logic.

Nevertheless, the choice of ‘‘ and ‘→’ for the primitive signs used in language PL’ is to some extent arbitrary. It would also have been possible to define all other operators of PL (including ‘→’) using the signs ‘‘ and ‘‘. On this approach, would be defined as , would be defined as , and would be defined as . Similarly, we could instead have begun with ‘‘ and ‘‘ as our starting operators. On this way of proceeding, would be defined as , would be defined as , and would be defined as .

There are, as we have seen, multiple different ways of reducing all truth-functional operators down to two primitives. There are also two ways of reducing all truth-functional operators down to a single primitive operator, but they require using an operator that is not included in language PL as primitive. On one approach, we utilize an operator written ‘|’, and explain the truth-function corresponding to this sign by means of the following chart:

T T F F	T F T F	F T T T

Here we can see that a statement of the form is false if both and are true, and true otherwise. For this reason one might read ‘|’ as akin to the English expression, “Not both … and …”. Indeed, it is possible to represent this truth-function in language PL using an expression of the form, . However, since it is our intention to show that all other truth-functional operators, including ‘‘ and ‘‘ can be derived from ‘|’, it is better not to regard the meanings of ‘‘ and ‘‘ as playing a part of the meaning of ‘|’, and instead attempt (however counterintuitive it may seem) to regard ‘|’ as conceptually prior to ‘‘ and ‘‘.

The sign ‘|’ is called the Sheffer stroke, and is named after H. M. Sheffer, who first publicized the result that all truth-functional connectives could be defined in virtue of a single operator in 1913.

We can then see that the connective ‘‘ can be defined in virtue of ‘|’, because an expression of the form generates the following truth table, and hence is equivalent to the corresponding expression of the form :

		|		|		|		|
T T F F	T F T F		T T F F	F T T T	T F T F	T F F F	T T F F	F T T T	T F T F

Similarly, we can define the operator ‘‘ using ‘|’ by noting that an expression of the form always has the same truth-value as the corresponding statement of the form :

		|		|		|		|
T T F F	T F T F		T T F F	F F T T	T T F F	T T T F	T F T F	F T F T	T F T F

The following truth table shows that a statement of the form always has the same truth table as a statement of the form :

		|		|		|
T T F F	T F T F		T T F F	T F T T	T F T F	F T F T	T F T F

Although far from intuitively obvious, the following table shows that an expression of the form always has the same truth-value as the corresponding wff of the form :

|

|

|

|

|

|

T T F F

T F T F

T T F F

F F T T

T T F F

T T T F

T F T F

F T F T

T F T F

T F F T

T T F F

F T T T

T F T F

This leaves only the sign ‘‘, which is perhaps the easiest to define using ‘|’, as clearly , or, roughly, “not both and “, has the opposite truth-value from itself:

	|		|
T F		T F	F T	T F

If, therefore, we desire a language for use in studying propositional logic that has as small a vocabulary as possible, we might suggest using a language that employs the sign ‘|’ as its sole primitive operator, and defines all other truth-functional operators in virtue of it. Let us call such a language PL”. PL” differs from PL and PL’ only in that its definition of a well-formed formula can be simplified even further:

Definition: A well-formed formula (or wff) of PL” is defined recursively as follows:

1. Any statement letter is a well-formed formula.
2. If and are well-formed formulas, then so is .
3. Nothing that cannot be constructed by successive steps of (1)-(2) is a well-formed formula.

In language PL”, strictly speaking, ‘|’ is the only operator. However, for reasons that should be clear from the above, any expression from language PL that involves any of the operators ‘‘, ‘‘, ‘‘, ‘→’, or ‘↔’ could be translated into language PL” without the loss of any of its important logical properties. In effect, statements using these signs could be regarded as abbreviations or shorthand expressions for wffs of PL” that only use the operator ‘|’.

Even here, the choice of ‘|’ as the sole primitive is to some extent arbitrary. It would also be possible to reduce all truth-functional operators down to a single primitive by making use of a sign ‘‘, treating it as roughly equivalent to the English expression, “neither … nor …”, so that the corresponding chart would be drawn as follows:

T T F F	T F T F	F F F T

If we were to use ‘‘ as our sole operator, we could again define all the others. would be defined as ; would be defined as ; would be defined as ; and similarly for the other operators. The sign ‘‘ is sometimes also referred to as the Sheffer stroke, and is also called the Peirce/Sheffer dagger.

Depending on one’s purposes in studying propositional logic, sometimes it makes sense to use a rich language like PL with more primitive operators, and sometimes it makes sense to use a relatively sparse language such as PL’ or PL” with fewer primitive operators. The advantage of the former approach is that it conforms better with our ordinary reasoning and thinking habits; the advantage of the latter is that it simplifies the logical language, which makes certain interesting results regarding the deductive systems making use of the language easier to prove.

For the remainder of this article, we shall primarily be concerned with the logical properties of statements formed in the richer language PL. However, we shall consider a system making use of language PL’ in some detail in Section VI, and shall also make brief mention of a system making use of language PL”.

4. Tautologies, Logical Equivalence and Validity

Truth-functional propositional logic concerns itself only with those ways of combining statements to form more complicated statements in which the truth-values of the complicated statements depend entirely on the truth-values of the parts. Owing to this, all those features of a complex statement that are studied in propositional logic derive from the way in which their truth-values are derived from those of their parts. These features are therefore always represented in the truth table for a given statement.

Some complex statements have the interesting feature that they would be true regardless of the truth-values of the simple statements making them up. A simple example would be the wff ““; that is, “ or not “. It is fairly easy to see that this statement is true regardless of whether ‘‘ is true or ‘‘ is false. This is also shown by its truth table:

	|
T F		T F	T T	F T	T F

There are, however, statements for which this is true but it is not so obvious. Consider the wff, ““. This wff also comes out as true regardless of the truth-values of ‘‘, ‘‘ and ‘‘.

|

→

→

→

T T T T F F F F

T T F F T T F F

T F T F T F T F

T F T F T F T F

T T T T T T T T

T T T T F F F F

T T F F T T T T

T T F F T T F F

T T T F T T T T

F F T F F F T F

T F T F T F T F

T T F T T T F T

T T F F T T F F

Statements that have this interesting feature are called tautologies. Let us define this notion precisely.

Definition: a wff is a tautology if and only if it is true for all possible truth-value assignments to the statement letters making it up.

Tautologies are also sometimes called logical truths or truths of logic because tautologies can be recognized as true solely in virtue of the principles of propositional logic, and without recourse to any additional information.

On the other side of the spectrum from tautologies are statements that come out as false regardless of the truth-values of the simple statements making them up. A simple example of such a statement would be the wff ““; clearly such a statement cannot be true, as it contradicts itself. This is revealed by its truth table:

	|
T F		T F	F F	F T	T F

To state this precisely:

Definition: a wff is a self-contradiction if and only if it is false for all possible truth-value assignments to the statement letters making it up.

Another, more interesting, example of a self-contradiction is the statement ““; this is not as obviously self-contradictory. However, we can see that it is when we consider its truth table:

		|			→					→
T T F F	T F T F		F T F F	T T F F	T F T T	T F T F	F F F F	F F T F	T F T F	T T F T	T T F F

A statement that is neither self-contradictory nor tautological is called a contingent statement. A contingent statement is true for some truth-value assignments to its statement letters and false for others. The truth table for a contingent statement reveals which truth-value assignments make it come out as true, and which make it come out as false. Consider the truth table for the statement ““:

		|		→				→
T T F F	T F T F		T T F F	T F T T	T F T F	F F T T	T T F F	F T T T	F T F T	T F T F

We can see that of the four possible truth-value assignments for this statement, two make it come as true, and two make it come out as false. Specifically, the statement is true when ‘‘ is false and ‘‘ is true, and when ‘‘ is false and ‘‘ is false, and the statement is false when ‘‘ is true and ‘‘ is true and when ‘‘ is true and ‘‘ is false.

Truth tables are also useful in studying logical relationships that hold between two or more statements. For example, two statements are said to be consistent when it is possible for both to be true, and are said to be inconsistent when it is not possible for both to be true. In propositional logic, we can make this more precise as follows.

Definition: two wffs are consistent if and only if there is at least one possible truth-value assignment to the statement letters making them up that makes both wffs true.

Definition: two wffs are inconsistent if and only if there is no truth-value assignment to the statement letters making them up that makes them both true.

Whether or not two statements are consistent can be determined by means of a combined truth table for the two statements. For example, the two statements, “” and “” are consistent:

		|							↔
T T F F	T F T F		T T F F	T T T F	T F T F		T F F T	T T F F	F T T F	F T F T	T F T F

Here, we see that there is one truth-value assignment, that in which both ‘‘ and ‘‘ are true, that makes both “” and “” true. However, the statements “” and “” are inconsistent, because there is no truth-value assignment in which both come out as true.

|

→

T T F F

T F T F

T T F F

T F T T

T F T F

T F F F

T T F F

F T F F

T F T F

T F T T

F F T T

T T F F

Another relationship that can hold between two statements is that of having the same truth-value regardless of the truth-values of the simple statements making them up. Consider a combined truth table for the wffs “” and ““:

|

→

T T F F

T F T F

F F T T

T T F F

T T F T

F T F T

T F T F

T T F T

T F T F

F F T F

F F T T

T T F F

Here we see that these two statements necessarily have the same truth-value.

Definition: two statements are said to be logically equivalent if and only if all possible truth-value assignments to the statement letters making them up result in the same resulting truth-values for the whole statements.

The above statements are logically equivalent. However, the truth table given above for the statements “” and “” show that they, on the other hand, are not logically equivalent, because they differ in truth-value for three of the four possible truth-value assignments.

Finally, and perhaps most importantly, truth tables can be utilized to determine whether or not an argument is logically valid. In general, an argument is said to be logically valid whenever it has a form that makes it impossible for the conclusion to be false if the premises are true. (See the encyclopedia article on “Validity and Soundness“.) In classical propositional logic, we can give this a more precise characterization.

Definition: a wff is said to be a logical consequence of a set of wffs , if and only if there is no truth-value assignment to the statement letters making up these wffs that makes all of true but does not make true.

An argument is logically valid if and only if its conclusion is a logical consequence of its premises. If an argument whose conclusion is and whose only premise is is logically valid, then is said to logically imply .

For example, consider the following argument:

We can test the validity of this argument by constructing a combined truth table for all three statements.

|

→

→

T T F F

T F T F

T T F F

T F T T

T F T F

F T F T

T F T F

T T T F

T T F F

T F T F

Here we see that both premises come out as true in the case in which both ‘‘ and ‘‘ are true, and in which ‘‘ is false but ‘‘ is true. However, in those cases, the conclusion is also true. It is possible for the conclusion to be false, but only if one of the premises is false as well. Hence, we can see that the inference represented by this argument is truth-preserving. Contrast this with the following example:

Consider the truth-value assignment making both ‘‘ and ‘‘ true. If we were to fill in that row of the truth-value for these statements, we would see that “” comes out as true, but “” comes out as false. Even if ‘‘ and ‘‘ are not actually both true, it is possible for them to both be true, and so this form of reasoning is not truth-preserving. In other words, the argument is not logically valid, and its premise does not logically imply its conclusion.

One of the most striking features of truth tables is that they provide an effective procedure for determining the logical truth, or tautologyhood of any single wff, and for determining the logical validity of any argument written in the language PL. The procedure for constructing such tables is purely rote, and while the size of the tables grows exponentially with the number of statement letters involved in the wff(s) under consideration, the number of rows is always finite and so it is in principle possible to finish the table and determine a definite answer. In sum, classical propositional logic is decidable.

5. Deduction: Rules of Inference and Replacement

a. Natural Deduction

Truth tables, as we have seen, can theoretically be used to solve any question in classical truth-functional propositional logic. However, this method has its drawbacks. The size of the tables grows exponentially with the number of distinct statement letters making up the statements involved. Moreover, truth tables are alien to our normal reasoning patterns. Another method for establishing the validity of an argument exists that does not have these drawbacks: the method of natural deduction. In natural deduction an attempt is made to reduce the reasoning behind a valid argument to a series of steps each of which is intuitively justified by the premises of the argument or previous steps in the series.

Consider the following argument stated in natural language:

Either cat fur or dog fur was found at the scene of the crime. If dog fur was found at the scene of the crime, officer Thompson had an allergy attack. If cat fur was found at the scene of the crime, then Macavity is responsible for the crime. But officer Thompson didn’t have an allergy attack, and so therefore Macavity must be responsible for the crime.

The validity of this argument can be made more obvious by representing the chain of reasoning leading from the premises to the conclusion:

1. Either cat fur was found at the scene of the crime, or dog fur was found at the scene of the crime. (Premise)
2. If dog fur was found at the scene of the crime, then officer Thompson had an allergy attack. (Premise)
3. If cat fur was found at the scene of the crime, then Macavity is responsible for the crime. (Premise)
4. Officer Thompson did not have an allergy attack. (Premise)
5. Dog fur was not found at the scene of the crime. (Follows from 2 and 4.)
6. Cat fur was found at the scene of the crime. (Follows from 1 and 5.)
7. Macavity is responsible for the crime. (Conclusion. Follows from 3 and 6.)

Above, we do not jump directly from the premises to the conclusion, but show how intermediate inferences are used to ultimately justify the conclusion by a step-by-step chain. Each step in the chain represents a simple, obviously valid form of reasoning. In this example, the form of reasoning exemplified in line 5 is called modus tollens, which involves deducing the negation of the antecedent of a conditional from the conditional and the negation of its consequent. The form of reasoning exemplified in step 5 is called disjunctive syllogism, and involves deducing one disjunct of a disjunction on the basis of the disjunction and the negation of the other disjunct. Lastly, the form of reasoning found at line 7 is called modus ponens, which involves deducing the truth of the consequent of a conditional given truth of both the conditional and its antecedent. “Modus ponens” is Latin for affirming mode, and “modus tollens” is Latin for denying mode.

A system of natural deduction consists in the specification of a list of intuitively valid rules of inference for the construction of derivations or step-by-step deductions. Many equivalent systems of deduction have been given for classical truth-functional propositional logic. In what follows, we sketch one system, which is derived from the popular textbook by Irving Copi (1953). The system makes use of the language PL.

b. Rules of Inference

Here we give a list of intuitively valid rules of inference. The rules are stated in schematic form. Any inference in which any wff of language PL is substituted unformly for the schematic letters in the forms below constitutes an instance of the rule.

Modus ponens (MP):

(Modus ponens is sometimes also called “modus ponendo ponens”, “detachment” or a form of “→-elimination”.)

Modus tollens (MT):

(Modus tollens is sometimes also called “modus tollendo tollens” or a form of “→-elimination”.)

Disjunctive syllogism (DS): (two forms)

(Disjunctive syllogism is sometimes also called “modus tollendo ponens” or “-elimination”.)

Addition (Add): (two forms)

(Addition is sometimes also called “disjunction introduction” or “–introduction”.)

Simplification (Simp): (two forms)

(Simplification is sometimes also called “conjunction elimination” or “-elimination”.)

Conjunction (Conj):

(Conjunction is sometimes also called “conjunction introduction”, “-introduction” or “logical multiplication”.)

Hypothetical syllogism (HS):

(Hypothetical syllogism is sometimes also called “chain reasoning” or “chain deduction”.)

Constructive dilemma (CD):

Absorption (Abs):

c. Rules of Replacement

The nine rules of inference listed above represent ways of inferring something new from previous steps in a deduction. Many systems of natural deduction, including those initially designed by Gentzen, consist entirely of rules similar to the above. If the language of a system involves signs introduced by definition, it must also allow the substitution of a defined sign for the expression used to define it, or vice versa. Still other systems, while not making use of defined signs, allow one to make certain substitutions of expressions of one form for expressions of another form in certain cases in which the expressions in question are logically equivalent. These are called rules of replacement, and Copi’s natural deduction system invokes such rules. Strictly speaking, rules of replacement differ from inference rules, because, in a sense, when a rule of replacement is used, one is not inferring something new but merely stating what amounts to the same thing using a different combination of symbols. In some systems, rules for replacement can be derived from the inference rules, but in Copi’s system, they are taken as primitive.

Rules of replacement also differ from inference rules in other ways. Inference rules only apply when the main operators match the patterns given and only apply to entire statements. Inference rules are also strictly unidirectional: one must infer what is below the horizontal line from what is above and not vice-versa. However, replacement rules can be applied to portions of statements and not only to entire statements; moreover, they can be implemented in either direction.

The rules of replacement used by Copi are the following:

Double negation (DN):

is interreplaceable with

(Double negation is also called “-elimination”.)

Commutativity (Com): (two forms)

is interreplaceable with
is interreplaceable with

Associativity (Assoc): (two forms)

is interreplaceable with
is interreplaceable with

Tautology (Taut): (two forms)

is interreplaceable with
is interreplaceable with

DeMorgan’s Laws (DM): (two forms)

is interreplaceable with
is interreplaceable with

Transposition (Trans):

is interreplaceable with

(Transposition is also sometimes called “contraposition”.)

Material Implication (Impl):

is interreplaceable with

Exportation (Exp):

is interreplaceable with

Distribution (Dist): (two forms)

is interreplaceable with
is interreplaceable with

Material Equivalence (Equiv): (two forms)

is interreplaceable with
is interreplaceable with

(Material equivalence is sometimes also called “biconditional introduction/elimination” or “↔-introduction/elimination”.)

d. Direct Deductions

A direct deduction of a conclusion from a set of premises consists of an ordered sequence of wffs such that each member of the sequence is either (1) a premise, (2) derived from previous members of the sequence by one of the inference rules, (3) derived from a previous member of the sequence by the replacement of a logically equivalent part according to the rules of replacement, and such that the conclusion is the final step of the sequence.

To be even more precise, a direct deduction is defined as an ordered sequence of wffs, , such that for each step where i is between 1 and n inclusive, either (1) is a premise, (2) matches the form given below the horizontal line for one of the 9 inference rules, and there are wffs in the sequence prior to matching the forms given above the horizontal line, (3) there is a previous step in the sequence where and differs from at most by matching or containing a part that matches one of the forms given for one of the 10 replacement rules in the same place in whcih contains the wff of the corresponding form, and such that the conclusion of the argument is .

Using line numbers and the abbreviations for the rules of the system to annotate, the chain of reasoning given above in English, when transcribed into language PL and organized as a direct deduction, would appear as follows:

1.	Premise
2.	Premise
3.	Premise
4.	Premise
5.	2,4 MT
6.	1,5 DS
7.	2,6 MP

There is no unique derivation for a given conclusion from a given set of premises. Here is a distinct derivation for the same conclusion from the same premises:

1.	Premise
2.	Premise
3.	Premise
4.	Premise
5.	2,3 Conj
6.	1,5 CD
7.	4,6 DS

Consider next the argument:

This argument has six distinct statement letters, and hence constructing a truth table for it would require 64 rows. The table would have 22 columns, thereby requiring 1,408 distinct T/F calculations. Happily, the derivation of the conclusion of the premises using our inference and replacement rules, while far from simple, is relatively less exhausting:

1.	Premise
2.	Premise
3.	Premise
4.	1 Equiv
5.	4 Simp
6.	2,5 HS
7.	3 Impl
8.	6,7 HS
9.	8 Impl
10.	9 DM
11.	10 Dist
12.	11 Simp
13.	12 Com
14.	13 Dist
15.	14 Simp
16.	15 Taut
17.	16 Add
18.	17 Impl

e. Conditional and Indirect Proofs

Together the nine inference rules and ten rules of replacement are sufficient for creating a deduction for any logically valid argument, provided that the argument has at least one premise. However, to cover the limiting case of arguments with no premises, and simply to facillitate certain deductions that would be recondite otherwise, it is also customary to allow for certain methods of deduction other than direct derivation. Specifically, it is customary to allow the proof techniques known as conditional proof and indirect proof.

A conditional proof is a derivation technique used to establish a conditional wff, that is, a wff whose main operator is the sign ‘→’. This is done by constructing a sub-derivation within a derivation in which the antecedent of the conditional is assumed as a hypothesis. If, by using the inference rules and rules of replacement (and possibly additional sub-derivations), it is possible to arrive at the consequent, it is permissible to end the sub-derivation and conclude the truth of the conditional statement within the main derivation, citing the sub-derivation as a conditional proof, or ‘CP’ for short. This is much clearer by considering the following example argument:

While a direct derivation establishing the validity of this argument is possible, it is easier to establish the validity of this argument using a conditional derivation.

1.	Premise
2.	Premise
3.	Premise
4.	Assumption
5.	1,4 MP
6.	2,4 MP
7.	3 Equiv
8.	7 Simp
9.	6,8 MT
10.	5,9 DS
11.	4-10 CP

Here in order to establish the conditional statement ““, we constructed a sub-derivation, which is the portion found at lines 4-10. First, we assumed the truth of ‘‘, and found that with it, we could derive ‘‘. Given the premises, we therefore had shown that if ‘‘ were also true, so would be ‘‘. Therefore, on the basis of the sub-derivation we were justified in concluding ““. This is the usual methodology used in logic and mathematics for establishing the truth of a conditional statement.

Another common method is that of indirect proof, also known as proof by reductio ad absurdum. (For a fuller discussion, see the article on reductio ad absurdum in the encyclopedia.) In an indirect proof (‘IP’ for short), our goal is to demonstrate that a certain wff is false on the basis of the premises. Again, we make use of a sub-derivation; here, we begin by assuming the opposite of that which we’re trying to prove, that is, we assume that the wff is true. If on the basis of this assumption, we can demonstrate an obvious contradiction, that is, a statement of the form , we can conclude that the assumed statement must be false, because anything that leads to a contradiction must be false.

For example, consider the following argument:

While, again, a direct derivation of the conclusion for this argument from the premises is possible, it is somewhat easier to prove that “” is true by showing that, given the premises, it would be impossible for ‘‘ to be true by assuming that it is and showing this to be absurd.

1.	Premise
2.	Premise
3.	Assumption
4.	1,3 MP
5.	2,3 MP
6.	4,5 MP
7.	3,6 Conj
8.	3-7 IP

Here we were attempting to show that “” was true given the premises. To do this we assumed instead that ‘‘ was true. Since this assumption was impossible, we were justified in concluding that ‘‘ is false, that is, that “” is true.

When making use of either conditional proof or indirect proof, once a sub-derivation is finished, the lines making it up cannot be used later on in the main derivation or any additional sub-derivations that may be constructed later on.

This completes our characterization of a system of natural deduction for the language PL.

The system of natural deduction just described is formally adequate in the following sense. Earlier, we defined a valid argument as one in which there is no possible truth-value assignment to the statement letters making up its premises and conclusion that makes the premises all true but the conclusion untrue. It is provable that an argument in the language of PL is formally valid in that sense if and only if it is possible to construct a derivation of the conclusion of that argument from the premises using the above rules of inference, rules of replacement and techniques of conditional and indirect proof. Space limitations preclude a full proof of this in the metalanguage, although the reasoning is very similar to that given for the axiomatic Propositional Calculus discussed in Sections VI and VII below.

Informally, it is fairly easy to see that no argument for which a deduction is possible in this system could be invalid according to truth tables. Firstly, the rules of inference are all truth-preserving. For example, in the case of modus ponens, it is fairly easy to see from the truth table for any set of statements of the appropriate form that no truth-value assignment could make both and true while making false. A similar consideration applies for the others. Moreover, truth tables can easily be used to verify that statements of one of the forms mentioned in the rules of replacement are all logically equivalent with those the rule allows one to swap for them. Hence, the statements could never differ in truth-value for any truth-value assignment. In case of conditional proof, note that any truth-value assignment must make either the conditional true, or it must make the antecedent true and consequent false. The antecedent is what is assumed in a conditional proof. So, if the truth-value assignment makes both it and the premises of the argument true, because the other rules are all truth-preserving, it would be impossible to derive the consequent unless it were also true. A similar consideration justifies the use of indirect proof.

This system represents a useful method for establishing the validity of an argument that has the advantage of coinciding more closely with the way we normally reason. (As noted earlier, however, there are many equivalent systems of natural deduction, all coinciding relatively closely to ordinary reasoning patterns.) One disadvantage this method has, however, is that, unlike truth tables, it does not provide a means for recognizing that an argument is invalid. If an argument is invalid, there is no deduction for it in the system. However, the system itself does not provide a means for recognizing when a deduction is impossible.

Another objection that might be made to the system of deduction sketched above is that it contains more rules and more techniques than it needs to. This leads us directly into our next topic.

6. Axiomatic Systems and the Propositional Calculus

The system of deduction discussed in the previous section is an example of a natural deduction system, that is, a system of deduction for a formal language that attempts to coincide as closely as possible to the forms of reasoning most people actually employ. Natural systems of deduction are typically contrasted with axiomatic systems. Axiomatic systems are minimalist systems; rather than including rules corresponding to natural modes of reasoning, they utilize as few basic principles or rules as possible. Since so few kinds of steps are available in a deduction, relatively speaking, an axiomatic system usually requires more steps for the deduction of a conclusion from a given set of premises as compared to a natural deduction system.

Typically, an axiomatic system consists in the specification of certain wffs that are specified as “axioms”. An axiom is something that is taken as a fundamental truth of the system that does not itself require proof. To allow for the deduction of results from the axioms or the premises of an argument, the system typically also includes at least one (and often only one) rule of inference. Usually, an attempt is made to limit the number of axioms to as few as possible, or at least, limit the number of forms axioms can take.

Because axiomatic systems aim to be minimal, typically they employ languages with simplified vocabularies whenever possible. For classical truth-functional propositional logic, this might involve using a simpler language such as PL’ or PL” instead of the full language PL.

For most of the remainder of this section, we shall sketch an axiomatic system for classical truth-functional propositional logic, which we shall dub the Propositional Calculus (or PC for short). The Propositional Calculus makes use of language PL’, described above. That is, the only connectives it uses are ‘→’ and ‘‘, and the other operators, if used at all, would be understood as shorthand abbreviations making use of the definitions discussion in Section III(c).

System PC consists of three axiom schemata, which are forms a wff fits if it is axiom, along with a single inference rule: modus ponens. We make this more precise by specifying certain definitions.

Definition: a wff of language PL’ is an axiom of PC if and only if it is an instance of one of the following three forms:

	(Axiom Schema 1, or AS1)
	(Axiom Schema 2, or AS2)
	(Axiom Schema 3, or AS3)

Note that according to this definition, every wff of the form is an axiom. This includes an infinite number of different wffs, from simple cases such as ““, to much more complicated cases such as ““.

An ordered step-by-step deduction constitutes a derivation in system PC if and only if each step in the deduction is either (1) a premise of the argument, (2) an axiom, or (3) derived from previous steps by modus ponens. Once again we can make this more precise with the following (more recondite) definition:

Definition: an ordered sequence of wffs is a derivation in system PC of the wff from the premises if and only if, for each wff in the sequence , either (1) is one of the premises , (2) is an axiom of PC, or (3) follows from previous members of the series by the inference rule modus ponens (that is, there are previous members of the sequence, and , such that takes the form ).

For example, consider the following argument written in the language PL’:

The following constitutes a derivation in system PC of the conclusion from the premises:

1.	Premise
2.	Premise
3.	Instance of AS1
4.	1,3 MP
5.	2,4 MP
6.	Instance of AS2
7.	5,6 MP
8.	4,7 MP

Historically, the original axiomatic systems for logic were designed to be akin to other axiomatic systems found in mathematics, such as Euclid’s axiomatization of geometry. The goal of developing an axiomatic system for logic was to create a system in which to derive truths of logic making use only of the axioms of the system and the inference rule(s). Those wffs that can be derived from the axioms and inference rule alone, that is, without making use of any additional premises, are called theorems or theses of the system. To make this more precise:

Definition: a wff is said to be a theorem of PC if and only if there is an ordered sequence of wffs, specifically, a derivation, such that, is and each wff in the sequence , is such that either (1) is an axiom of PC, or (2) follows from previous members of the series by modus ponens.

One very simple theorem of system PC is the wff ““. We can show that it is a theorem by constructing a derivation of “” that makes use only of axioms and MP and no additional premises.

1.	Instance of AS1
2.	Instance of AS1
3.	Instance of AS2
4.	2,3 MP
5.	1,4 MP

It is fairly easy to see that not only is “” a theorem of PC, but so is any wff of the form . Whatever happens to be, there will be a derivation in PC of the same form:

1.	Instance of AS1
2.	Instance of AS1
3.	Instance of AS2
4.	2,3 MP
5.	1,4 MP

So even if we make in the above the more complicated wff, for example, ““, a derivation with the same form shows that “” is also a theorem of PC. Hence, we call a theorem schema of PC, because all of its instances are theorems of PC. From now on, let’s call it “Theorem Schema 1”, or “TS1” for short.

The following are also theorem schemata of PC:

	(Theorem Schema 2, or TS2)
	(TS3)
	(TS4)
	(TS5)

You may wish to verify this for yourself by attempting to construct the appropriate proofs for each. Be warned that some require quite lengthy derivations!

It is common to use the notation:

to mean that β is a theorem. Similarly, it is common to use the notation:

to mean that it is possible to construct a derivation of making use of as premises.

Considered in terms of number of rules it employs, the axiomatic system PC is far less complex than the system of natural deduction sketched in the previous section. The natural deduction system made use of nine inference rules, ten rules of replacement and two additional proof techniques. The axiomatic system instead, makes use of three axiom schemata and a single inference rule and no additional proof techniques. Yet, the axiomatic system is not lacking in any way.

Indeed, for any argument using language PL’ that is logically valid according to truth tables it is possible to construct a derivation in system PC for that argument. Moreover, every wff of language PL’ that is a logical truth, that is, a tautology according to truth tables, is a theorem of PC. The reverse of these results is true as well; every theorem of PC is a tautology, and every argument for which a derivation in system PC exists is logically valid according to truth tables. These and other features of the Propositional Calculus are discussed, and some are even proven in the next section below.

While the Propositional Calculus is simpler in one way than the natural deduction system sketched in the previous section, in many ways it is actually more complicated to use. For any given argument, a deduction of the conclusion from the premises conducted in PC is likely to be far longer and less psychologically natural than one carried out in a natural deduction system. Such deductions are only simpler in the sense that fewer distinct rules are employed.

System PC is only one of many possible ways of axiomatizing propositional logic. Some systems differ from PC in only very minor ways. For example, we could alter our definition of “axiom” so that a wff is an axiom iff it is an instance of (A1), an instance of (A2), or an instance of the following:

(A3′)

Replacing axiom schema (A3) with (A3′), while altering the way certain deductions must be constructed (making the proofs of many important results longer), has little effect otherwise; the resulting system would have all the same theorems and every argument for which a deduction is possible in the system above would also have a deduction in the revised system, and vice versa.

We also noted above that, strictly speaking, there are an infinite number of axioms of system PC. Instead of utilizing an infinite number of axioms, we might alternatively have utilized only three axioms, namely, the specific wffs:

(A1*)
(A2*)
(A3*)

Note that (A1*) is just a unique wff; on this approach, the wff “” would not count as an axiom, even though it shares a common form with (A1*). To such a system it would be necessary to add an additional inference rule, a rule of substitution or uniform replacement. This would allow one to infer, from a theorem of the system, the result of uniformly replacing any given statement letter (for example, ‘‘ or ‘‘) that occurs within the theorem, with any wff, simple or complex, provided that the same wff replaces all occurrences of the same statement letter in the theorem. On this approach, ““, while not an axiom, would still be a theorem because it could be derived from the rule of uniform replacement twice, that is, by first replacing ‘‘ in (A1*) with ““, and then replacing ‘‘ with ““. The resulting system differs in only subtle ways from our earlier system PC. System PC, strictly speaking, uses only one inference rule, but countenances an infinite number of axioms. This system uses only three axioms, but makes use of an additional rule. System PC, however, avoids this additional inference rule by allowing everything that one could get by substitution in (A1*) to be an axiom. For every theorem , therefore, if is a wff obtained from by uniformly substituting wffs for statement letters in , then is also a theorem of PC, because there would always be a proof of analogous to the proof of only beginning from different axioms.

It is also possible to construct even more austere systems. Indeed, it is possible to utilize only a single axiom schema (or a single axiom plus a rule of replacement). One possibility, suggested by C. A. Meredith (1953), would be to define an axiom as any wff matching the following form:

The resulting system is equally powerful as system PC and has exactly the same set of theorems. However, it is far less psychologically intuitive and straightforward, and deductions even for relatively simple results are often very long.

Historically, the first single axiom schema system made use, instead of language PL’, the even simpler language PL” in which the only connective is the Sheffer stroke, ‘|’, as discussed above. In that case, it is possible to make use only of the following axiom schema:

The inference rule of MP is replaced with the rule that from wffs of the form and , one can deduce the wff . This system was discovered by Jean Nicod (1917). Subsequently, a number of possible single axiom systems have been found, some faring better than others in terms of the complexity of the single axiom and in terms of how long deductions for the same results are required to be. (For research in this area, consult McCune et. al. 2002.) Generally, however the more the system allows, the shorter the deductions.

Besides axiomatic and natural deduction forms, deduction systems for propositional logic can also take the form of a sequent calculus; here, rather than specifying definitions of axioms and inference rules, the rules are stated directly in terms of derivability or entailment conditions; for example, one rule might state that if (either or ) then if , then . Sequent calculi, like modern natural deduction systems, were first developed by Gerhard Gentzen. Gentzen’s work also suggests the use of tree-like deduction systems rather than linear step-by-step deduction systems, and such tree systems have proven more useful in automated theorem-proving, that is, in the creation of algorithms for the mechanical construction of deductions (for example, by a computer). However, rather then exploring the details of these and other rival systems, in the next section, we focus on proving things about the system PC, the axiomatic system treated at length above.

7. Important Meta-Theoretic Results for the Propositional Calculus

Note: this section is relatively more technical, and is designed for audiences with some prior background in logic or mathematics. Beginners may wish to skip to the next section.

In this section, we sketch informally the proofs given for certain important features of the Propositional Calculus. Our first topic, however, concerns the language PL’ generally.

Metatheoretic result 1: Language PL’ is expressively adequate, that is, within the context of classical bivalent logic, there are no truth-functions that cannot be represented in it.

We noted in Section III(c) that the connectives ‘‘, ‘↔’ and ‘‘ can be defined using the connectives of PL’ (‘→’ and ‘‘). More generally, metatheoretic result 1 holds that any statement built using truth-functional connectives, regardless of what those connectives are, has an equivalent statement formed using only ‘→’ and ‘‘. Here’s the proof.

1. Assume that is some wff built in some language containing any set of truth-functional connectives, including those not found in PL, PL’ or PL”. For example, might make use of some three or four-place truth-functional connectives, or connectives such as the exclusive or, or the sign ‘‘, or any others you might imagine.

2. We need to show that there is a wff formed only with the connectives ‘→’ and ‘‘ that is logically equivalent with . Because we have already shown that forms equivalent to those built from ‘‘, ‘↔’, and ‘‘ can be constructed from ‘→’ and ‘‘, we are entitled to use them as well.

3. In order for it to be logically equivalent to , the wff that we construct must have the same final truth-value for every possible truth-value assignment to the statement letters making up , or in other words, it must have the same final column in a truth table.

4. Let be the distinct statement letters making up . For some possible truth-value assignments to these letters, may be true, and for others may be false. The only hard case would be the one in which is contingent. If were not contingent, it must either be a tautology, or a self-contradiction. Since clearly tautologies and self-contradictions can be constructed in PL’, and all tautologies are logically equivalent to one another, and all self-contradictions are equivalent to one another, in those cases, our job is easy. Let us suppose instead that is contingent.

5. Let us construct a wff in the following way.

(a) Consider in turn each truth-value assignment to the letters . For each truth-value assignment, construct a conjunction made up of those letters the truth-value assignment makes true, along with the negations of those letters the truth-value assignment makes false. For instance, if the letters involved are ‘‘, ‘‘ and ‘‘, and the truth-value assignment makes ‘‘ and ‘‘ true but ‘‘ false, consider the conjunction ‘‘.

(b) From the resulting conjunctions, form a complex disjunction formed from those conjunctions formed in step (a) for which the corresponding truth-value assignment makes true. For example, if the truth-value assignment making ‘‘ and ‘‘ true but ‘‘ false makes true, include it the disjunction. Suppose, for example, that this truth-value assignment does make true, as does that assignment in which ‘‘ and ‘‘ and ‘‘ are all made false, but no other truth-value assignment makes true. In that case, the resulting disjunction would be ‘‘.

6. The wff constructed in step 5 is logically equivalent to . Consider that for those truth-value assignments making true, one of the conjunctions making up the disjunction is true, and hence the whole disjunction is true as well. For those truth-value assignments making false, none of the conjunctions making up is true, because each conjunction will contain at least one conjunct that is false on that truth-value assignment.

7. Because is constructed using only ‘‘, ‘‘ and ‘‘, and these can in turn be defined using only ‘‘ and ‘→’, and because is equivalent to , there is a wff built up only from ‘‘ and ‘→’ that is equivalent to , regardless of the connectives making up .

8. Therefore, PL’ is expressively adequate.

Corollary 1.1: Language PL” is also expressively adequate.

The corollary follows at once from metatheoretic result 1, along with the fact, noted in Section III(c), that ‘→’, and ‘‘ can be defined using only ‘|’.

Metatheoretic result 2 (a.k.a. “The Deduction Theorem”): In the Propositional Calculus, PC, whenever it holds that , it also holds that

What this means is that whenever we can prove a given result in PC using a certain number of premises, then it is possible, using all the same premises leaving out one exception, , to prove the conditional statement made up of the removed premise, , as antecedent and the conclusion of the original derivation, , as consequent. The importance of this result is that, in effect, it shows that the technique of conditional proof, typically found in natural deduction (see Section V), is unnecessary in PC, because whenever it is possible to prove the consequent of a conditional by taking the antecedent as an additional premise, a derivation directly for the conditional can be found without taking the antecedent as a premise.

Here’s the proof:

1. Assume that . This means that there is a derivation of in the Propositional Calculus from the premises . This derivation takes the form of an ordered sequence , where the last member of the sequence, , is , and each member of the sequence is either (1) a premise, that is, it is one of , (2) an axiom of PC, (3) derived from previous members of the sequence by modus ponens.

2. We need to show that there is a derivation of , which, while possibly making use of the other premises of the argument, does not make use of . We’ll do this by showing that for each member, , of the sequence of the original derivation: , one can derive without making use of as a premise.

3. Each step in the sequence of the original derivation was gotten at in one of three ways, as mentioned in (1) above. Regardless of which case we are dealing with, we can get the result that . There are three cases to consider:

Case (a): Suppose is a premise of the original argument. Then is either one of or it is itself. In the latter subcase, what we desire to get is that can be gotten at without using as a premise. Because is an instance of TS1, we can get it without using any premises. In the latter case, notice that is one of the premises we’re allowed to use in the new derivation. We’re also allowed to introduce the instance of AS1, . From these, we can get by modus ponens.

Case (b): Suppose is an axiom. We need to show that we can get without using as a premise. In fact, we can get it without using any premises. Because is an axiom, we can use it in the new derivation as well. As in the last case, we have as another axiom (an instance of AS1). From these two axioms, we arrive at by modus ponens.

Case (c): Suppose that was derived from previous members of the sequence by modus ponens. Specifically, there is some and such that both j and k are less than i, and takes the form . We can assume that we have already been able to derive both —that is, —and in the new derivation without making use of . (This may seem questionable in the case that either or was itself gotten at by modus ponens. But notice that this just pushes the assumption back, and eventually one will reach the beginning of the original derivation. The first two steps of the sequence, namely, and , cannot have been derived by modus ponens, since this would require there to have been two previous members of the sequence, which is impossible.) So, in our new derivation, we already have both and .
Notice that is an instance of AS2, and so it can be introduced in the new derivation. By two steps of modus ponens, we arrive at , again without using as a premise.

4. If we continue through each step of the original derivation, showing for each such step , we can get without using as a premise, eventually, we come to the last step of the original derivation, , which is itself. Applying the procedure from step (3), we get that without making use of as a premise. Therefore, the new derivation formed in this way shows that , which is what we were attempting to show.

What’s interesting about this proof for metatheoretic result 2 is that it provides a recipe, given a derivation for a certain result that makes use of one or more premises, for transforming that derivation into one of a conditional statement in which one of the premises of the original argument has become the antecedent. This may be much clearer with an example.

Consider the following derivation for the result that :

1.	Premise
2.	AS1
3.	1,2 MP
4.	AS2
5.	3,4 MP

It is possible to transform the above derivation into one that uses no premises and that shows that is a theorem of PC. The procedure for such a transformation involves looking at each step of the original derivation, and for each one, attempting to derive the same statement, only beginning with ““, without making use of “” as a premise. How this is done depends on whether the step is a premise, an axiom, or a result of modus ponens, and depending on which it is, applying one of the three procedures sketched in the proof above. The result is the following:

1.	TS1
2.	AS1
3.	AS1
4.	2,3 MP
5.	AS2
6.	4,5 MP
7.	1,6 MP
8.	AS2
9.	AS1
10.	8,9 MP
11.	AS2
12.	10,11 MP
13.	7,12 MP

The procedure for transforming one sort of derivation into another is purely rote. Moreover, the result is quite often not the most elegant or easy way to show that which you were trying to show. Notice, for example, in the above that lines (2) and (7) are redudant, and more steps were taken than necessary. However, the purely rote procedure is effective.

This metatheoretic result is due to Jacques Herbrand (1930).

It is interesting on its own, especially when one reflects on it as a substitution or replacement for the conditional proof technique. However, it is also very useful for proving other metatheoretic results, as we shall see below.

Metatheoretic result 3: If is a wff of language PL’, and the statement letters making it up are , then if we consider any possible truth-value assignment to these letters, and consider the set of premises, , that contains if the truth-value assignment makes true, but contains if the truth-value assignment makes false, and similarly for , if the truth-value assignment makes true, then in PC, it holds that , and if it makes false, then .

Here’s the proof.

1. By the definition of a wff, is either itself a statement letter, or ultimately built up from statement letters by the connectives ‘‘ and ‘→’.

2. If is itself a statement letter, then obviously either it or its negation is a member of . It is a member of if the truth-value assignment makes it true. In that case, obviously, there is a derivation of from , since a premise maybe introduced at any time. If the truth-value assignment makes it false instead, then is a member of , and so we have a derivation of from , since again a premise may be introduced at any time. This covers the case in which our wff is simply a statement letter.

3. Suppose that is built up from some other wff with the sign ‘‘, that is, suppose that is . We can assume that we have already gotten the desired result for . (Either is a statement letter, in which case the result holds by step (2), or is itself ultimately built up from statement letters, so even if verifying this assumption requires making a similar assumption, ultimately we will get back to statement letters.) That is, if the truth-value assignment makes true, then we have a derivation of from . If it makes it false, then we have a derivation of from . Suppose that it makes true. Since is the negation of , the truth-value assignment must make false. Hence, we need to show that there is a derivation of from . Since is , is . If we append to our derivation of from the derivation of , an instance of TS2, we can reach a derivation of by modus ponens, which is what was required. If we assume instead that the truth-value assignment makes false, then by our assumption, there is a derivation of from . Since is the negation of , this truth-value assigment must make true. Now, simply is , so we already have a derivation of it from .

4. Suppose instead that is built up from other wffs and with the sign ‘→’, that is, suppose that is . Again, we can assume that we have already gotten the desired result for and . (Again, either they themselves are statement letters or built up in like fashion from statement letters.) Suppose that the truth-value assignment we are considering makes true. Because is , by the semantics for the sign ‘→’, the truth-value assignment must make either false or true. Take the first subcase. If it makes false, then by our assumption, there is a derivation of from . If we append to this the derivation of the instance of TS3, , by modus ponens we arrive at derivation of , that is, , from . If instead, the truth-value assignment makes true, then by our assumption there is a derivation of from . If we add to this derivation the instance of AS1, , by modus ponens, we then again arrive at a derivation of , that is, , from . If instead, the truth-value assignment makes false, then since is , the truth-value assignment in question must make true and false. By our assumption, then it is possible to prove both and from . If we concatenate these two derivations, and add to them the derivation of the instance of TS4, , then by two applications of modus ponens, we can derive , which is simply , which is what was desired.

From the above we see that the Propositional Calculus PC can be used to demonstrate the appropriate results for a complex wff if given as premises either the truth or falsity of all its simple parts. This is of course the foundation of truth-functional logic, that the truth or falsity of those complex statements one can make in it be determined entirely by the truth or falsity of the simple statements entering in to it. Metatheoretic result 3 is again interesting on its own, but it plays a crucial role in the proof of completeness, which we turn to next.

Metatheoretic result 4 (Completeness): If is a wff of language PL’ and a tautology, then is a theorem of the Propositional Calculus.

This feature of the Propositional Calculus is called completeness because it shows that the Propositional Calculus, as a deductive system aiming to capture all the truths of logic, is a success. Every wff true solely in virtue of the truth-functional nature of the connectives making it up is something that one can prove using only the axioms of PC along with modus ponens. Here’s the proof:

1. Suppose that is a tautology. This means that every possible truth-value assignment to its statement letters makes it true.

2. Let the statement letters making up be , arranged in some order (say alphabetically and by the numerical order of their subscripts). It follows from (1) and metatheoretic result 3, that there is a derivation in PC of using any possible set of premises that consists, for each statement letter, of either it or its negation.

3. By metatheoretic result 2, we can remove from each of these sets of premises either or , depending on which it contains, and make it an antecedent of a conditional in which is consequent, and the result will be provable without using or as a premise. This means that for every possible set of premises consisting of either or and so on, up until , we can derive both and .

4. The wff is an instance of TS5. Therefore, for any set of premises from which one can derive both and , by two applications of modus ponens, one can also derive itself.

5. Putting (3) and (4) together, we have the result that can be derived from every possible set of premises consisting of either or and so on, up until .

6. We can apply the same reasoning given in steps (3)-(5) to remove or its negation from the premise sets by the deduction theorem, arriving at the result that for every set of premises consisting of either or and so on, up until , it is possible to derive . If we continue to apply this reasoning, eventually, we’ll get the result that we can derive with either or its negation as our sole premise. Again, applying the deduction theorem, this means that both and can be proven in PC without using any premises, that is, they are theorems. Concatenating the derivations of these theorems, along with the instance of TS5, , and by two applications of modus ponens, it follows that itself is a theorem, which is what we sought to demonstrate.

The above proof of the completeness of system PC is easier to appreciate when visualized. Suppose, just for the sake of illustration, that the tautology we wish to demonstrate in system PC has three statement letters, ‘‘, ‘‘ and ‘‘. There are eight possible truth-value assignments to these letters, and since is a tautology, all of them make true. We can sketch in at least this much of ‘s truth table:

			|
T T T T F F F F	T T F F T T F F	T F T F T F T F		T T T T T T T T

Now, given this feature of , it follows from metatheoretic result 3, that for every possible combination of premises that consists of either ‘‘ or “” (but not both), either ‘‘ or ““, and ‘‘ or ““, it is possible from those premises to construct a derivation showing . This can be visualized as follows:

By the deduction theorem, we can pull out the last premise from each list of premises and make it an antecedent. However, because from the same remaining list of premises we get both and , we can get by itself from those premises according to TS5. Again, to visualize this:

		… and so
		… and so
		… and so
		… and so

We can continue this line of reasoning until all the premises are removed.

		and so	and so	and so
		and so	and so

At the end of this process, we see that is a theorem. Despite only having three axiom schemata and a single inference rule, it is possible to prove any tautology in the simple Propositional Calculus, PC. It is complete in the requisite sense.

This method of proving the completeness of the Propositional Calculus is due to Kalmár (1935).

Corollary 4.1: If a given wff of language PL’ is a logical consequence of a set of wffs , according to their combined truth table, then there is a derivation of with as premises in the Propositional Calculus.

Without going into the details of the proof of this corollary, it follows from the fact that if is a logical consequence of , then the wff of the form is a tautology. As a tautology, it is a theorem of PC, and so if one begins with its derivation in PC and appends a number of steps of modus ponens using as premises, one can derive .

Metatheoretic result 5 (Soundness): If a wff is a theorem of the Propositional Calculus (PC), then is a tautology.

Above, we saw that all tautologies are theorems of PC. The reverse is also true: all theorems of PC are tautologies. Here’s the proof:

1. Suppose that is a theorem of PC. This means that there is an ordered sequence of steps, each of which is either (1) an axiom of PC, or (2) derived from previous members of the sequence by modus ponens, and such that is the last member of the sequence.

2. We can show that not only is a tautology, but so are all the members of the sequence leading to it. The first thing to note is that every axiom of PC is a tautology. To be an axiom of PC, a wff must match one of the axiom schemata AS1, AS2 or AS3. All such wffs must be tautologous; this can easily be verified by constructing truth tables for AS1, AS2 and AS3. (This is left to the reader.)

3. The rule of modus ponens preserves tautologyhood. If is a tautology and is also a tautology, must be a tautology as well. This is because if were not a tautology, it would be false on some truth-value assignments. However, , as a tautology, is true for all truth-value assignments. Because a statement of the form is false for any truth-value assignment making true and false, it would then follow that some truth-value assignment makes false, which is impossible if it too is a tautology.

4. Hence, we see that the axioms with which we begin the sequence, and every step derived from them using modus ponens, must all be tautologies, and consequently, the last step of the sequence, , must also be a tautology.

This result is called the soundness of the Propositional Calculus; it shows that in it, one cannot demonstrate something that is not logically true.

Corollary 5.1: A wff of language PL’ is a tautology if and only if is a theorem of system PC.

This follows immediately from metatheoretic results 4 and 5.

Corollary 5.2 (Consistency): There is no wff of language PL’ such that both and are theorems of the Propositional Calculus (PC).

Due to metatheoretic result 5, all theorems of PC are tautologies. It is therefore impossible for both and to be theorems, as this would require both to be tautologies. That would mean that both are true for all truth-value assignments, but obviously, they must have different truth-values for any given truth-value assignment, and cannot both be true for any, much less all, such assignments.

This result is called consistency because it guarantees that no theorem of system PC can be inconsistent with any other theorem.

Corollary 5.3: If there is a derivation of the wff with as premises in the Propositional Calculus, then is a logical consequence of the set of wffs , according to their combined truth table.

This is the converse of Corollary 4.1. It follows by the reverse reasoning involved in that corollary. If there is a derivation of taking as premises, then by multiple applications of the deduction theorem (Metatheoretic result 2), it follows that is a theorem of PC. By metatheoretic result 5, must be a tautology. If so, then there cannot be a truth-value assignment making all of true while making false, and so is a logical consequence of .

Corollary 5.4: There is a derivation of the wff with as premises in the Propositional Calculus if and only if is a logical consequence of , according to their combined truth table.

This follows at once from corollaries 4.1 and 5.3. In sum, then, the Propositional Calculus method of demonstrating something to follow from the axioms of logic is extensionally equivalent to the truth table method of determining whether or not something is a logical truth. Similarly, the truth-table method for testing the validity of an argument is equivalent to the test of being able to construct a derivation for it in the Propositional Calculus. In short, the Propositional Calculus is exactly what we wanted it to be.

Corollary 5.5 (Decidability): The Propositional Calculus (PC) is decidable, that is, there is a finite, effective, rote procedure for determining whether or not a given wff is a theorem of PC or not.

By Corollary 5.1, a wff is a theorem of PC if and only if it is a tautology. Truth tables provide a rote, effective, and finite procedure for determining whether or not a given wff is a tautology. They therefore also provide such a procedure for determining whether or not a given wff is a theorem of PC.

8. Forms of Propositional Logic

So far we have focused only on classical, truth-functional propositional logic. Its distinguishing features are (1) that all connectives it uses are truth-functional, that is, the truth-values of complex statements formed with those connectives depend entirely on the truth-values of the parts, and (2) that it assumes bivalence: all statements are taken to have exactly one of two truth-values—truth or falsity—with no statement assigned both truth-values or neither. Classical truth-functional propositional logic is the most widely studied and discussed form, but there are other forms of propositional logic.

Perhaps the most well known form of non-truth-functional propositional logic is modal propositional logic. Modal propositional logic involves introducing operators into the logic involving necessity and possibility, usually along with truth-functional operators such as ‘→’, ‘‘, ‘‘, etc.. Typically, the sign ‘‘ is used in place of the English operator, “it is necessary that…”, and the sign ‘‘ is used in place of the English operator “it is possible that…”. Sometimes both these operators are taken as primitive, but quite often one is defined in terms of the other, since would appear to be logically equivalent with . (Roughly, it means the same to say that something is not necessarily not true as it does to say that it is possibly true.)

To see that modal propositional logic is not truth-functional, just consider the following pair of statements:

The first states that it is necessary that . Let us suppose in fact that ‘‘ is true, but might have been false. Since is not necessarily true, the statement “” is false. However, the statement “” is a tautology and so it could not be false. Hence, the statement “” is true. Notice that both ‘‘ and “” are true, but different truth-values result when the operator ‘‘ is added. So, in modal propositional logic, the truth-value of a statement does not depend entirely on the truth-values of the parts.

The study of modal propositional logic involves identifying under what conditions statements involving the operators ‘‘ and ‘‘ should be regarded as true. Different notions or conceptions of necessity lead to different answers to that question. It also involves discovering what inference rules or systems of deduction would be appropriate given the addition of these operators. Here, there is more controversy than with classical truth-functional logic. For example, in the context of discussions of axiomatic systems for modal propositional logic, very different systems result depending on whether instances of the following schemata are regarded as axiomatic truths, or even truths at all:

If a statement is necessary, is it necessarily necessary? If a statement is possible, is it necessarily possible? A positive answer to the first question is a key assumption in a logical system known as S4 modal logic. Positive answers to both these questions are key assumptions in a logical system known as S5 modal logic. Other systems of modal logic that avoid such assumptions have also been developed. (For an excellent introduction survey, see Hughes and Cresswell 1996.)

Deontic propositional logic and epistemic propositional logic are two other forms of non-truth-functional propositional logic. The former involves introduction of operators similar to the English operators “it is morally obligatory that…” and “it is morally permissible that…”. Obviously, some things that are in fact true were not morally obligatory, whereas some things that are true were morally obligatory. Again, the truth-value of a statement in deontic logic does not depend wholly on the truth-value of the parts. Epistemic logic involves the addition of operators similar to the English operators “it is known that…” and “it is believed that …”. While everything that is known to be the case is in fact the case, not everything that is the case is known to be the case, so a statement built up with a “it is known that…” will not depend entirely on the truth of the proposition it modifies, even if it depends on it to some degree.

Yet another widely studied form of non-truth-functional propositional logic is relevance propositional logic, which involves the addition of an operator ‘‘ used to connect two statements and to form a statement , which is interpreted to mean that is related to in theme or subject matter. For example, if ‘‘ means that Ben loves Jennifer and ‘‘ means that Jennifer is a pop star, then the statement “” is regarded as true; whereas if ‘‘ means The sun is shining in Tokyo, then “” is false, and hence “” is true. Obviously, whether or not a statement formed using the connective ‘‘ is true does not depend solely on the truth-value of the propositions involved.

One of the motivations for introducing non-truth-functional propositional logics is to make up for certain oddities of truth-functional logic. Consider the truth table for the sign ‘→’ used in Language PL. A statement of the form is regarded as true whenever its antecedent is false or consequent is true. So if we were to translate the English sentence, “if the author of this article lives in France, then the moon is made of cheese” as ““, then strangely, it comes out as true given the semantics of the sign ‘→’ because the antecedent, ‘‘, is false. In modal propositional logic it is possible to define a much stronger sort of operator to use to translate English conditionals as follows:

⥽ is defined as

If we transcribe the English “if the author of this article lives in France, then the moon is made of cheese” instead as “ ⥽ “, then it does not come out as true, because presumably, it is possible for the author of this article to live in France without the moon being made of cheese. Similarly, in relevance logic, one could also define a stronger sort of connective as follows:

is defined as

Here too, if we were to transcribe the English “if the author of this article lives in France, then the moon is made of cheese” as “” instead of simply ““, it comes out as false, because the author of this article living in France is not related to the composition of the moon.

Besides non-truth-functional logic, other logical systems differ from classical truth-functional logic by allowing statements to be assigned truth-values other than truth or falsity, or to be assigned neither truth nor falsity or both truth and falsity. These sorts of logical systems may still be truth-functional in the sense that the truth-value of a complex statement may depend entirely on the truth-values of the parts, but the rules governing such truth-functionality would be more complicated than for classical logic, because it must consider possibilities that classical logic rejects.

Many-valued or multivalent logics are those that consider more than two truth-values. They may admit anything from three to an infinite number of possible truth-values. The simplest sort of many-valued logic is one that admits three truth-values, for example, truth, falsity and indeterminancy. It might seem, for example, that certain statements such as statements about the future, or paradoxical statements such as “this sentence is not true” cannot easily be assigned either truth or falsity, and so, it might be concluded, must have an indeterminate truth-value. The admission of this third truth-value requires one to expand the truth tables given in Section III(a). There, we gave a truth table for statements formed using the operator ‘→’; in three-valued logic, we have to decide what the truth-value of a statement of the form is when either or both of and has an indeterminate truth-value. Arguably, if any component of a statement is indeterminate in truth-value, then the whole statement is indeterminate as well. This would lead to the following expanded truth table:

T T T I I I F F F	T I F T I F T I F	T I F I I I T I T

However, we might wish to retain the feature of classical logic that a statement of the form is always true when its antecedent is false or its consequent is true, and hold that it is indeterminate only when its antecedent is indeterminate and its consequent false or when its antecedent is true and its consequent indeterminate, so that its truth table appears:

T T T I I I F F F	T I F T I F T I F	T I F T T I T T T

Such details will have an effect on the remainders of the logical systems. For example, if an axiomatic or natural deduction system is created, and a desirable feature is that something be provable from no premises if and only if it is a tautology in the sense of being true (and not just not false) for all possible truth-value assignments, if we make use of the first truth table for ‘→’, then “” should not be provable, because it is indeterminate when ‘‘ is, whereas if we use the second truth table, then “” should be provable, since it is a tautology according to that truth table, that is, it is true regardless of which of the three truth-values is assigned to ‘‘.

Here we get just a glimpse at the complications created by admitting more than two truth-values. If more than three are admitted, and possibly infinitely many, then the issues become even more complicated.

Intuitionistic propositional logic results from rejecting the assumption that every statement is true or false, and countenances statements that are neither. The result is a sort of logic very much akin to a three-valued logic, since “neither true nor false”, while strictly speaking the rejection of a truth-value, can be thought of as though it were a third truth-value. In intuitionistic logic, the so-called “law of excluded middle,” that is, the law that all statements of the form are true is rejected. This is because intuitionistic logic takes truth to coincide with direct provability, and it may be that certain statements, such as Goldbach’s conjecture in mathematics, are neither provably the case nor provably not the case.

Paraconsistent propositional logic is even more radical, in countenancing statements that are both true and false. Again, depending on the nature of the system, semantic rules have to be given that determine what the truth-value or truth-values a complex statement has when its component parts are both true and false. Such decisions determine what sorts of new or restricted rules of inference would apply to the logical system. For example, paraconsistent logics, if not trivial, must restrict the rules of inference allowable in classical truth-functional logic, because in systems such as those sketched in Sections V and VI above, from a contradiction, that is, a statement of the form , it is possible to deduce any other statement. Consider, for example, the following deduction in the natural deduction system sketched in Section V.

1.	Premise
2.	1 Simp
3.	1 Simp
4.	2 Add
5.	3,4 DS

In order to avoid this result, paraconsistent logics must restrict the notion of a valid inference. In order for an inference to be considered valid, not only must it be truth-preserving, that is, that it be impossible to arrive at something untrue when starting with true premises, it must be falsity-avoiding, that is, it must be impossible, starting with true premises, to arrive at something that is false. In paraconsistent logic, where a statement can be both true and false, these two requirements do not coincide. The inference rule of disjunctive syllogism, while truth-preserving, is not falsity-avoiding. In cases in which its premises are true, its conclusion can still be false; more specifically, provided that at least one of its premises is both true and false, its conclusion can be false.

Other forms of non-classical propositional logic, and non-truth-functional propositional logic, continue to be discovered. Obviously any deviance from classical bivalent propositional logic raises complicated logical and philosophical issues that cannot be fully explored here. For more details both on non-classical logic, and on non-truth-functional logic, see the recommended reading section.

9. Suggestions for Further Reading

• Anderson, A. R. and N. D. Belnap [and J. M. Dunn]. 1975 and 1992. Entailment. 2 vols. Princeton, NJ: Princeton University Press.
• Bocheński, I. M. 1961. A History of Formal Logic. Notre Dame, Ind.: University of Notre Dame Press.
• Boole, George. 1847. The Mathematical Analysis of Logic. Cambridge: Macmillan.
• Boole, George. 1854. An Investigation into the Laws of Thought. Cambridge: Macmillan.
• Carroll, Lewis. 1958. Symbolic Logic and the Game of Logic. London: Dover.
• Church, Alonzo. 1956. Introduction to Mathematical Logic. Princeton, NJ: Princeton University Press.
• Copi, Irving. 1953. Introduction to Logic. New York: Macmillan.
• Copi, Irving. 1974. Symbolic Logic. 4th ed. New York: Macmillan.
• da Costa, N. C. A. 1974. “On the Theory of Inconsistent Formal Systems,” Notre Dame Journal of Formal Logic 25: 497-510.
• De Morgan, Augustus. 1847. Formal Logic. London: Walton and Maberly.
• Fitch, F. B. 1952. Symbolic Logic: An Introduction. New York: Ronald Press.
• Frege, Gottlob. 1879. Begriffsschrift, ene der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle: L. Nerbert. Published in English as Conceptual Notation, ed. and trans. by Terrell Bynum. Clarendon: Oxford, 1972.
• Frege, Gottlob. 1923. “Gedankengefüge,” Beträge zur Philosophie des deutchen Idealismus 3: 36-51. Published in English as “Compound Thoughts,” in The Frege Reader, edited by Michael Beaney. Oxford: Blackwell, 1997.
• Gentzen, Gerhard. 1934. “Untersuchungen über das logische Schließen” Mathematische Zeitschrift 39: 176-210, 405-31. Published in English as “Investigations into Logical Deduction,” in Gentzen 1969.
• Gentzen, Gerhard. 1969. Collected Papers. Edited by M. E. Szabo. Amsterdam: North-Holland Publishing.
• Haack, Susan. 1996. Deviant Logic, Fuzzy Logic. Chicago: University of Chicago Press.
• Herbrand, Jacques. 1930. “Recherches sur la théorie de la démonstration,” Travaux de la Société des Sciences et de la Lettres de Varsovie 33: 133-160.
• Hilbert, David and William Ackermann. 1950. Principles of Mathematical Logic. New York: Chelsea.
• Hintikka, Jaakko. 1962. Knowledge and Belief: An Introduction to the Logic of the Two Notions. Ithaca: Cornell University Press.
• Hughes, G. E. and M. J. Cresswell. 1996. A New Introduction to Modal Logic. London: Routledge.
• Jevons, W. S. 1880. Studies in Deductive Logic. London: Macmillan.
• Kalmár, L. 1935. “Über die Axiomatisierbarkeit des Aussagenkalküls,” Acta Scientiarum Mathematicarum 7: 222-43.
• Kleene, Stephen C. 1952. Introduction to Metamathematics. Princeton, NJ: Van Nostrand.
• Kneale, William and Martha Kneale. 1962. The Development of Logic. Clarendon: Oxford.
• Lewis, C. I. and C. H. Langford. 1932. Symbolic Logic. New York: Dover.
• Łukasiewicz, Jan. 1920. “O logice trojwartosciowej,” Ruch Filozoficny 5: 170-171. Published in English as “On Three-Valued Logic,” in Łukasiewicz 1970.
• Łukasiewicz, Jan. 1970. Selected Works. Amsterdam: North-Holland.
• Łukasiewicz, Jan and Alfred Tarski. 1930. “Untersuchungen über den Aussagenkalkül,” Comptes Rendus des séances de la Société des Sciences et de la Lettres de Varsovie 32: 30-50. Published in English as “Investigations into the Sentential Calculus,” in Tarski 1956.
• Mally, Ernst. 1926. Grundgesetze des Sollens: Elemente der Logik des Willens. Graz: Leuschner und Lubensky.
• McCune, William, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist and Larry Wos. 2002. “Short Single Axioms for Boolean Algebra,” Journal of Automated Reasoning 29: 1-16.
• Mendelson, Elliot. 1997. Introduction to Mathematical Logic. 4th ed. London: Chapman and Hall.
• Meredith, C. A. 1953. “Single Axioms for the Systems (C, N), (C, O) and (A, N) of the Two-valued Propositional Calculus,” Journal of Computing Systems 3: 155-62.
• Müller, Eugen, ed. 1909. Abriss der Algebra der Logik, by E. Schröder. Leipzig: Teubner.
• Nicod, Jean. 1917. “A Reduction in the Number of the Primitive Propositions of Logic,” Proceedings of the Cambridge Philosophical Society 19: 32-41.
• Peirce, C. S. 1885. “On the Algebra of Logic,” American Journal of Mathematics 7: 180-202.
• Post, Emil. 1921. “Introduction to a General Theory of Propositions,” American Journal of Mathematics 43: 163-185.
• Priest, Graham, Richard Routley and Jean Norman, eds. 1990. Paraconsistent Logic. Munich: Verlag.
• Prior, Arthur. 1990. Formal Logic. 2nd. ed. Oxford: Oxford University Press.
• Read, Stephen, 1988. Relevant Logic. New York: Blackwell.
• Rescher, Nicholas. 1966. The Logic of Commands. London: Routledge and Kegan Paul.
• Rescher, Nicholas. 1969. Many-Valued Logic. New York: McGraw Hill.
• Rosser, J. B. 1953. Logic for Mathematicians. New York: McGraw Hill.
• Russell, Bertrand. 1906. “The Theory of Implication,” American Journal of Mathematics 28: 159-202.
• Schlesinger, G. N. 1985. The Range of Epistemic Logic. Aberdeen: Aberdeen University Press.
• Sheffer, H. M. 1913. “A Set of Five Postulates for Boolean Algebras with Application to Logical Constants,” Transactions of the American Mathematical Society 14: 481-88.
• Smullyan, Raymond. 1961. Theory of Formal Systems. Princeton: Princeton University Press.
• Tarski, Alfred. 1956. Logic, Semantics and Meta-Mathematics. Oxford: Oxford University Press.
• Urquhart, Alasdair. 1986. “Many-valued Logic,” In Handbook of Philosophical Logic, vol. 3, edited by D. Gabbay and F. Guenthner. Dordrecht: Reidel.
• Venn, John. 1881. Symbolic Logic. London: Macmillan.
• Whitehead, Alfred North and Bertrand Russell. 1910-1913. Principia Mathematica. 3 vols. Cambridge: Cambridge University Press.
• Wittgenstein, Ludwig. 1922. Tractatus Logico-Philosophicus. London: Routledge and Kegan Paul.

Author Information

Kevin C. Klement
Email: klement@philos.umass.edu
University of Massachusetts, Amherst
U. S. A.

Logical Consequence

Logical consequence is arguably the central concept of logic. The primary aim of logic is to tell us what follows logically from what. In order to simplify matters we take the logical consequence relation to hold for sentences rather than for abstract propositions, facts, state of affairs, etc. Correspondingly, logical consequence is a relation between a given class of sentences and the sentences that logically follow. One sentence is said to be a logical consequence of a set of sentences, if and only if, in virtue of logic alone, it is impossible for the sentences in the set to be all true without the other sentence being true as well. If sentence X is a logical consequence of a set of sentences K, then we may say that K implies or entails X, or that one may correctly infer the truth of X from the truth of the sentences in K. For example, Kelly is not at work is a logical consequence of Kelly is not both at home and at work and Kelly is at home. However, the sentence Kelly is not a football fan does not follow from All West High School students are football fans and Kelly is not a West High School student. The central question to be investigated here is: What conditions must be met in order for a sentence to be a logical consequence of others?

One popular answer derives from the work of Alfred Tarski, one of the preeminent logicians of the twentieth century, in his famous 1936 paper, “The Concept of Logical Consequence.” Here Tarski uses his observations of the salient features of what he calls the common concept of logical consequence to guide his theoretical development of it. Accordingly, we begin by examining the common concept focusing on Tarski’s observations of the criteria by which we intuitively judge what follows from what and which Tarski thinks must be reflected in any theory of logical consequence. Then two theoretical definitions of logical consequence are introduced: the model theoretic and the deductive theoretic definitions. They represent two major approaches to making the common concept of logical consequence more precise. The article concludes by highlighting considerations relevant to evaluating model theoretic and deductive theoretic characterizations of logical consequence.

Table of Contents

1. Introduction
2. The Concept of Logical Consequence: Model-Theoretic and Deductive-Theoretic Conceptions of Logic
   1. Tarski’s Characterization of the Common Concept of Logical Consequence
      1. The Logical Consequence Relation Has a Modal Element
      2. The Logical Consequence Relation is Formal
      3. The Logical Consequence Relation is A Priori
   2. Logical and Non-Logical Terminology
      1. The Nature of Logical Constants Explained in Terms of Their Semantic Properties
      2. The Nature of Logical Constants Explained in Terms of Their Inferential Properties
3. Model-Theoretic and Deductive-Theoretic Conceptions of Logic
4. Conclusion
5. References and Further Reading

1. Introduction

For a given language, a sentence is said to be a logical consequence of a set of sentences, if and only if, in virtue of logic alone, the sentence must be true if every sentence in the set were to be true. This corresponds to the ordinary notion of a sentence “logically following” from others. Logicians have attempted to make the ordinary concept more precise relative to a given language L by sketching a deductive system for L, or by formalizing the intended semantics for L. Any adequate precise characterization of logical consequence must reflect its salient features such as those highlighted by Alfred Tarski: (1) that the logical consequence relation is formal, that is, depends on the forms of the sentences involved, (2) that the relation is a priori, that is, it is possible to determine whether or not it holds without appeal to sense-experience, and (3) that the relation has a modal element.

For more comprehensive presentations of the two definitions of logical consequence, as well as further critical discussion, see the entries Logical Consequence, Model-Theoretic Conceptions and Logical Consequence, Deductive-Theoretic Conceptions.

2. The Concept of Logical Consequence

a. Tarski’s Characterization of the Common Concept of Logical Consequence

Tarski begins his article, “On the Concept of Logical Consequence,” by noting a challenge confronting the project of making precise the common concept of logical consequence.

The concept of logical consequence is one of those whose introduction into a field of strict formal investigation was not a matter of arbitrary decision on the part of this or that investigator; in defining this concept efforts were made to adhere to the common usage of the language of everyday life. But these efforts have been confronted with the difficulties which usually present themselves in such cases. With respect to the clarity of its content the common concept of consequence is in no way superior to other concepts of everyday language. Its extension is not sharply bounded and its usage fluctuates. Any attempt to bring into harmony all possible vague, sometimes contradictory, tendencies which are connected with the use of this concept, is certainly doomed to failure. We must reconcile ourselves from the start to the fact that every precise definition of this concept will show arbitrary features to a greater or less degree. (Tarski 1936, p. 409)

Not every feature of the technical account will be reflected in the ordinary concept, and we should not expect any clarification of the concept to reflect each and every deployment of it in everyday language and life. Nevertheless, despite its vagueness, Tarski believes that there are identifiable, essential features of the common concept of logical consequence.

…consider any class K of sentences and a sentence X which follows from this class. From an intuitive standpoint, it can never happen that both the class K consists of only true sentences and the sentence X is false. Moreover, since we are concerned here with the concept of logical, that is, formal consequence, and thus with a relation which is to be uniquely determined by the form of the sentences between which it holds, this relation cannot be influenced in any way by empirical knowledge, and in particular by knowledge of the objects to which the sentence X or the sentences of class K refer. The consequence relation cannot be affected by replacing designations of the objects referred to in these sentences by the designations of any other objects. (Tarski 1936, pp. 414-415)

According to Tarski, the logical consequence relation as it is employed by typical reasoners is (1) necessary, (2) formal, and (3) not influenced by empirical knowledge. I now elaborate on (1)-(3) in order to shape two preliminary characterizations of logical consequence.

i. The Logical Consequence Relation Has a Modal Element

Tarski countenances an implicit modal notion in the common concept of logical consequence. If X is a logical consequence of K, then not only is it the case that not all of the elements of K are true and X is false, but also this is necessarily the case. That is, X follows from K only if it is not possible for all of the sentences in K to be true with X false. For example, the supposition that All West High School students are football fans and that Kelly is not a West High School student does not rule out the possibility that Kelly is a football fan. Hence, the sentences All West High School students are football fans and Kelly is not a West High School student do not entail Kelly is not a football fan, even if she, in fact, isn’t a football fan. Also, Most of Kelly’s male classmates are football fans does not entail Most of Kelly’s classmates are football fans. What if the majority of Kelly’s class is composed of females who are not fond of football?

We said above that Kelly is not both at home and at work and Kelly is at home jointly imply Kelly is not at work. Note that it doesn’t seem possible for the first two sentences to be true and Kelly is not at work false. But it is hard to see what this comes to without further clarification of the relevant notion of possibility. For example, consider the following pairs of sentences.

Kelly kissed her sister at 2:00pm. 2:00pm is not a time during which Kelly and her sister were 100 miles apart.	Kelly is a female. Kelly is not the US President.
There is a chimp in Paige’s house. There is a primate in Paige’s house.	Ten is a prime number. Ten is greater than nine.

For each pair of sentences, there is a sense in which it is not possible for the first to be true and the second false. At the very least an account of logical consequence must distinguish logical possibility from other types of possibility. Should truths about physical laws, US political history, zoology, and mathematics constrain what we take to be possible in determining whether or not the first sentence of each pair could logically be true with the second sentence false? If not, then this seems to mystify logical possibility (e.g., how could ten be a prime number?). To paraphrase questions asked by G.E. Moore (1959, pp. 231-238), given that I know that George W. Bush is US President and that he is not a female named Kelly, isn’t it inconsistent for me to grant the logical possibility of the truth of Kelly is a female and the falsity of Kelly is not the US President? Or should I ignore my present state of knowledge in considering what is logically possible? Tarski does not derive a clear notion of logical possibility from the common concept of logical consequence. Perhaps there is none to be had, and we should seek the help of a proper theoretical development in clarifying the notion of logical possibility. Towards this end, let’s turn to the other features of logical consequence highlighted by Tarski, starting with the formality criterion of logical consequence.

ii. The Logical Consequence Relation is Formal

Tarski observes that logical consequence is a formal consequence relation. And he tells us that a formal consequence relation is a consequence relation that is uniquely determined by the form of the sentences between which it holds. Consider the following pair of sentences

(1) Some children are both lawyers and peacemakers.
(2) Some children are peacemakers

Intuitively, (2) is a logical consequence of (1). It appears that this fact does not turn on the subject matter of the sentences. Replace ‘children’, ‘lawyers’, and ‘peacemakers’ in (1) and (2) with the variables S, M, and P to get the following.

(1′) Some S are both M and P
(2′) Some S are P

(1′) and (2′) are forms of (1) and (2), respectively. Note that there is no interpretation of S, M, and P according to which the sentence that results from (1′) is true and the resulting instance of (2′) is false. Hence, (2) is a formal consequence of (1) and on each interpretation of S, M, and P the resulting (2′) is a formal consequence of the sentence that results from (1′) (e.g., Some clowns are sad is a formal consequence of Some clowns are both lonely and sad). Tarski’s observation is that for any sentence X and set K of sentences, X is a logical consequence of K only if X is a formal consequence of K. The formality criterion of logical consequence can work in explaining why one sentence doesn’t entail another in cases where it seems impossible for the first to be true and the second false. For example, (3) is false and (4) is true.

(3) Ten is a prime number
(4) Ten is greater than nine

Does (4) follow from (3)? One might think that (4) does not follow from (3) because being a prime number does not necessitate being greater than nine. However, this does not require one to think that ten could be a prime number and less than or equal to nine, which is probably a good thing since it is hard to see how this is possible. Rather, we take

(3′) a is a P
(4′) a is R than b

to be the forms of (5) and (6) and note that there are interpretations of ‘a’, ‘b’, ‘P’, and ‘R’ according to which the first is true and the second false (e.g. let ‘a’ and ‘b’ name the numbers two and ten, respectively, and let ‘P’ mean prime number, and ‘R’ greater). Note that the claim here is not that formality is sufficient for a consequence relation to qualify as logical but only that it is a necessary condition. I now elaborate on this last point by saying a little more about forms of sentences (that is, sentential forms) and formal consequence.

Distinguishing between a term of a sentence replaced with a variable and one held constant determines a form of the sentence. In Some children are both lawyers and peacemakers we may replace ‘Some’ with a variable and treat all the other terms as constant. Then

(1”) D children are both lawyers and peacemakers

is a form of (1), and each sentence generated by assigning a meaning to D shares this form with (1). For example, the following three sentences are instances of (1”), produced by interpreting D as ‘No’, ‘Many’, and ‘Few’.

No children are both lawyers and peacemakers
Many children are both lawyers and peacemakers
Few children are both lawyers and peacemakers

Whether X is a formal consequence of K then turns on a prior selection of terms as constant and others replaced with variables. Relative to such a determination, X is a formal consequence of K if and only if (iff) there is no interpretation of the variables according to which each of the K are true and X is false. So, taking all the terms, except for ‘Some’, in (1) Some children are both philosophers and peacemakers and in (2) Some children are peacemakers as constants makes the following forms of (1) and (2).

(1”) D children are both lawyers and peacemakers
(2”) D children are peacemakers

Relative to this selection, (2) is not a formal consequence of (1) because replacing ‘D’ with ‘No’ yields a true instance of (1”) and a false instance of (2”).

Consider the following pair.

(5) Kelly is female
(6) Kelly is not US President

(6) is a formal consequence of (5) relative to replacing ‘Kelly’ with a variable. Given current U.S. political history, there is no individual whose name yields a true (5) and a false (6) when it replaces ‘Kelly’. This is not, however, sufficient reason for seeing (6) as a logical consequence of (5). There are two ways of thinking about why, a metaphysical consideration and an epistemological one. First the metaphysical consideration. It seems possible for (5) to be true and (6) false. The course of U.S. political history could have turned out differently. One might think that the current US President could–logically–have been a female named, say, ‘Sally’. Using ‘Sally’ as a replacement for ‘Kelly’ would yield in that situation a true (5) and a false (6). Also, it seems possible that in the future there will be a female US President. In order for a formal consequence relation from K to X to qualify as logical it has to be the case that it is necessary that there is no interpretation of the variables in K and X according to which the K-sentences are true and X is false.

The epistemological consideration is that one might think that knowledge that X follows logically from K should not essentially depend on being justified by experience of extra-linguistic states of affairs. Clearly, the determination that (6) follows formally from (5) essentially turns on empirical knowledge, specifically knowledge about the current political situation in the US. This leads to the final highlight of Tarski’s rendition of the intuitive concept of logical consequence: that logical consequence cannot be influenced by empirical knowledge.

iii. The Logical Consequence Relation is A Priori

Tarski says that by virtue of being formal, knowledge that X follows logically from K cannot be affected by knowledge of the objects that X and the sentences of K are about. Hence, our knowledge that X is a logical consequence of K cannot be influenced by empirical knowledge. However, as noted above, formality by itself does not insure that the extension of a consequence relation is not influenced by empirical knowledge. So, let’s view this alleged feature of logical consequence as independent of formality. We characterize empirical knowledge in two steps as follows. First, a priori knowledge is knowledge “whose truth, given an understanding of the terms involved, is ascertainable by a procedure which makes no reference to experience” (Hamlyn 1967, p. 141). Empirical, or a posteriori, knowledge is knowledge that is not a priori, that is, knowledge whose validation necessitates a procedure that does make reference to experience. We can safely read Tarski as saying that a consequence relation is logical only if knowledge that something falls in its extension is a priori, that is, only if the relation is a priori. Knowledge of physical laws, a determinant in people’s observed sizes, is not a priori and such knowledge is required to know that there is no interpretation of k, h, and t according to which (7) is true and (8) false.

(7) k kissed h at time t
(8) t is not a time during which k and h were 100 miles apart

So (8) cannot be a logical consequence of (7). However, my knowledge that Kelly is not Paige’s only friend follows from Kelly is taller than Paige’s only friend is a priori since I know a priori that nobody is taller than herself.

Let’s summarize and tie things together. We began by asking, for a given language L, what conditions must be met in order for a sentence X of L to be a logical consequence of a class K of L-sentences? Tarski thinks that an adequate response must reflect the common concept of logical consequence, that is, the concept as it is ordinarily employed. By the lights of this concept, an adequate account of logical consequence must reflect the formality and necessity of logical consequence, and must also reflect the fact that knowledge of what follows logically from what is a priori. Tying the criteria together, in order to fix what follows logically from what in a given language L, we must select a class of constants that determines a formal consequence relation that is both necessary and known, if at all, a priori. Such constants are called logical constants, and we say that the logical form of a sentence is a function of the logical constants that occur in the sentence and the pattern of the remaining expressions. As was illustrated above, the notion of formality does not presuppose a criterion of logical constancy. A consequence relation based on any division between constants and terms replaced with variables will automatically be formal with respect to the latter.

b. Logical and Non-Logical Terminology

Tarski’s basic move from his rendition of the common concept of logical consequence is to distinguish between logical terms and non-logical terms and then say that X is a logical consequence of K only if there is no possible interpretation of the non-logical terms of the language L that makes all of the sentences in K true and X false. The choice of the right terms as logical will reflect the modal element in the concept of logical consequence, that is, will insure that there is no ‘possible’ interpretation of the variable, non-logical terms of the language L that makes all of the K true and X false, and will insure that this is known a priori. Of course, we have yet to spell out the modal notion in the concept of logical consequence. Tarski pretty much left this underdeveloped in his (1936). Lacking such an explanation hampers our ability to clarify the rationale for a selection of terms to serve as the logical ones.

Traditionally, logicians have regarded sentential connectives such as and, not, or, if…then, the quantifiers all and some, and the identity predicate ‘=’ as logical terms. Remarking on the boundary between logical and non-terms, Tarski (1936, p. 419) writes the following.

Underlying this characterization of logical consequence is the division of all terms of the language discussed into logical and extra-logical. This division is not quite arbitrary. If, for example, we were to include among the extra-logical signs the implication sign, or the universal quantifier, then our definition of the concept of consequence would lead to results which obviously contradict ordinary usage. On the other hand, no objective grounds are known to me which permit us to draw a sharp boundary between the two groups of terms. It seems to be possible to include among logical terms some which are usually regarded by logicians as extra-logical without running into consequences which stands in sharp contrast to ordinary usage.

Tarski seems right to think that the logical consequence relation turns on the work that the logical terminology does in the relevant sentences. It seems odd to say that Kelly is happy does not logically follow from All are happy because the second is true and the first false when All is replaced with Few. However, by Tarski’s version of the ordinary concept of logical consequence there is no reason not to treat say taller than as a logical term along with not and, therefore, no reason not to take Kelly is not taller than Paige as following logically from Paige is taller than Kelly. Also, it seems plausible to say that I know a priori that there is no possible interpretation of Kelly and is mortal according to which it is necessary that Kelly is mortal is true and Kelly is mortal is false. This makes Kelly is mortal a logical consequence of it is necessary that Kelly is mortal. Given that taller than and it is necessary that, along with other terms, were not generally regarded as logical terms by logicians of Tarski’s day, the fact that they seem to be logical terms by the common concept of logical consequence, as observed by Tarski, highlights the question of what it takes to be a logical term. Tarski says that future research will either justify the traditional boundary between the logical and the non-logical or conclude that there is no such boundary and the concept of logical consequence is a relative concept whose extension is always relative to some selection of terms as logical (p. 420). For further discussion of Tarski’s views on logical terminology and contemporary views see Logical Consequence, Model-Theoretic Conceptions: Section 5.3.

How, exactly, does the terminology usually regarded by logicians as logical work in making it the case that one sentence follows from others? In the next two sections two distinct approaches to understanding the nature of logical terms are sketched. Each approach leads to a unique way of characterizing logical consequence and thus yields a unique response to the above question.

i. The Nature of Logical Constants Explained in Terms of Their Semantic Properties

Consider the following metaphor, borrowed from Bencivenga (1999).

The locked room metaphor

Suppose that you are locked in a dark windowless room and you know everything about your language but nothing about the world outside. A sentence X and a class K of sentences are presented to you. If you can determine that X is true if all the sentences in K are, X is a logical consequence of K.

Ignorant of US politics, I couldn’t determine the truth of Kelly is not US President solely on the basis of Kelly is a female. However, behind such a veil of ignorance I would be able to tell that Kelly is not US President is true if Kelly is female and Kelly is not US President is true. How? Short answer: based on my linguistic competence; longer answer: based on my understanding of the semantic contribution of and to the determination of the truth conditions of a sentence of the form P and Q. For any sentences P and Q, I know that P and Q is true just in case P is true and Q is true. So, I know, a priori, if P and Q is true, then Q is true. As noted by one philosopher, “This really is remarkable since, after all, it’s what they mean, together with the facts about the non-linguistic world, that decide whether P or Q are true” (Fodor 2000, p.12).

Taking not and and to be the only logical constants in (9) Kelly is not both at home and at work, (10) Kelly is at home, and (11) Kelly is not at work, we formalize the sentences as follows, letting k mean Kelly, H mean is at home, and W mean is at work.

(9′) not-(Hk and Wk)
(10′) Hk
(11′) not-Wk

There is no interpretation of k, H, and W according to which (9′) and (10′) are true and (11′) is false. The reason why turns on the semantic properties of and and not, which are knowable a priori. Suppose (9′) and (10′) are true on some interpretation of the variable terms. Then the meaning of not in (9′) makes it the case that Hk and Wk is false, which, by the meaning of and requires that Hk is false or Wk is false. Given (10′), it must be that Wk is false, that is, not-Wk is true. So, there can’t be an interpretation of the variable terms according to which (9′) and (10′) are true and (11′) is false, and, as the above reasoning illustrates, this is due exclusively to the semantic properties of not and and. So the reason that it is impossible that an interpretation of k, H, and W make (9′) and (10′) true and (11′) false is that the supposition otherwise is inconsistent with the semantic functioning of not and and. Compare: the supposition that there is an interpretation of k according to which k is a female is true and k is not US President is false does not seem to violate the semantic properties of the constant terms. If we identify the meanings of the predicates with their extensions in all possible worlds, then the supposition that there is a female U.S. President does not violate the meanings of female and US President for surely it is possible that there be a female US President. But, supposing that (9′) and (10′) could be true with (11′) false on some interpretation of k, H, and W, violates the semantic properties of either and or not.

In sum, our first-step characterization of logical consequence is the following. For a given language L,

X is a logical consequence of K if and only if there is no possible interpretation of the non-logical terminology of L according to which all the sentence in K are true and X is false.

A possible interpretation of the non-logical terminology of the language L according to which sentences are true or false is a reading of the non-logical terms according to which the sentences receive a truth-value (that is, is either true or false) in a situation that is not ruled out by the semantic properties of the logical constants. The philosophical locus of the technical development of ‘possible interpretation’ in terms of models is Tarski (1936). A model for a language L is the theoretical development of a possible interpretation of non-logical terminology of L according to which the sentences of L receive a truth-value. Models have become standard tools for characterizing the logical consequence relation, and the characterization of logical consequence in terms of models is called the Tarskian or model-theoretic characterization of logical consequence. We say that X is a model-theoretic consequence of K if and only if all models of K are models of X. This relation may be represented as K ⊨ X. If model-theoretic consequence is adequate as a representation of logical consequence, then it must reflect the salient features of the common concept, which, according to Tarski means that it must be necessary, formal and a priori.

For further discussion of this conception of logical consequence, see the article, Logical Consequence, Model-Theoretic Conceptions.

ii. The Nature of Logical Constants Explained in Terms of Their Inferential Properties

We now turn to a second approach to understanding logical constants. Instead of understanding the nature of logical constants in terms of their semantic properties as is done on the model-theoretic approach, on the second approach we appeal to their inferential properties conceived of in terms of principles of inference, that is, principles justifying steps in deductions. We begin with a remark made by Aristotle. In his study of logical consequence, Aristotle comments that

A syllogism is discourse in which, certain things being stated, something other than what is stated follows of necessity from their being so. I mean by the last phrase that they produce the consequence, and by this, that no further term is required from without in order to make the consequence necessary. (Prior Analytics, p. 24b)

Adapting this to our X and K, we may say that X is a logical consequence of K when the sentences of K are sufficient to produce X. How are we to think of a sentence being produced by others? One way of developing this is to appeal to a notion of an actual or possible deduction. X is a deductive consequence of K if and only if there is a deduction of X from K. In such a case, we say that X may be correctly inferred from K or that it would be correct to conclude X from K. A deduction is associated with a pair ; the set K of sentences is the basis of the deduction, and X is the conclusion. A deduction from K to X is a finite sequence S of sentences ending with X such that each sentence in S (that is, each intermediate conclusion) is derived from a sentence (or more) in K or from previous sentences in S in accordance with a correct principle of inference.

For example, intuitively, the following inference seems correct.

	Kelly is not both at home and at work
	Kelly is at home
(therefore)	Kelly is not at work

The set K of sentences above the line is the basis of the inference and the sentence X below is the conclusion. We represent their logical forms, again, as follows.

	(9′) not-(Hk and Wk)
	(10′) Hk
(therefore)	(11′) not-Wk

Consider the following deduction of (11′) from (10′) and (9′).

Deduction: Assume that (12′) Wk. Then from (10′) and (12′) we may deduce that (13′) Hk and Wk. (13′) contradicts (9′) and so (12′), our initial assumption, must be false. We have deduced not-Wk from not-(Hk and Wk) and Hk.

Since the deduction of not-Wk from not-(Hk and Wk) and Hk did not depend on the interpretation of k, W, and H, the deductive relation is formal. Furthermore, my knowledge of this is a priori because my knowledge of the underlying principles of inference in the above deduction is not empirical. For example, letting P and Q be any sentences, we know a priori that P and Q may be inferred from the set K={P, Q} of basis sentences. This principle grounds the move from (10′) and (12′) to (13′). Also, the deduction appeals to the principle that if we deduce a contradiction from an assumption, then we may infer that the assumption is false. The correctness of this principle seems to be an a priori matter. Let’s look at another example of a deduction.

	(1) Some children are both lawyers and peacemakers
(therefore)	(2) Some children are peacemakers

The logical forms are, again, the following.

	(1′) Some S are both M and P
(therefore)	(2′) Some S are P

Again, intuitively, (2′) is deducible from (1′).

Deduction: The basis tells us that at least one S–let’s call this S ‘a‘–is both an M and a P. Clearly, a is a P may be deduced from a is both an M and a P. Since we’ve assumed that a is an S, what we derive with respect to a we derive with respect to some S. So our derivation of a is a P is a derivation of Some S is a P, which is our desired conclusion.

Since the deduction is formal, we have shown not merely that (2) can be correctly inferred from (1), but we have shown that for any interpretation of S, M, and P it is correct to infer (2′) from (1′).

Typically, deductions leave out steps (perhaps because they are too obvious), and they usually do not justify each and every step made in moving towards the conclusion (again, obviousness begets brevity). The notion of a deduction is made precise by describing a mechanism for constructing deductions that are both transparent and rigorous (each step is explicitly justified and no steps are omitted). This mechanism is a deductive system (also known as a formal system or as a formal proof calculus). A deductive system D is a collection of rules that govern which sequences of sentences, associated with a given , are allowed and which are not. Such a sequence is called a proof in D (or, equivalently, a deduction in D) of X from K. The rules must be such that whether or not a given sequence associated with qualifies as a proof in D of X from K is decidable purely by inspection and calculation. That is, the rules provide a purely mechanical procedure for deciding whether a given object is a proof in D of X from K.

We say that a deductive system D is correct when for any K and X, proofs in D of X from K correspond to intuitively valid deductions. For example, intuitively, there are no correct principles of inference according to which it is correct to conclude

Some animals are both mammals and reptiles

on the basis of the following two sentences.

Some animals are mammals
Some animals are reptiles

Hence, a proof in a deductive system of the former sentence from the latter two is evidence that the deductive system is incorrect. The point here is that a proof in D may fail to represent a deduction if D is incorrect.

A rich variety of deductive systems have been developed for registering deductions. Each system has its advantages and disadvantages, which are assessed in the context of the more specific tasks the deductive system is designed to accomplish. Historically, the general purpose of the construction of deductive systems was to reduce reasoning to precise mechanical rules (Hodges 1983, p. 26). Some view a deductive system defined for a language L as a mathematical model of actual or possible chains of correct reasoning in L. Sundholm (1983) offers a thorough survey of three main types of deductive systems. For a shorter, excellent introduction to the concept of a deductive system see Henkin (1967). A deductive system is developed in detail in the accompanying article, Logical Consequence, Deductive-Theoretic Conceptions.

If there is a proof of X from K in deductive system D, then we may say that X is a deductive consequence in D of K, which is sometimes expressed as K ⊢_D X. Relative to a correct deductive system D, we characterize logical consequence in terms of deductive consequence as follows.

X is a logical consequence of K if and only if X is a deductive consequence in D of K, that is, there is an actual or possible proof in D of X from K.

This is called the deductive-theoretic (or proof-theoretic) characterization of logical consequence.

3. Model-Theoretic and Deductive-Theoretic Conceptions of Logic

We began with Tarski’s observations of the common or ordinary concept of logical consequence that we employ in daily life. According to Tarski, if X is a logical consequence of a set of sentences, K, then, in virtue of the logical forms of the sentences involved, if all of the members of K are true, then X must be true, and furthermore, we know this a priori. The formality criterion makes the logical constants the essential determinant of the logical consequence relation. The logical consequence relation is fixed exclusively in terms of the nature of the logical terminology. We have highlighted two different approaches to the nature of a logical constant: (1) in terms of its semantic contribution to sentences in which it occurs and (2) in terms of its inferential properties. The two approaches yield distinct conceptions of the notion of necessity inherent in the common concept of logical consequence, and lead to the following characterizations of logical consequence.

(1) X is a logical consequence of K if and only if there is no possible interpretation of the non-logical terminology of the language according to which all the sentences in K are true and X is false.

(2) X is a logical consequence of K if and only if X is deducible from K.

We make the notions of possible interpretation in (1) and deducibility in (2) precise by appealing to the technical notions of model and deductive system. This leads to the following theoretical characterizations of logical consequence.

(1) The model-theoretic characterization of logical consequence: X is a logical consequence of K iff all models of K are models of X.

(2) The deductive- theoretic characterization of logical consequence: X is a logical consequence of K iff there is a deduction in a correct deductive system of X from K.

Following Shapiro (1991, p. 3) define a logic to be a language L plus either a model-theoretic or a deductive-theoretic account of logical consequence. A language with both characterizations is a full logic just in case both characterizations coincide. A soundness proof establishes K ⊢_D X only if K ⊨ X, and a completeness proof establishes K ⊢_D X if K ⊨ X. These proofs together establish that the two characterizations coincide, and in such a case the deductive system D is said to be complete and sound with respect to the model-theoretic consequence relation defined for the relevant language L.

We said that the primary aim of logic is to tell us what follows logically from what. These two characterizations of logical consequence lead to two different orientations or conceptions of logic (see Tharp 1975, p. 5).

Model-theoretic approach: Logic is a theory of possible interpretations. For a given language the class of situations that can–logically–be described by that language.

Deductive-theoretic approach: Logic is a theory of formal deductive inference.

The article now concludes by highlighting three considerations relevant to evaluating a particular deployment of the model-theoretic or deductive-theoretic definition in defining logical consequence. These considerations emerge from the above development of the two theoretic definitions from the common concept of logical consequence.

4. Conclusion

The two theoretical characterizations of logical consequence do not provide the means for drawing a boundary in a language L between logical and non-logical terms. Indeed, their use presupposes that a list of logical terms is in hand. Hence, in evaluating a model-theoretic or deductive-theoretic definition of logical consequence for a language L the issue arises whether or not the boundary in L between logical and non-logical terms has been correctly drawn. This requires a response to a central question in the philosophy of logic: what qualifies as a logical constant? Tarski gives a well-reasoned response in his (1986). (For more recent discussion see McCarthy 1981 and 1998, Hanson 1997, and Warbrod 1999.)

A second thing to consider in evaluating a theoretical account of logical consequence is whether or not its characterization of the logical terminology is accurate. For example, model-theoretic and deductive accounts of logical consequence are inadequate unless they reflect the semantic and inferential properties of the logical terms, respectively. So a model-theoretic account is inadequate unless it gets right the semantic contributions of the logical terms to the truth conditions of the sentences formed using them. For a particular deductive system D, the question arises whether or not D’s rules of inference reflect the inferential properties of the logical terms. (For further discussion of the semantic and inferential properties of logical terms see Haack 1978 and 1996, Read 1995, and Quine 1986.)

A third consideration in assessing the success of a theoretical definition of logical consequence is whether or not the definition, relative to a selection of terms as logical, reflects the salient features of the common concept of logical consequence. There are criticisms of the theoretical definitions that claim that they are incapable of reflecting the common concept of logical consequence. Typically, such criticisms are used to question the status of the model-theoretic and deductive-theoretic approaches to logic.

For example, there are critics who question the model-theoretic approach to logic by arguing that any model-theoretic account lacks the conceptual resources to reflect the notion of necessity inherent in the common concept of logical consequence because such an account does not rule out the possibility of there being logically possible situations in which sentences in K are true and X is false even though every model of K is a model of X. Kneale (1961) is an early critic, Etchemendy (1988, 1999) offers a sustained and multi-faceted attack. Also, it is argued that the model-theoretic approach to logic makes knowledge of what follows from what depend on knowledge of the existence of models, which is knowledge of worldly matters of fact. But logical knowledge should not depend on knowledge about the extra-linguistic world (recall the locked room metaphor in 2.2.1). This standard logical positivist line has been recently challenged by those who see logic penetrated and permeated by metaphysics (e.g., Putnam 1971, Almog 1989, Sher 1991, Williamson 1999).

The status of the deductive-theoretic approach to logic is not clear for, as Tarski argues in his (1936), deductive-theoretic accounts are unable to reflect the fact that, according to the common concept, logical consequence is not compact. Relative to any deductive system D, the ⊢_D-consequence relation is compact if and only if for any sentence X and set K of sentences, if K ⊢_D X, then K’ ⊢_D X, where K’ is a finite subset of sentences from K. But there are intuitively correct principles of inference according to which one may infer a sentence X from a set K of sentences, even though it is incorrect to infer X from any finite subset of K. This suggests that the intuitive notion of deducibility is not completely captured by any compact consequence relation. We need to weaken

X is a logical consequence of K if and only if there is a proof in a correct deductive system of X from K,

given above, to

X is a logical consequence of K if there is a proof in a correct deductive system of X from K.

In sum, the issue of the nature of logical consequence, which intersects with other areas of philosophy, is still a matter of debate. Tarski’s analysis of the concept is not universally accepted; philosophers and logicians differ over what the features of the common concept are. For example, some offer accounts of the logical consequence relation according to which it is not a priori (e.g., see Koslow 1999, Sher 1991 and see Hanson 1997 for criticism of Sher) or deny that it even need be strongly necessary (Smiley 1995, 2000, section 6). The entry Logical Consequence, Model-Theoretic Conceptions gives a model-theoretic definition of logical consequence. For a detailed development of a deductive system see the entry Logical Consequence, Deductive-Theoretic Conceptions. The critical discussion in both articles deepens and extends points made in the conclusion of this article.

5. References and Further Reading

• Almog, J. (1989): “Logic and the World”, pp. 43-65 in Themes From Kaplan, ed. J. Almog, J. Perry, J., and H. Wettstein. New York: Oxford UP.
• Aristotle. (1941): Basic Works, ed. R. McKeon. New York: Random House.
• Bencivenga, E. (1999): “What is Logic About?”, pp. 5-19 in Varzi (1999).
• Etchemendy, J. (1983): “The Doctrine of Logic as Form”, Linguistics and Philosophy 6, pp. 319-334.
• Etchemendy, J. (1988): “Tarski on truth and logical consequence”, Journal of Symbolic Logic 53, pp. 51-79.
• Etchemendy, J. (1999): The Concept of Logical Consequence. Stanford: CSLI Publications.
• Fodor, J. (2000): The Mind Doesn’t Work That Way. Cambridge: The MIT Press.
• Gabbay, D. and F. Guenthner, eds. (1983): Handbook of Philosophical Logic, Vol 1. Dordrecht: D. Reidel Publishing Company.
• Haack, S. (1978): Philosophy of Logics . Cambridge: Cambridge University Press.
• Haack, S. (1996): Deviant Logic, Fuzzy Logic. Chicago: The University of Chicago Press.
• Hodges, W. (1983): “Elementary Predicate Logic”, in Gabbay, D. and F. Guenthner (1983).
• Hamlyn, D.W. (1967): “A Priori and A Posteriori”, pp.105-109 in The Encyclopedia of Philosophy, Vol. 1, ed. P. Edwards. New York: Macmillan & The Free Press.
• Hanson, W. (1997): “The Concept of Logical Consequence”, The Philosophical Review 106, pp. 365-409.
• Henkin, L. (1967): “Formal Systems and Models of Formal Systems”, pp. 61-74 in The Encyclopedia of Philosophy, Vol. 8, ed. P. Edwards. New York: Macmillan & The Free Press.
• Kneale, W. (1961): “Universality and Necessity”, British Journal for the Philosophy of Science 12, pp. 89-102.
• Koslow, A. (1999): “The Implicational Nature of Logic: A Structuralist Account”, pp. 111-155 in Varzi (1999).
• McCarthy, T. (1981): “The Idea of a Logical Constant”, Journal of Philosophy 78, pp. 499-523.
• McCarthy, T. (1998): “Logical Constants”, pp. 599-603 in Routledge Encyclopedia of Philosophy, Vol. 5, ed. E. Craig. London: Routledge.
• McGee, V. (1999): “Two Problems with Tarski’s Theory of Consequence”, Proceedings of the Aristotelean Society 92, pp. 273-292.
• Moore, G.E., (1959): “Certainty”, pp. 227-251 in Philosophical Papers. London: George Allen & Unwin.
• Priest. G. (1995): “Etchemendy and Logical Consequence”, Canadian Journal of Philosophy 25, pp. 283-292.
• Putnam, H. (1971): Philosophy of Logic. New York: Harper & Row.
• Quine, W.V. (1986): Philosophy of Logic, 2nd ed.. Cambridge: Harvard UP.
• Read, S. (1995): Thinking About Logic. Oxford: Oxford UP.
• Shapiro, S. (1991): Foundations without Foundationalism: A Case For Second-Order Logic. Oxford: Clarendon Press.
• Shapiro, S. (1993): ” Modality and Ontology”, Mind 102, pp. 455-481.
• Shapiro, S. (1998): “Logical Consequence: Models and Modality”, pp. 131-156 in The Philosophy of Mathematics Today, ed. Matthias Schirn. Oxford, Clarendon Press.
• Shapiro, S. (2000): Thinking About Mathematics , Oxford: Oxford University Press.
• Sher, G. (1989): “A Conception of Tarskian Logic”, Pacific Philosophical Quarterly 70, pp. 341-368.
• Sher, G. (1991): The Bounds of Logic: A Generalized Viewpoint, Cambridge, MA: The MIT Press.
• Sher, G. (1996): “Did Tarski commit ‘Tarski’s fallacy’?” Journal of Symbolic Logic 61, pp. 653-686.
• Sher, G. (1999): “Is Logic a Theory of the Obvious?”, pp. 207-238 in Varzi (1999).
• Smiley, T. (1995): “A Tale of Two Tortoises”, Mind 104, pp. 725-36.
• Smiley, T. (1998): “Consequence, Conceptions of”, pp. 599-603 in Routledge Encyclopedia of Philosophy, vol. 2, ed. E. Craig. London: Routledge.
• Sundholm, G. (1983): “Systems of Deduction”, in Gabbay and Guenthner (1983).
• Tarski, A. (1933): “Pojecie prawdy w jezykach nauk dedukeycyjnych”, translated as “On the Concept of Truth in Formalized Languages”, pp. 152-278 in Tarski (1983).
• Tarski, A. (1936): “On the Concept of Logical Consequence”, pp. 409-420 in Tarski (1983).
• Tarski, A. (1983): Logic, Semantics, Metamathematics, 2nd ed. Indianapolis: Hackett Publishing.
• Tarski, A. (1986): “What are logical notions?” History and Philosophy of Logic 7, pp. 143-154.
• Tharp, L. (1975): “Which Logic is the Right Logic?” Synthese 31, pp. 1-21.
• Warbrod, K., (1999): “Logical Constants” Mind 108, pp. 503-538.
• Williamson, T. (1999): “Existence and Contingency”, Proceedings of the Aristotelian Society Supplementary Vol. 73, pp. 181-203.
• Varzi, A., ed. (1999): European Review of Philosophy, Vol. 4: The Nature of Logic, Stanford: CSLI Publications.

Author Information

Matthew McKeon
Email: mckeonm@msu.edu
Michigan State University
U. S. A.

Deductive-Theoretic Conceptions of Logical Consequence

According to the deductive-theoretic conception of logical consequence, a sentence X is a logical consequence of a set K of sentences if and only if X is a deductive consequence of K, that is, X is deducible or provable from K. Deductive consequence is clarified in terms of the notion of proof in a correct deductive system. Since, arguably, logical consequence conceived deductive-theoretically is not a compact relation and deducibility in a deductive system is, there are languages for which deductive consequence cannot be defined in terms of deducibility in a correct deductive system. However, it is true that if a sentence is deducible in a correct deductive system from other sentences, then the sentence is a deductive consequence of them. A deductive system is correct only if its rules of inference correspond to intuitively valid principles of inference. So whether or not a natural deductive system is correct brings into play rival theories of valid principles of inference such as classical, relevance, intuitionistic, and free logics.

Table of Contents

1. Introduction
2. Linguistic Preliminaries: the Language M
   1. Syntax of M
   2. Semantics for M
3. What is a Logic?
4. Deductive System N
5. The Status of the Deductive Characterization of Logical Consequence in Terms of N
   1. Tarski’s argument that the model-theoretic characterization of logical consequence is more basic than its characterization in terms of a deductive system
   2. Is deductive system N correct?
      1. Relevance logic
      2. Intuitionistic logic
      3. Free logic
6. Conclusion
7. References and Further Reading

1. Introduction

According to the deductive-theoretic conception of logical consequence, a sentence X is a logical consequence of a set K of sentences if and only if X is a deductive consequence of K, that is, X is deducible from K. X is deducible from K just in case there is an actual or possible deduction of X from K. In such a case, we say that X may be correctly inferred from K or that it would be correct to conclude X from K. A deduction is associated with a pair ; the set K of sentences is the basis of the deduction, and X is the conclusion. A deduction from K to X is a finite sequence S of sentences ending with X such that each sentence in S (that is, each intermediate conclusion) is derived from a sentence (or more) in K or from previous sentences in S in accordance with a correct principle of inference. The notion of a deduction is clarified by appealing to a deductive system. A deductive system D is a collection of rules that govern which sequences of sentences, associated with a given , are allowed and which are not. Such a sequence is called a proof in D (or, equivalently, a deduction in D) of X from K. The rules must be such that whether or not a given sequence associated with qualifies as a proof in D of X from K is decidable purely by inspection and calculation. That is, the rules provide a purely mechanical procedure for deciding whether a given object is a proof in D of X from K. We write

K ⊢_D X

to mean

X is deducible in deductive system D from K.

See the entry Logical Consequence, Philosophical Considerations for discussion of the interplay between the concepts of logical consequence and deductive consequence, and deductive systems. We say that a deductive system D is correct when for any K and X, proofs in D of X from K correspond to intuitively valid deductions. For a given language the deductive consequence relation is defined in terms of a correct deductive system D only if it is true that

X is a deductive consequence of K if and only if X is deducible in D from K.

Sundholm (1983) offers a thorough survey of three main types of deductive systems. In this article, a natural deductive system is presented that originates in the work of the mathematician Gerhard Gentzen (1934) and the logician Fredrick Fitch (1952). We will refer to the deductive system as N (for ‘natural deduction’). For an in-depth introductory presentation of a natural deductive system very similar to N see Barwise and Etchemendy (2001). N is a collection of inference rules. A proof of X from K that appeals exclusively to the inference rules of N is a formal deduction or formal proof. We shall take a formal proof to be associated with a pair where K is a set of sentences from a first-order language M, which will be introduced below, and X is an M-sentence. The set K of sentences is the basis of the deduction, and X is the conclusion. We say that a formal deduction from K to X is a finite sequence S of sentences ending with X such that each sentence in S is either an assumption, deduced from a sentence (or more) in K, or deduced from previous sentences in S in accordance with one of N’s inference rules.

Formal proofs are not only epistemologically significant for securing knowledge, but also the derivations making up formal proofs may serve as models of the informal deductive reasoning performed using sentences from language M. Indeed, a primary value of a formal proof is that it can serve as a model of ordinary deductive reasoning that explains the force of such reasoning by representing the principles of inference required to get to X from K.

Gentzen, one of the first logicians to present a natural deductive system, makes clear that a primary motive for the construction of his system is to reflect as accurately as possible the actual logical reasoning involved in mathematical proofs. He writes,

My starting point was this: The formalization of logical deduction especially as it has been developed by Frege, Russell, and Hilbert, is rather far removed from the forms of deduction used in practice in mathematical proofs…In contrast, I intended first to set up a formal system which comes as close as possible to actual reasoning. The result was a ‘calculus of natural deduction’. (Gentzen 1934, p. 68)

Natural deductive systems are distinguished from other deductive systems by their usefulness in modeling ordinary, informal deductive inferential practices. Paraphrasing Gentzen, we may say that if one is interested in seeing logical connections between sentences in the most natural way possible, then a natural deductive system is a good choice for defining the deductive consequence relation.

The remainder of the article proceeds as follows. First, an interpreted language M is given. Next, we present the deductive system N and represent the deductive consequence relation in M. After discussing the philosophical significance of the deductive consequence relation defined in terms of N, we consider some standard criticisms of the correctness of deductive system N.

2. Linguistic Preliminaries: the Language M

Here we define a simple language M, a language about the McKeon family, by first sketching what strings qualify as well-formed formulas (wffs) in M. Next we define sentences from formulas, and then give an account of truth in M, that is we describe the conditions in which M-sentences are true.

a. Syntax of M

Building blocks of formulas

Terms

Individual names—’beth’, ‘kelly’, ‘matt’, ‘paige’, ‘shannon’, ‘evan’, and ‘w₁‘, ‘w₂‘, ‘w₃‘, etc.

Variables—’x’, ‘y’, ‘z’, ‘x₁‘, ‘y₁‘, ‘z₁‘, ‘x₂‘, ‘y₂‘, ‘z₂‘, etc.

Predicates

1-place predicates—’Female’, ‘Male’

2-place predicates—’Parent’, ‘Brother’, ‘Sister’, ‘Married’, ‘OlderThan’, ‘Admires’, ‘=’.

Blueprints of well-formed formulas (wffs)

Atomic formulas: An atomic wff is any of the above n-place predicates followed by n terms which are enclosed in parentheses and separated by commas.

Formulas: The general notion of a well-formed formula (wff) is defined recursively as follows:

(1) All atomic wffs are wffs.
(2) If α is a wff, so is ~α.
(3) If α and β are wffs, so is (α & β).
(4) If α and β are wffs, so is (α v β).
(5) If α and β are wffs, so is (α → β).
(6) If Ψ is a wff and v is a variable, then ∃vΨ is a wff.
(7) If Ψ is a wff and v is a variable, then ∀vΨ is a wff.
Finally, no string of symbols is a well-formed formula of M unless the string can be derived from (1)-(7).

The signs ‘~’, ‘&’, ‘v‘, and ‘→’, are called sentential connectives. The signs ‘∀’ and ‘∃’ are called quantifiers.

It will prove convenient to have available in M an infinite number of individual names as well as variables. The strings ‘Parent(beth, paige)’ and ‘Male(x)’ are examples of atomic wffs. We allow the identity symbol in an atomic formula to occur in between two terms, e.g., instead of ‘=(evan, evan)’ we allow ‘(evan = evan)’. The symbols ‘~’, ‘&’, ‘v‘, and ‘→’ correspond to the English words ‘not’, ‘and’, ‘or’ and ‘if…then’, respectively. ‘∃’ is our symbol for an existential quantifier and ‘∀’ represents the universal quantifier. ∃vΨ and ∀vΨ correspond to for some v, Ψ, and for all v, Ψ, respectively. For every quantifier, its scope is the smallest part of the wff in which it is contained that is itself a wff. An occurrence of a variable v is a bound occurrence iff it is in the scope of some quantifier of the form ∃v or the form ∀v, and is free otherwise. For example, the occurrence of ‘x’ is free in ‘Male(x)’ and in ‘∃y Married(y, x)’. The occurrences of ‘y’ in the second formula are bound because they are in the scope of the existential quantifier. A wff with at least one free variable is an open wff, and a closed formula is one with no free variables. A sentence is a closed wff. For example, ‘Female(kelly)’ and ‘∃y∃x Married(y, x)’ are sentences but ‘OlderThan(kelly, y)’ and ‘(∃x Male(x) & Female(z))’ are not. So, not all of the wffs of M are sentences. As noted below, this will affect our definition of truth for M.

b. Semantics for M

We now provide a semantics for M. This is done in two steps. First, we specify a domain of discourse, that is, the chunk of the world that our language M is about, and interpret M’s predicates and names in terms of the elements composing the domain. Then we state the conditions under which each type of M-sentence is true. To each of the above syntactic rules (1-7) there corresponds a semantic rule that stipulates the conditions in which the sentence constructed using the syntactic rule is true. The principle of bivalence is assumed and so ‘not true’ and ‘false’ are used interchangeably. In effect, the interpretation of M determines a truth-value (true, false) for each and every sentence of M.

Domain D—The McKeons: Matt, Beth, Shannon, Kelly, Paige, and Evan.

Here are the referents and extensions of the names and predicates of M.

Terms: ‘matt’ refers to Matt, ‘beth’ refers to Beth, ‘shannon’ refers to Shannon, etc.

Predicates. The meaning of a predicate is identified with its extension, that is the set (possibly empty) of elements from the domain D the predicate is true of. The extension of a one-place predicate is a set of elements from D, the extension of a two-place predicate is a set of ordered pairs of elements from D.

The extension of ‘Male’ is {Matt, Evan}.

The extension of ‘Female’ is {Beth, Shannon, Kelly, Paige}.

The extension of ‘Parent’ is {<Matt, Shannon>, <Matt, Kelly>, <Matt, Paige>, <Matt, Evan>, <Beth, Shannon>, <Beth, Kelly>, <Beth, Paige>, <Beth, Evan>}.

The extension of ‘Married’ is {<Matt, Beth>, <Beth, Matt>}.

The extension of ‘Sister’ is {<Shannon, Kelly>, <Kelly, Shannon>, <Shannon, Paige>, <Paige, Shannon>, <Kelly, Paige>, <Paige, Kelly>, <Kelly, Evan>, <Paige, Evan>, <Shannon, Evan>}.

The extension of ‘Brother’ is {<Evan, Shannon>, <Evan, Kelly>, <Evan, Paige>}.

The extension of ‘OlderThan’ is {<Beth, Matt>, <Beth, Shannon>, <Beth, Kelly>, <Beth, Paige>, <Beth, Evan>, <Matt, Shannon>, <Matt, Kelly>, <Matt, Paige>, <Matt, Evan>, <Shannon, Kelly>, <Shannon, Paige>, <Shannon, Evan>, <Kelly, Paige>, <Kelly, Evan>, <Paige, Evan>}.

The extension of ‘Admires’ is {<Matt, Beth>, <Shannon, Matt>, <Shannon, Beth>, <Kelly, Beth>, <Kelly, Matt>, <Kelly, Shannon>, <Paige, Beth>, <Paige, Matt>, <Paige, Shannon>, <Paige, Kelly>, <Evan, Beth>, <Evan, Matt>, <Evan, Shannon>, <Evan, Kelly>, <Evan, Paige>}.

The extension of ‘=’ is {<Matt, Matt>, <Beth, Beth>, <Shannon, Shannon>, <Kelly, Kelly>, <Paige, Paige>, <Evan, Evan>}.

The atomic sentence ‘Female(kelly)’ is true because, as indicated above, the referent of ‘kelly’ is in the extension of the property designated by ‘Female’. The atomic sentence ‘Married(shannon, kelly)’ is false because the ordered pair is not in the extension of the relation designated by ‘Married’.

(I)

An atomic sentence with a one-place predicate is true iff the referent of the term is a member of the extension of the predicate, and an atomic sentence with a two-place predicate is true iff the ordered pair formed from the referents of the terms in order is a member of the extension of the predicate.

(II)	~α is true iff α is false.
(III)	(α & β) is true when both α and β are true; otherwise (α & β) is false.
(IV)	(α v β) is true when at least one of α and β is true; otherwise (α v β) is false.
(V)	(α → β) is true if and only if (iff) α is false or β is true. So, (α → β) is false just in case α is true and β is false.

The meanings for ‘~’ and ‘&’ roughly correspond to the meanings of ‘not’ and ‘and’ as ordinarily used. We call ~α and (α & β) negation and conjunction formulas, respectively. The formula (~α v β) is called a disjunction and the meaning of ‘v‘ corresponds to inclusive or. There are a variety of conditionals in English (e.g., causal, counterfactual, logical), with each type having a distinct meaning. The conditional defined by (V) above is called the material conditional. One way of following (V) is to see that the truth conditions for (α → β) are the same as for ~(α & ~β).

By (II) ‘~Married(shannon, kelly)’ is true because, as noted above, ‘Married(shannon, kelly)’ is false. (II) also tells us that ‘~Female(kelly)’ is false since ‘Female(kelly)’ is true. According to (III), ‘(~Married(shannon, kelly) & Female(kelly))’ is true because ‘~Married(shannon, kelly)’ is true and ‘Female(kelly)’ is true. And ‘(Male(shannon) & Female(shannon))’ is false because ‘Male(shannon)’ is false. (IV) confirms that ‘(Female(kelly) v Married(evan, evan))’ is true because, even though ‘Married(evan, evan)’ is false, ‘Female(kelly)’ is true. From (V) we know that the sentence ‘(~(beth = beth) → Male(shannon))’ is true because ‘~(beth = beth)’ is false. If α is false then (α → β) is true regardless of whether or not β is true. The sentence ‘(Female(beth) → Male(shannon))’ is false because ‘Female(beth)’ is true and ‘Male(shannon)’ is false.

Before describing the truth conditions for quantified sentences we need to say something about the notion of satisfaction. We’ve defined truth only for the formulas of M that are sentences. So, the notions of truth and falsity are not applicable to non-sentences such as ‘Male(x)’ and ‘((x = x) → Female(x))’ in which ‘x’ occurs free. However, objects may satisfy wffs that are non-sentences. We introduce the notion of satisfaction with some examples. An object satisfies ‘Male(x)’ just in case that object is male. Matt satisfies ‘Male(x)’, Beth does not. This is the case because replacing ‘x’ in ‘Male(x)’ with ‘Matt’ yields a truth while replacing the variable with ‘beth’ yields a falsehood. An object satisfies ‘((x = x) → Female(x))’ if and only if it is either not identical with itself or is a female. Beth satisfies this wff (we get a truth when ‘beth’ is substituted for the variable in all of its occurrences), Matt does not (putting ‘matt’ in for ‘x’ wherever it occurs results in a falsehood). As a first approximation, we say that an object with a name, say ‘a’, satisfies a wff Ψv in which at most v occurs free if and only if the sentence that results by replacing v in all of its occurrences with ‘a’ is true. ‘Male(x)’ is neither true nor false because it is not a sentence, but it is either satisfiable or not by a given object. Now we define the truth conditions for quantifications, utilizing the notion of satisfaction. For a more detailed discussion of the notion of satisfaction, see the article, “Logical Consequence, Model-Theoretic Conceptions.”

Let Ψ be any formula of M in which at most v occurs free.

(VI)	∃vΨ is true just in case there is at least one individual in the domain of quantification (e.g. at least one McKeon) that satisfies Ψ.
(VII)	∀vΨ is true just in case every individual in the domain of quantification (e.g. every McKeon) satisfies Ψ.

Here are some examples. ‘∃x(Male(x) & Married(x, beth))’ is true because Matt satisfies ‘(Male(x) & Married(x, beth))’; replacing ‘x’ wherever it appears in the wff with ‘matt’ results in a true sentence. The sentence ‘∃xOlderThan(x, x)’ is false because no McKeon satisfies ‘OlderThan(x, x)’, that is replacing ‘x’ in ‘OlderThan(x, x)’ with the name of a McKeon always yields a falsehood.

The universal quantification ‘∀x( OlderThan(x, paige) → Male(x))’ is false for there is a McKeon who doesn’t satisfy ‘(OlderThan(x, paige) → Male(x))’. For example, Shannon does not satisfy ‘(OlderThan(x, paige) → Male(x))’ because Shannon satisfies ‘OlderThan(x, paige)’ but not ‘Male(x)’. The sentence ‘∀x(x = x)’ is true because all McKeons satisfy ‘x = x’; replacing ‘x’ with the name of any McKeon results in a true sentence.

Note that in the explanation of satisfaction we suppose that an object satisfies a wff only if the object is named. But we don’t want to presuppose that all objects in the domain of discourse are named. For the purposes of an example, suppose that the McKeons adopt a baby boy, but haven’t named him yet. Then, ‘∃x Brother(x, evan)’ is true because the adopted child satisfies ‘Brother(x, evan)’, even though we can’t replace ‘x’ with the child’s name to get a truth. To get around this is easy enough. We have added a list of names, ‘w_1′, ‘w_2′, ‘w_3′, etc. to M, and we may say that any unnamed object satisfies Ψv iff the replacement of v with a previously unused w_i assigned as a name of this object results in a true sentence. In the above scenerio, ‘∃xBrother(x, evan)’ is true because, ultimately, treating ‘w₁‘ as a temporary name of the child, ‘Brother(w₁, evan)’ is true. Of course, the meanings of the predicates would have to be amended in order to reflect the addition of a new person to the domain of McKeons.

3. What is a Logic?

We have characterized an interpreted formal language M by defining what qualifies as a sentence of M and by specifying the conditions under which any M-sentence is true. The received view of logical consequence entails that the logical consequence relation in M turns on the nature of the logical constants in the relevant M-sentences. We shall regard just the sentential connectives, the quantifiers of M, and the identity predicate as logical constants (the language M is a first-order language). For discussion of the notion of a logical constant see Logical Consequence, Philosophical Considerations and Logical Consequence, Model-Theoretic Conceptions. Intuitively, one M-sentence is a logical consequence of a set of M-sentences if and only if it is impossible for all the sentences in the set to be true without the former sentence being true as well. A model-theoretic conception of logical consequence in M clarifies this intuitive characterization of logical consequence by appealing to the semantic properties of the logical constants, represented in the above truth clauses (I)-(VII). The entry Logical Consequence, Model-Theoretic Conceptions formalizes the account of truth in language M and gives a model-theoretic characterization of logical consequence in M. In contrast to the model-theoretic conception, the deductive-theoretic conception clarifies logical consequence, conceived of in terms of deducibility, by appealing to the inferential properties of logical constants portrayed as intuitively valid principles of inference, that is, principles justifying steps in deductions. See Logical Consequence, Philosophical Considerations for discussion of the relationship between the logical consequence relation and the model-theoretic and deductive-theoretic conceptions of it.

Deductive system N’s inference rules, introduced below, are introduction and elimination rules, defined for each logical constant of our language M. An introduction rule introduces a logical constant into a proof and is useful for deriving a sentence that contains the constant. An elimination rule for the constant makes it possible to derive a sentence that has at least one less occurrence of the logical constant. Elimination rules are useful for deriving a sentence from another in which the constant appears.

Following Shapiro (1991, p. 3), we define a logic to be a language L plus either a model-theoretic or a deductive-theoretic account of logical consequence. A language with both characterizations is a full logic just in case both characterizations coincide. For discussion on the relationship between the model-theoretic and deductive-theoretic accounts of logical consequence, see Logical Consequence, Philosophical Considerations. The logic for M developed below may be viewed as a classical logic or a first-order theory.

4. Deductive System N

In stating N’s rules, we begin with the simpler inference rules and give a sample formal deduction of them in action. Then we turn to the inference rules that employ what we shall call sub-proofs. In the statement of the rules, we let P and Q be any sentences from our language M. We shall number each line of a formal deduction with a positive integer. We let k, l, m, n, o, p and q be any positive integers such that k < m, and l < m, and m < n < o < p < q.

&-Intro

	k.	P
	l.	Q
	m.	(P & Q)	&-Intro: k, l

&-Elim

	k.	(P & Q)				k.	(P & Q)
	m.	P	&-Elim: k			m.	Q	&-Elim: k

&-Intro allows us to derive a conjunction from both of its two parts (called conjuncts). According to the &-Elim rule we may derive a conjunct from a conjunction. To the right of the sentence derived using an inference rule is the justification. Steps in a proof are justified by identifying both the lines in the proof used and by citing the appropriate rule. The vertical lines serve as proof margins, which, as you will shortly see, help in portraying the structure of a proof when it contains embedded sub-proofs.

~-Elim

	k.	~~P
	m.	P	~-Elim: k

The ~-Elim rule allows us to drop double negations and infer what was subject to the two negations.

v-Intro

	k.	P				k.	P
	m.	(P v Q)	v-Intro: k			m.	(Q v P)	v-Intro: k

By v-Intro we may derive a disjunction from one of its parts (called disjuncts).

→-Elim

	k.	(P → Q)
	l.	P
	m.	Q	→-Elim: k, l

The →- Elim rule corresponds to the principle of inference called modus ponens: from a conditional and its antecedent one may infer the consequent.

Here’s a sample deduction using the above inference rules. The formal deduction–the sequence of sentences 4-11—is associated with the pair

<{(Female(paige) & Female (kelly)), (Female(paige) → ~~Sister(paige, kelly)), (Female(kelly) → ~~Sister(paige, shannon))}, ((Sister(paige, kelly) & Sister(paige, shannon)) v Male(evan))>.

The first element is the set of basis sentences and the second element is the conclusion. We number the basis sentences and list them (beginning with 1) ahead of the deduction. The deduction ends with the conclusion.

	1.	(Female(paige) & Female (kelly))	Basis
	2.	(Female(paige) → ~~Sister(paige, kelly))	Basis
	3.	(Female(kelly) → ~~Sister(paige, shannon))	Basis
	4.	Female(paige)	&-Elim: 1
	5.	Female(kelly)	&-Elim: 1
	6.	~~Sister(paige, kelly)	→-Elim: 2, 4
	7.	Sister(paige, kelly)	~-Elim: 6
	8.	~~Sister(paige, shannon)	→-Elim: 3, 5
	9.	Sister(paige, shannon)	~-Elim: 8
	10.	(Sister(paige, kelly) & Sister(paige, shannon))	&-Intro: 7, 9
	11.	((Sister(paige, kelly) & Sister(paige, shannon)) v Male(evan))	v-Intro: 10

Again, the column all the way to the right gives the explanations for each line of the proof. Assuming the adequacy of N, the formal deduction establishes that the following inference is correct.

	(Female(paige) & Female (kelly))
	(Female(paige) → ~~Sister(paige, kelly))
	(Female(kelly) → ~~Sister(paige, shannon))
(therefore)	((Sister(paige, kelly) & Sister(paige, shannon)) v Male(evan))

For convenience in building proofs, we expand M to include ‘⊥’, which we use as a symbol for a contradiction (e.g., ‘(Female(beth) & ~Female(beth))’).

⊥-Intro

	k.	P
	l.	~P
	m.	⊥	⊥-Intro: k, l

⊥-Elim

	k.	⊥
	m.	P	⊥-Elim: k

If we have derived a sentence and its negation we may derive ⊥ using ⊥-Intro. The ⊥-Elim rule represents the idea that any sentence P is deducible from a contradiction. So, from ⊥ we may derive any sentence P using ⊥-Elim.

Here’s a deduction using the two rules.

	1.	(Parent(beth, evan) & ~Parent(beth, evan))	Basis
	2.	Parent(beth, evan)	&-Elim: 1
	3.	~Parent(beth, evan)	&-Elim: 1
	4.	⊥	⊥-Intro: 2, 3
	5.	Parent(beth, shannon)	⊥-Elim: 4

For convenience, we introduce a reiteration rule that allows us to repeat steps in a proof as needed.

Reit

	k.	P
		.
		.
		.
	m.	P	Reit: k

We now turn to the rules for the sentential connectives that employ what we shall call sub-proofs. Consider the following inference.

	1.	~(Married(shannon, kelly) & OlderThan(shannon, kelly))
	2.	Married(shannon, kelly)
(therefore)		~Olderthan(shannon, kelly)

Here is an informal deduction of the conclusion from the basis sentences.

Proof: Suppose that ‘Olderthan(shannon, kelly)’ is true. Then, from this assumption and basis sentence 2 it follows that ‘((Shannon is married to Kelly) & (Shannon is taller than Kelly))’ is true. But this contradicts the first basis sentence ‘~((Shannon is married to Kelly) & (Shannon is taller than Kelly))’, which is true by hypothesis. Hence our initial supposition is false. We have derived that ‘~(Shannon is married to Kelly)’ is true.

Such a proof is called a reductio ad absurdum proof (or reductio for short). Reductio ad absurdum is Latin for ‘reduction to the absurd’. (For more information, see the article “Reductio ad absurdum“.) In order to model this proof in N we introduce the ~-Intro rule.

~-Intro

			k.	P	Assumption
				.
				.
				.
			m.	⊥
	n.		~P		~-Intro: k-m

The ~-Intro rule allows us to infer the negation of an assumption if we have derived a contradiction, symbolized by ‘⊥’, from the assumption. The indented proof margin (k-m) signifies a sub-proof. In a sub-proof the first line is always an assumption (and so requires no justification), which is cancelled when the sub-proof is ended and we are back out on a line that sits on a wider proof margin. The effect of this is that we can no longer appeal to any of the lines in the sub-proof to generate later lines on wider proof margins. No deduction ends in the middle of a sub-proof.

Here is a formal analogue of the above informal reductio.

	1.		~(Married(shannon, kelly) & OlderThan(shannon, kelly))		Basis
	2.		Married(shannon, kelly)		Basis
			3.	OlderThan(shannon, kelly)	Assumption
			4.	(Married(shannon, kelly) & OlderThan(shannon, kelly))	&-Intro: 2, 3
			5.	⊥	⊥-Intro: 1, 4
	6.		~Olderthan(shannon, kelly)		~-Intro: 3-5

We signify a sub-proof with the indented proof margin line; the start and finish of a sub-proof is indicated by the start and break of the indented proof margin. An assumption, like a basis sentence, is a supposition we suppose true for the purposes of the deduction. The difference is that whereas a basis sentence may be used at any step in a proof, an assumption may only be used to make a step within the sub-proof it heads. At the end of the sub-proof, the assumption is discharged. We now look at more sub-proofs in action and introduce another of N’s inference rules. Consider the following inference.

	1.	(Male(kelly) v Female(kelly))
	2.	(Male(kelly) → ~Sister(kelly, paige))
	3.	(Female(kelly) → ~Brother(kelly, evan))
(therefore)		(~Sister(kelly, paige) v ~Brother(kelly, evan))

Informal Proof:

By assumption ‘(Male(kelly) v Female(kelly))’ is true, that is, by assumption at least one of the disjuncts is true.

Suppose that ‘Male(kelly)’ is true. Then by modus ponens we may derive that ‘~Sister(kelly, paige)’ is true from this assumption and the basis sentence 2. Then ‘(~Sister(kelly, paige) v ~Brother(kelly, evan))’ is true.

Suppose that ‘Female(kelly)’ is true. Then by modus ponens we may derive that ‘~Brother(kelly, evan)’ is true from this assumption and the basis sentence 3. Then ‘(~Sister(kelly, paige) v ~Brother(kelly, evan))’ is true.

So in either case we have derived that ‘(~Sister(kelly, paige) v ~Brother(kelly, evan))’ is true. Thus we have shown that this sentence is a deductive consequence of the basis sentences.

We model this proof in N using the v-Elim rule.

v-Elim

	k.		(P v Q)
			m.	P	Assumption
				.
				.
				.
			n.	R
			o.	Q	Assumption
				.
				.
				.
			p.	R
	q.		R		v-Elim: k, m-n, o-p

The v-Elim rule allows us to derive a sentence from a disjunction by deriving it from each disjunct, possibly using sentences on earlier lines that sit on wider proof margins.

The following formal proof models the above informal one.

	1.		(Male(kelly) v Female(kelly))		Basis
	2.		(Male(kelly) → ~Sister(kelly, paige))		Basis
	3.		(Female(kelly) → ~Brother(kelly, evan))		Basis
			4.	Male(kelly)	Assumption
			5.	~Sister(kelly, paige)	→-Elim: 2, 4
			6.	(~Sister(kelly, paige) v ~Brother(kelly, evan))	v-Intro: 5
			7.	Female(kelly)	Assumption
			8.	~Brother(kelly, evan)	→-Elim: 3, 7
			9.	(~Sister(kelly, paige) v ~Brother(kelly, evan))	v-Intro: 8
	10.		(~Sister(kelly, paige) v ~Brother(kelly, evan))		v-Elim: 1, 4-6, 7-9

	1.		(P v Q)		Basis
	2.		~P		Basis
			3.	P	Assumption
			4.	⊥	⊥-Intro: 2, 3
			5.	Q	⊥-Elim: 4
			6.	Q	Assumption
			7.	Q	Reit: 6
	8.		Q		v-Elim: 1, 3-5, 6-7

Now we introduce the →-Intro rule by considering the following inference.

	1.	(Olderthan(shannon, kelly) → OlderThan(shannon, paige))
	2.	(OlderThan(shannon, paige) → OlderThan(shannon, evan))
(therefore)		(Olderthan(shannon, kelly) → OlderThan(shannon, evan))

Informal proof:

Suppose that OlderThan(shannon, kelly). From this assumption and basis sentence 1 we may derive, by modus ponens, that OlderThan(shannon, paige). From this and basis sentence 2 we get, again by modus ponens, that OlderThan(shannon, evan). Hence, if OlderThan(shannon, kelly), then OlderThan(shannon, evan).

The structure of this proof is that of a conditional proof: a deduction of a conditional from a set of basis sentence which starts with the assumption of the antecedent, then a derivation of the consequent, and concludes with the conditional. To build conditional proofs in N, we rely on the →-Intro rule.

→-Intro

			k.	P	Assumption
				.
				.
				.
			m.	Q
	n.		(P → Q)		→-Intro: k-m

According to the →-Intro rule we may derive a conditional if we derive the consequent Q from the assumption of the antecedent P, and, perhaps, other sentences occurring earlier in the proof on wider proof margins. Again, such a proof is called a conditional proof.

We model the above informal conditional proof in N as follows.

	1.		(Olderthan(shannon, kelly) → OlderThan(shannon, paige))		Basis
	2.		(Olderthan(shannon, paige) → OlderThan(shannon, evan))		Basis
			3.	OlderThan(shannon, kelly)	Assumption
			4.	OlderThan(shannon, paige)	→-Elim: 1, 3
			5.	OlderThan(shannon, evan)	→-Elim: 2, 4
	6.		(OlderThan(shannon, kelly) → OlderThan(shannon, evan))		→-Intro: 3-5

Mastery of a deductive system facilitates the discovery of proof pathways in hard cases and increases one’s efficiency in communicating proofs to others and explaining why a sentence is a logical consequence of others. For example, suppose that (1) if Beth is not Paige’s parent, then it is false that if Beth is a parent of Shannon, Shannon and Paige are sisters. Further suppose (2) that Beth is not Shannon’s parent. Then we may conclude that Beth is Paige’s parent. Of course, knowing the type of sentences involved is helpful for then we have a clearer idea of the inference principles that may be involved in deducing that Beth is a parent of Paige. Accordingly, we represent the two basis sentences and the conclusion in M, and then give a formal proof of the latter from the former.

	1.		(~Parent(beth, paige) → ~(Parent(beth, shannon) → Sister(shannon, paige)))				Basis
	2.		~Parent(beth, shannon)				Basis
			3.	~Parent(beth, paige)			Assumption
			4.	~(Parent(beth, shannon) → Sister(shannon, paige))			→-Elim: 1, 3
					5.	Parent(beth, shannon)	Assumption
					6.	⊥	⊥-Intro: 2, 5
					7.	Sister(shannon, paige)	⊥-Elim: 6
			8.	(Parent(beth, shannon) → Sister(shannon, paige))			→-Intro: 5-7
			9.	⊥			⊥-Intro: 4, 8
	10.		~~Parent(beth, paige)				~-Intro: 3-9
	11.		Parent(beth, paige)				~-Elim: 10

Because we derived a contradiction at line 9, we got ‘~~Parent(beth, paige)’ at line 10, using ~-Intro, and then we derived ‘Parent(beth, paige)’ by ~-Elim. Look at the conditional proof (lines 5-7) from which we derived line 8. Pretty neat, huh? Lines 2 and 5 generated the contradiction from which we derived ‘Sister(shannon, paige)’ at line 7 in order to get the conditional at line 8. This is our first example of a sub-proof (5-7) embedded in another sub-proof (3-9). It is unlikely that independent of the resources of a deductive system, a reasoner would be able to readily build the informal analogue of this pathway from the basis sentences to the sentence at line 11. Again, mastery of a deductive system such as N can increase the efficiency of our performances of rigorous reasoning and cultivate skill at producing elegant proofs (proofs that take the least number of steps to get from the basis to the conclusion).

We now introduce the Intro and Elim rules for the identity symbol and the quantifiers. Let n and n’ be any names, and Ωn and Ωn’ be any well-formed formulas in which n and n’ appear and that have no free variables.

=-Intro

	k. (n = n) =-Intro

=-Elim

	k.	Ωn
	l.	(n = n’ )
	m.	Ωn’	=-Elim: k, l

The =-Intro rule allows us to introduce (n = n) at any step in a proof. Since (n = n) is deducible from any sentence, there is no need to identify the lines from which line k is derived. In effect, the =-Intro rule confirms that ‘(paige = paige)’, ‘(shannon = shannon)’, ‘(kelly = kelly)’, etc… may be inferred from any sentence(s). The =-Elim rule tells us that if we have proven Ωn and (n = n’ ), then we may derive Ωn’ which is gotten from Ωn by replacing n with n’ in some but possibly not all occurrences. The =-Elim rule represents the principle known as the indiscernibility of identicals, which says that if (n = n’ ) is true, then whatever is true of the referent of n is true of the referent of n’. This principle grounds the following inference

	1.	~Sister(beth, kelly)
	2.	(beth = shannon)
(therefore)		~Sister(shannon, kelly)

The indiscernibility of identicals is fairly obvious. If I know that Beth isn’t Kelly’s sister and that Beth is Shannon (perhaps ‘Shannon’ is an alias) then this establishes, with the help of the indiscernibility of identicals, that Shannon isn’t Kelly’s sister. Now we turn to the quantifier rules.

Let Ωv be a formula in which v is the only free variable, and let n be any name.

∃-Intro

	k.	Ωn
	m.	∃vΩv	∃-Intro: k

∃-Elim

	k.		∃vΩv
	[n]		m.	Ωn	Assumption
				.
				.
				.
			n.	P
	o.		P		∃-Elim: k, m-n

Here, n must be unique to the subproof, that is, n doesn’t occur on any of the lines above m and below n.

The ∃-Intro rule, which represents the principle of inference known as existential generalization, tells us that if we have proven Ωn, then we may derive ∃vΩv which results from Ωn by replacing n with a variable v in some but possibly not all of its occurrences and prefixing the existential quantifier. According to this rule, we may infer, say, ‘∃x Married(x, matt)’ from the sentence ‘Married(beth, matt)’. By the ∃-Elim rule, we may reason from a sentence that is produced from an existential quantification by stripping the quantifier and replacing the resulting free variable in all of its occurrences by a name which is new to the proof. Recall that the language M has an infinite number of constants, and the name introduced by the ∃-Elim rule may be one of the w_i. We regard the assumption at line l, which starts the embedded sub-proof, as saying “Suppose n names an arbitrary individual from the domain of discourse such that Ωn is true.” To illustrate the basic idea behind the ∃-Elim rule, if I tell you that Shannon admires some McKeon, you can’t infer that Shannon admires any particular McKeon such as Matt, Beth, Shannon, Kelly, Paige, or Evan. Nevertheless we have it that she admires somebody. The principle of inference corresponding to the ∃-Elim rule, called existential instantiation, allows us to assign this ‘somebody’ an arbitrary name new to the proof, say, ‘w₁‘ and reason within the relevant sub-proof from ‘Shannon admires w₁‘. Then we cancel the assumption and infer a sentence that doesn’t make any claims about w₁. For example, suppose that (1) Shannon admires some McKeon. Let’s call this McKeon ‘w₁‘, that is, assume (2) that Shannon admires a McKeon named ‘w₁‘. By the principle of inference corresponding to v-Intro we may derive (3) that Shannon admires w₁ or w₁ admires Kelly. From (3), we may infer by existential generalization (4) that for some McKeon x, Shannon admires x or x admires Kelly. We now cancel the assumption (that is, cancel (2)) by concluding (5) that for some McKeon x, Shannon admires x or x admires Kelly from (1) and the subproof (2)-(4), by existential instantiation. Here is the above reasoning set out formally.

	1.		∃x Admires(shannon, x)		Basis
	[w1]		2.	Admires(shannon, w1)	Assumption
			3.	(Admires(shannon, w1) v Admires(w1, kelly))	v-Intro: 2
			4.	∃x(Admires(shannon, x) v Admires(x, kelly))	∃-Intro: 3
	5.		∃x(Admires(shannon, x) v Admires(x, kelly))		∃-Elim: 1, 2-4

The string at the assumption of the sub-proof (line 2) says “Suppose that ‘w₁ ‘ names an arbitrary McKeon such that ‘Admires(shannon, w₁)’ is true.” This is not a sentence of M, but of the meta-language for M, that is, the language used to talk about M. Hence, the ∃-Elim rule (as well as the ∀-Intro rule introduced below) has a meta-linguistic character.

∀-Intro

	[n]		k.		Assumption
				.
				.
				.
			m.	Ωn
	n.		∀vΩv		∀-Intro: k-m
				n must be unique to the subproof

∀-Elim

	k.	∀vΩv
	m.	Ωn	∀-Elim: k

The ∀-Elim rule corresponds to the principle of inference known as universal instantiation: to infer that something holds for an individual of the domain if it holds for the entire domain. The ∀-Intro rule allows us to derive a claim that holds for the entire domain of discourse from a proof that the claim holds for an arbitrary selected individual from the domain. The assumption at line k reads in English “Suppose n names an arbitrarily selected individual from the domain of discourse.” As with the ∃-Elim rule, the name introduced by the ∀-Intro rule may be one of the w_i. The ∀-Intro rule corresponds to the principle of inference often called universal generalization.

For example, suppose that we are told that (1) if a McKeon admires Paige, then that McKeon admires himself/herself, and that (2) every McKeon admires Paige. To show that we may correctly infer that every McKeon admires himself/herself we appeal to the principle of universal generalization, which (again) is represented in N by the ∀-Intro rule. We begin by assuming that (3) a McKeon is named ‘w₁‘. All we assume about w₁ is that w₁ is one of the McKeons. From (2), we infer that (4) w₁ admires Paige. We know from (1), using the principle of universal instantiation (the ∀-Elim rule in N), that (5) if w₁ loves Paige then w₁ loves w₁. From (4) and (5) we may infer that (6) w₁ loves w₁ by modus ponens. Since w₁ is an arbitrarily selected individual (and so what holds for w₁ holds for all McKeons) we may conclude from (3)-(6) that (7) every McKeon loves himself/herself follows from (1) and (2) by universal generalization. This reasoning is represented by the following formal proof.

	1.		∀x(Admires(x, paige) → Admires(x, x))		Basis
	2.		∀x Admires(x, paige)		Basis
	[w1]		3.		Assumption
			4.	Admires(w1, paige)	∀-Elim: 2
			5.	(Admires(w1, paige) → Admires(w1, w1))	∀-Elim: 1
			6.	Admires(w1, w1)	→-Elim: 4, 5
	7.		∀x Admires(x, x)		∀-Intro: 3-6

Line 3, the assumption of the sub-proof, corresponds to the English sentence “Let ‘w₁‘ refer to an arbitrary McKeon.” The notion of a name referring to an arbitrary individual from the domain of discourse, utilized by both the ∀-Intro and ∃-Elim rules in the assumptions that start the respective sub-proofs, incorporates two distinct ideas. One, relevant to the ∃-Elim rule, means “some specific object, but I don’t know which”, while the other, relevant to the ∀-Intro rule means “any object, it doesn’t matter which” (See Pelletier 1999, pp. 118-120 for discussion.)

Consider:

K = {All McKeons admire those who admire somebody, Some McKeon admires a McKeon}
X = Paige admires Paige

Here’s a proof that X is deducible from K.

	1.		∀x(∃y Admires(x, y) → ∀z Admires(z, x))		Basis
	2.		∃x∃y Admires(x, y)		Basis
	[w1]		3.	∃y Admires(w1, y)	Assumption
			4.	(∃y Admires(w1, y) → ∀z Admires(z, w1))	∀-Elim: 1
			5.	∀z Admires(z, w1)	→-Elim: 3, 4
			6.	Admires(paige, w1)	∀-Elim: 5
			7.	∃y Admires(paige, y)	∃-Intro: 6
			8.	(∃y Admires(paige, y) → ∀z Admires(z, paige))	∀-Elim: 1
			9.	∀z Admires(z, paige)	→-Elim: 7, 8
			10.	Admires(paige, paige)	∀-Elim: 9
	11.		Admires(paige, paige)		∃-Elim: 2, 3-10

An informal correlate put somewhat succinctly, runs as follows.

Let’s call the unnamed admirer, mentioned in (2), w₁. From this and (1), every McKeon admires w₁ and so Paige admires w₁. Hence, Paige admires somebody. From this and (1) it follows that everybody admires Paige. So, Paige admires Paige. This is our desired conclusion

Even though the informal proof skips steps and doesn’t mention by name the principles of inference used, the formal proof guides its construction.

5. The Status of the Deductive Characterization of Logical Consequence in Terms of N

We began the article by presenting the deductive-theoretic characterization of logical consequence: X is a logical consequence of a set K of sentences if and only if X is deducible from K, that is, there is a deduction of X from K. To make it official, we now characterize the deductive consequence relation in M in terms of deducibility in N.

X is a deductive consequence of K if and only if K ⊢_N X, that is, X is deducible in N from K

We now inquire into the status of this characterization of deductive consequence.

The first thing to note is that deductive system N is complete and sound with respect to the model-theoretic consequence relation defined in Logical Consequence, Model-Theoretic Conceptions: Section 4.4. Let

K ⊢_N X

abbreviate

X is deducible in N from K

Similarly, let

K ⊨ X

abbreviate

X is a model-theoretic consequence of K, that is, every M-structure that is a model of K is also a model of X. (For more information on structures and models, see Logical Consequence, Model-Theoretic Conceptions.)

The completeness and soundness of N means that for any set K of M sentences and M-sentence X, K ⊢_N X if and only if K ⊨ X. A soundness proof establishes K ⊢_N X only if K ⊨ X, and a completeness proof establishes K ⊢_N X if K ⊨ X. So, the ⊢_N and ⊨ relations, defined on sentences of M, are extensionally equivalent. The question arises: which characterization of the logical consequence relation is more basic or fundamental?

a. Tarski’s argument that the model-theoretic characterization of logical consequence is more basic than its characterization in terms of a deductive system

The first thing to note is that the ⊢_N-consequence relation is compact. For any deductive system D and pair there is a K’ such that, K ⊢_D X if and only if K’ ⊢_D X, where K’ is a finite subset of sentences from K. As pointed out by Tarski (1936), among others, there are intuitively correct principles of inference reflected in certain languages according to which one may infer a sentence X from a set K of sentences, even though it is incorrect to infer X from any finite subset of K. Here’s a rendition of his reasoning, focusing on the ⊢_N-consequence relation defined on a language for arithmetic, which allows us to talk about the natural numbers 0, 1, 2, 3, and so on. Let ‘P’ be a predicate defined over the domain of natural numbers and let ‘NatNum(x)’ abbreviate ‘x is a natural number’. According to Tarski, intuitively,

∀x(NatNum(x) → P(x))

is a logical consequence of the infinite set S of sentences

P(0)
P(1)
P(2)
.
.
.

However, the universal quantification is not a ⊢_N-consequence of the set S. The reason why is that the ⊢_N-consequence relation is compact: for any sentence X and set K of sentences, X is a ⊢_N-consequence of K, if and only if X is a ⊢_N-consequence of some finite subset of K. Proofs in N are objects of finite length; a deduction is a finite sequence of sentences. Since the universal quantification is not a ⊢_N-consequence of any finite subset of S, it is not a ⊢_N-consequence of S. By the completeness of system N, it follows that

∀x(NatNum(x) → P(x))

is not a ⊨-consequence of S either. Consider the structure U* whose domain is the set of McKeons. Let all numerals name Beth. Let the extension of ‘NatNum’ be the entire domain, and the extension of ‘P’ be just Beth. Then each element of S is true in U*, but ‘∀x (NatNum(x) → P(x))’ is not true in U*. (See Logical Consequence, Model-Theoretic Conceptions for further discussion of structures.) Note that the sentences in S only say that P holds for 0, 1, 2, and so on, and not also that 0,1, 2, etc., are all the elements of the domain of discourse. The above interpretation takes advantage of this fact by reinterpreting all numerals as names for Beth.

However, we can reflect model-theoretically the intuition that ‘∀x(NatNum(x) → P(x))’ is a logical consequence of set S by doing one of two things. We can add to S the functional equivalent of the claim that 1, 2, 3, etc., are all the natural numbers there are on the basis that this is an implicit assumption of the view that the universal quantification follows from S. Or we could add ‘NatNum’ and all numerals to our list of logical terms. On either option it still won’t be the case that ‘∀x(NatNum(x) → P(x))’ is a ⊢_N-consequence of the set S. There is no way to accommodate the intuition that ‘∀x(NatNum(x) → P(x))’ is a logical consequence of S in terms of a compact consequence relation. Tarski takes this to be a reason to think that the model-theoretic account of logical consequence is definitive as opposed to an account of logical consequence in terms of a compact consequence relation such as ⊢_N.

Tarski’s illustration shows that what is called the ω-rule is a correct inference rule.

The ω-rule is that from:

{P(0), P(1), P(2), …}

one may infer

∀x(NatNum(x) → P(x))

with respect to any predicate P. Any inference guided by this rule is correct even though it can’t be represented in a deductive system as this notion has been used here and discussed in Logical Consequence, Philosophical Considerations.

Compactness is not a salient feature of logical consequence conceived deductive theoretically. This suggests, by the third criterion of a successful theoretical definition of logical consequence mentioned in Logical Consequence, Philosophical Considerations, that no compact consequence relation is definitive of the intuitive notion of deducibility. So, assuming that deductive system N is correct (that is, deducibility is co-extensive in M with the ⊢_N-relation), we can’t treat

X is intuitively deducible from K if and only if K ⊢_N X.

as a definition of deducibility in M since

X is a deductive consequence of K if and only if X is deducible in a correct deductive system from K.

is not true with respect to languages for which deducibility is not captured by any compact consequence relation (that is, not captured by any deduction-system account of it ). Some (e.g., Quine) demur using a language for purposes of science in which deducibility is not completely represented by a deduction-system account because of epistemological considerations. Nevertheless, as Tarski (1936) argues, the fact that there cannot be deduction-system accounts of some intuitively correct principles of inference is reason for taking a model-theoretic characterization of logical consequence to be more fundamental than any characterization in terms of a deductive system sound and complete with respect to the model-theoretic characterization.

b. Is deductive system N correct?

In discussing the status of the characterization of logical consequence in terms of deductive system N, we assumed that N is correct. The question arises whether N is, indeed, correct. That is, is it the case that X is intuitively deducible from K if and only if K ⊢_N X? The biconditional holds only if both (1) and (2) are true.

(1) If sentence X is intuitively deducible from set K of sentences, then K ⊢_N X.
(2) If K ⊢_N X, then sentence X is intuitively deducible from set K of sentences.

So N is incorrect if either (1) or (2) is false. The truth of (1) and (2) is relevant to the correctness of the characterization of logical consequence in terms of system N, because any adequate deductive-theoretic characterization of logical consequence must identify the logical terms of the relevant language and account for their inferential properties (for discussion, see Logical Consequence, Philosophical Considerations: Section 4). (1) is false if the list of logical terms in M is incomplete. In such a case, there will be a sentence X and set K of sentences such that X is intuitively deducible from set K because of at least one inferential property of logical terminology unaccounted for by N and so false that K ⊢_N X (for discussion of some of the issues surrounding what qualifies as a logical term see Logical Consequence, Model-theoretic Conceptions: Section 5.3). In this case, N would be incorrect because it wouldn’t completely account for the inferential machinery of language M. (2) is false if there are deductions in N that are intuitively incorrect. Are there such deductions? In order to fine-tune the question note that the sentential connectives, the identity symbol, and the quantifiers of M are intended to correspond to or, and, not, if…then (the indicative conditional), is identical with, some, and all. Hence, N is a correct deductive system only if the Intro and Elim rules of N reflect the inferential properties of the ordinary language expressions. In what follows, we sketch three views that are critical of the correctness of system N because they reject (2).

i. Relevance logic

Not everybody accepts it as a fact that any sentence is deducible from a contradiction, and so some question the correctness of the ⊥-Elim rule. Consider the following informal proof of Q from P & ~P, for sentences P and Q, as a rationale for the ⊥-Elim rule.

From (1) P and not-P, we may correctly infer (2) P, from which it is correct to infer (3) P or Q. We derive (4) not-P from (1). (5) P follows from (3) and (4).

The proof seems to be composed of valid modes of inference. Critics of the ⊥-Elim rule are obliged to tell us where it goes wrong. Here we follow the relevance logicians Anderson and Belnap (1962, pp.105-108; for discussion, see Read 1995, pp. 54-60). In a nutshell, Anderson and Belnap claim that the proof is defective because it commits a fallacy of equivocation. The move from (2) to (3) is correct only if or has the sense of at least one. For example, from Kelly is female it is legit to infer that at least one of the two sentences Kelly is female and Kelly is older than Paige is true. On this sense of or given that Kelly is female, one may infer that Kelly is female or whatever you like. However, in order for the passage from (3) and (4) to (5) to be legitimate the sense of or in (3) is if not-…then. For example from if Kelly is not female, then Kelly is not Paige’s sister and Kelly is not female it is correct to infer Kelly is not Paige’s sister. Hence, the above “support” for the ⊥-Elim rule is defective for it equivocates on the meaning of or.

Two things to highlight. First, Anderson and Belnap think that the inference from (2) to (3) on the if not-…then reading of or is incorrect. Given that Kelly is female it is problematic to deduce that if she is not then Kelly is older than Paige—or whatever you like. Such an inference commits a fallacy of relevance for Kelly not being female is not relevant to her being older than Paige. The representation of this inference in system N appeals to the ⊥-Elim rule, which is rejected by Anderson and Belnap. Second, the principle of inference underlying the move from (3) and (4) to (5)—from P or Q and not-P to infer Q—is called the principle of the disjunctive syllogism. Anderson and Belnap claim that this principle is not generally valid when or has the sense of at least one, which it has when it is rendered by ‘v‘ (e.g., see above). If Q is relevant to P, then the principle holds on this reading of or.

It is worthwhile to note the essentially informal nature of the debate. It calls upon our pre-theoretic intuitions about correct inference. It would be quite useless to cite the proof in N of the validity of disjunctive syllogism (given above) against Anderson and Belnap for it relies on the ⊥-Elim rule whose legitimacy is in question. No doubt, pre-theoretical notions and original intuitions must be refined and shaped somewhat by theory. Our pre-theoretic notion of correct deductive reasoning in ordinary language is not completely determinant and precise independently of the resources of a full or partial logic. (See Shapiro 1991, chaps. 1 and 2 for discussion of the interplay between theory and pre-theoretic notions and intuitions.) Nevertheless, hardcore intuitions regarding correct deductive reasoning do seem to drive the debate over the legitimacy of deductive systems such as N and over the legitimacy of the ⊥-Elim rule in particular. Anderson and Belnap (1962, p. 108) write that denying the principle of the disjunctive syllogism, regarded as a valid mode of inference since Aristotle, “… will seem hopelessly naïve to those logicians whose logical intuitions have been numbed through hearing and repeating the logicians fairy tales of the past half century, and hence stand in need of further support”. The possibility that intuitions in support of the general validity of the principle of the disjunctive syllogism have been shaped by a bad theory of inference is motive enough to consider argumentative support for the principle and to investigate deductive systems for relevance logic.

A natural deductive system for relevance logic has the means for tracking the relevance quotient of the steps used in a proof and allows the application of an introduction rule in the step from A to B “only when A is relevant to B in the sense that A is used in arriving at B” (Anderson and Belnap 1962, p. 90). Consider the following proof in system N.

	1.		Admires(evan, paige)		Basis
			2.	~Married(beth, matt)	Assumption
			3.	Admires(evan, paige)	Reit: 1
	4.		(~Married(beth, matt) → Admires(evan, paige))		→-Intro: 2-3

Recall that the rationale behind the →-Intro rule is that we may derive a conditional if we derive the consequent Q from the assumption of the antecedent P, and, perhaps, other sentences occurring earlier in the proof on wider proof margins. The defect of this rule, according to Anderson and Belnap is that “from” in “from the assumption of the antecedent P” is not taken seriously. They seem to have a point. By the lights of the → -Intro rule, we have derived line 4 but it is hard to see how we have derived the sentence at line 3 from the assumption at step 2 when we have simply reiterated the basis at line 3. Clearly, ‘~Married(beth, matt)’ was not used in inferring ‘Admires(evan, beth)’ at line 3. The relevance logician claims that the →-Intro rule in a correct natural deductive system should not make it possible to prove a conditional when the consequent was arrived at independently of the antecedent. A typical strategy is to use classes of numerals to mark the relevance conditions of basis sentences and assumptions and formulate the Intro and Elim rules to tell us how an application of the rule transfers the numerical subscript(s) from the sentences used to the sentence derived with the help of the rule. Label the basis sentences, if any, with distinct numerical subscripts. Let a, b, c, etc., range over classes of numerals. The →-rules for a relevance natural deductive system may be represented as follows.

→-Elim

	k.	(P → Q)a
	l.	Pb
	m.	Qa∪b	→-Elim: k, l

→-Intro

			k.	P{k}	Assumption
				.
				.
				.
			m.	Qb
	n.		(P → Q)b – {k}		→-Intro: k-m, provided k∈b
			The numerical subscript of the assumption at line k must be new to the proof. This is insured by using the line number for the subscript.

In the directions for the →-Intro rule, the proviso that k∈b insures that the antecedent P is used in deriving the consequent Q. Anderson and Belnap require that if the line that results from the application of either rule is the conclusion of the proof the relevance markers be discharged. Here is a sample proof of the above two rules in action.

			1.		Admires(evan, paige)1		Assumption
					2.	(Admires(evan, paige) → ~Married(beth, matt))2	Assumption
					3.	~Married(beth, matt)1, 2	→-Elim: 1,2
			4.		((Admires(evan, paige) → ~Married(beth, matt)) → ~Married(beth, matt))1		→-Intro: 2-3
	5.		(Admires(evan, paige) → ((Admires(evan, paige) → ~Married(beth, matt)) → ~Married(beth, matt)))				→-Intro: 1-4

For further discussion see Anderson and Belnap (1962). For a comprehensive discussion of relevance deductive systems see their (1975). For a more up-to-date review of the relevance logic literature see Dunn (1986).

ii. Intuitionistic logic

We now consider the correctness of the ~-Elim rule and consider the rule in the context of using it along with the ~-Intro rule.

~-Intro

			k.	P	Assumption
				.
				.
				.
			m.	⊥
	n.		~P		~-Intro: k-m

~-Elim

	k.	~~P
	m.	P	~-Elim: k

Here is a typical use in classical logic of the ~-Intro and ~-Elim rules. Suppose that we derive a contradiction from the assumption that a sentence P is true. So, if P were true, then a contradiction would be true which is impossible. So P cannot be true and we may infer that not-P. Similarily, suppose that we derive a contradiction from the assumption that not-P. Since a contradiction cannot be true, not-P is not true. Then we may infer that P is true by ~-Elim.

The intuitionist logician rejects the reasoning given in bold. If a contradiction is derived from not-P we may infer that not-P is not true, that is, that not-not-P is true, but it is incorrect to infer that P is true. Why? Because the intuitionist rejects the presupposition behind the ~-Elim rule, which is that for any proposition P there are two alternatives: P and not-P. The grounds for this are the intuitionistic conceptions of truth and meaning.

According to intuitionistic logic, truth is an epistemic notion: the truth of a sentence P consists of our ability to verify it. To assert P is to have a proof of P, and to assert not-P is to have a refutation of P. This leads to an epistemic conception of the meaning of logical constants. The meaning of a logical constant is characterized in terms of its contribution to the criteria of proof for the sentences in which it occurs. Compare with classical logic: the meaning of a logical constant is semantically characterized in terms of its contribution to the determination of the truth conditions of the sentences in which it occurs. For example, the classical logician accepts a sentence of the form P v Q only when she accepts that at least one of the disjuncts is true. On the other hand, the intuitionistic logician accepts P v Q only when she has a method for proving P or a method for proving Q. But then the Law of Excluded Middle no longer holds, because a sentence of the form P or not-P is true, that is assertible, only when we are in a position to prove or refute P, and we lack the means for verifying or refuting all sentences. The alleged problem with the ~-Elim rule is that it illegitimately extends the grounds for asserting P on the basis of not-not-P since a refutation of not-P is not ipso facto a proof of P.

Since there are finitely many McKeons and the predicates of language M seem well defined, we can work through the domain of the McKeons to verify or refute any M-sentence and so there doesn’t seem to be an M-sentence that is neither verifiable nor refutable. However, consider a language about the natural numbers. Any sentence that results by substituting numerals for the variables in ‘x = y + z’ is decidable. This is to say that for any natural numbers x, y, and z, we have an effective procedure for determining whether or not x is the sum of y and z. Hence, for all x, y, and z either we may assert that x = y + z or we may assert the contrary. Let ‘A(x)’ abbreviate ‘if x is even and greater than 2 then there exists primes y and z such that x = y + z’. Since there are algorithms for determining of any number whether or not it is even, greater than 2, or prime, the hypothesis that the open formula ‘A(x)’ is satisfied by a given natural number is decidable for we can effectively determine for all smaller numbers whether or not they are prime. However, there is no known method for verifying or refuting Goldbach’s conjecture, for all x, A(x). Even though, for each numeral n standing for a natural number, the sentence A(n) is decidable (that is, we can determine which of A(n) or not-A(n) is true), the sentence ‘for all x, A(x)’ is not. That is, we are not in a position to hold that either Goldbach’s conjecture is true or that it is not. Clearly, verification of the conjecture via an exhaustive search of the domain of natural numbers is not possible since the domain is non-finite. Minus a counterexample or proof of Goldbach’s conjecture, the intuitionist demurs from asserting that either Goldbach’s conjecture is true or it is not. This is just one of many examples where the intuitionist thinks that the law of excluded middle fails.

In sum, the legitimacy of the ~-Elim rule requires a realist conception of truth as verification transcendent. On this conception, sentences have truth-values independently of the possibility of a method for verifying them. Intuitionistic logic abandons this conception of truth in favor of an epistemic conception according to which the truth of a sentence turns on our ability to verify it. Hence, the inference rules of an intuitionistic natural deductive system must be coded in such a way to reflect this notion of truth. For example, consider an intuitionistic language in which a, b, … range over proofs, ‘a: P’ stands for ‘a is a proof of P’, and ‘(a, b)’ stands for some suitable pairing of the proofs a and b. The &-rules of an intuitionistic natural deductive system may look like the following:

&-Intro

	k.	a: P
	l.	b: Q
	m.	(a, b): (P & Q)	&-Intro: k, l

&-Elim

	k.	(a, b): (P & Q)		& nbsp;		k.	(a, b): (P & Q)
	m.	a: P	&-Elim: k			m.	b: Q	&-Elim: k

Apart from the negation rules, it is fairly straightforward to dress the Intro and Elim rules of N with a proof interpretation as is illustrated above with the &-rules. For the details see Van Dalen (1999). For further introductory discussion of the philosophical theses underlying intuitionistic logic see Read (1995) and Shapiro (2000). Tennant (1997) offers a more comprehensive discussion and defense of the philosophy of language underlying intuitionistic logic.

iii. Free Logic

We now turn to the ∃-Intro and ∀-Elim rules. Consider the following two inferences.

	(1)	Male(evan)			(3)	∀x Male(x)
(therefore)	(2)	∃x Male(x)		(therefore)	(4)	Male(evan)

Both are correct by the lights of our system N. Specifically, (2) is derivable from (1) by the ∃-Intro rule and we get (4) from (3) by the ∀-Elim rule. Note an implicit assumption required for the legitimacy of these inferences: every individual constant refers to an element of the quantifier domain. If this existence assumption, which is built into the semantics for M and reflected in the two quantifier rules, is rejected, then the inferences are unacceptable. What motivates rejecting the existence assumption and denying the correctness of the above inferences?

There are contexts in which singular terms are used without assuming that they refer to existing objects. For example, it is perfectly reasonable to regard the individual constants of a language used to talk about myths and fairy tales as not denoting existing objects. It seems inappropriate to infer that some actually existing individual is jolly on the basis that the sentence Santa Claus is jolly is true. Also, the logic of a language used to debate the existence of God should not presuppose that God refers to something in the world. The atheist doesn’t seem to be contradicting herself in asserting that God does not exist. Furthermore, there are contexts in science where introducing an individual constant for an allegedly existing object such as a planet or particle should not require the scientist to know that the purported object to which the term allegedly refers actually exists. A logic that allows non-denoting individual constants (terms that do not refer to existing things) while maintaining the existential import of the quantifiers (‘∀x’ and ‘∃x’ mean something like ‘for all existing individuals x’ and ‘for some existing individuals x’, respectively) is called a free logic. In order for the above two inferences to be correct by the lights of free logic, the sentence Evan exists must be added to the basis. Correspondingly, the ∃-Intro and ∀-Elim rules in a natural deductive system for free logic may be portrayed as follows. Again, let Ωv be a formula in which v is the only free variable, and let n be any name.

		∀-Elim					∃-Intro
	k.	∀vΩv				k.	Ωn
	l.	E!n				l.	E!n
	m.	Ωn	∀-Elim: k, l			m.	∃vΩv	∃-Intro: k, l

E!n abbreviates n exists and so we suppose that ‘E!’ is an item of the relevant language. The ∀-Intro and ∃-Elim rules in a free logic deductive system also make explicit the required existential presuppositions with respect to individual constants (for details see Bencivenga 1986, p. 387). Free logic seems to be a useful tool for representing and evaluating reasoning in contexts such as the above. Different types of free logic arise depending on whether we treat terms that do not denote existing individuals as denoting objects that do not actually exist or as simply not denoting at all.

In sum, there are contexts in which it is appropriate to use languages whose vocabulary and syntactic formation rules are independent of our knowledge of the actual existence of the entities the language is about. In such languages, the quantifier rules of deductive system N sanction incorrect inferences, and so at best N represents correct deductive reasoning in languages for which the existential presupposition with respect to singular terms makes sense. The proponent of system N may argue that only those expressions guaranteed a referent (e.g., demonstratives) are truly singular terms. On this view, advocated by Bertrand Russell at one time, expressions that may not have a referent such as Santa Claus, God, Evan, Bill Clinton, the child abused by Michael Jackson are not genuinely singular expressions. For example, in the sentence Evan is male, Evan abbreviates a unique description such as the son of Matt and Beth. Then Evan is male comes to

There exists a unique x such that x is a son of Matt and Beth and x is male.

From this we may correctly infer that some are male. The representation of this inference in N appeals to both the ∃-Intro and &exists;-Elim rules, as well as the &-Elim rule. However, treating most singular expressions as disguised definite descriptions at worst generates counter-intuitive truth-value assignments (Santa Claus is jolly turns out false since there is no Santa Claus) and seems at best an unnatural response to the criticism posed from the vantagepoint of free logic.

For a short discussion of the motives behind free logic and a review of the family of free logics see Read (1995, chap. 5). For a more comprehensive discussion and a survey of the relevant literature see Bencivenga (1986). Morscher and Hieke (2001) is a collection of recent essays devoted to taking stock of the past fifty years of research in free logic and outlining new directions.

6. Conclusion

This completes our discussion of the deductive-theoretic conception of logical consequence. Since, arguably, logical consequence conceived deductive-theoretically is not compact it cannot be defined in terms of deducibility in a correct deductive system. Nevertheless correct deductive systems are useful for modeling deductive reasoning and they have applications in areas such as computer science and mathematics. Is deductive system N correct? In other words: Do the Intro and Elim rules of N represent correct principles of inference? We sketched three motives for answering in the negative, each leading to a logic that differs from the classical one developed here and which requires altering Intro and Elim rules of N. It is clear from the discussion that any full coverage of the topic would have to engage philosophical issues, still a matter of debate, such as the nature of truth, meaning and inference. For a comprehensive and very readable survey of proposed revisions to classical logic (those discussed here and others) see Haack (1996). For discussion of related issues, see also the entries, “Logical Consequence, Philosophical Considerations” and “Logical Consequence, Model-Theoretic Conceptions” in this encyclopedia.

7. References and Further Reading

• Anderson, A.R. and N. Belnap (1962): “Entailment”, pp. 76-110 in Logic and Philosophy, ed. G. Iseminger. New York: Appleton-Century-Crofts, 1968.
• Anderson, A.R., and N. Belnap (1975): Entailment: The Logic of Relevance and Necessity. Princeton: Princeton University Press.
• Barwise, J. and J. Etchemendy (2001): Language, Proof and Logic. Chicago: University of Chicago Press and CSLI Publications.
• Bencivenga, E. (1986): “Free logics”, pp. 373-426 in Gabbay and Geunthner (1986).
• Dunn, M. (1986): “Relevance Logic and Entailment”, pp. 117-224 in Gabbay and Geunthner (1986).
• Fitch, F.B. (1952): Symbolic Logic: An Introduction. New York: The Ronald Press.
• Gabbay, D. and F. Guenthner, eds. (1983): Handbook of Philosophical Logic, Vol 1. Dordrecht: D. Reidel.
• Gabbay, D. and F. Guenthner, eds. (1986): Handbook of Philosophical Logic, Vol. 3. Dordrecht: D. Reidel.
• Gentzen, G. (1934): “Investigations Into Logical Deduction”, pp. 68-128 in Collected Papers, ed. M.E. Szabo. Amsterdam: North-Holland, 1969.
• Haack, S. (1978): Philosophy of Logics. Cambridge: Cambridge University Press.
• Haack, S. (1996): Deviant Logic, Fuzzy Logic. Chicago: The University of Chicago Press.
• Morscher E. and A. Hieke, eds. (2001): New Essays in Free Logic: In Honour of Karel Lambert, Dordrecht: Kluwer.
• Pelletier, F.J. (1999): “A History of Natural Deduction and Elementary Logic Textbooks”, pp.105-138 in Logical Consequence: Rival Approaches, ed. J. Woods and B. Brown. Oxford: Hermes Science Publishing, 2001.
• Read, S. (1995): Thinking About Logic. Oxford: Oxford University Press.
• Shapiro, S. (1991): Foundations without Foundationalism: A Case For Second-Order Logic. Oxford: Clarendon Press.
• Shapiro, S. (2000): Thinking About Mathematics. Oxford: Oxford University Press.
• Sundholm, G. (1983): “Systems of Deduction”, in Gabbay and Guenthner (1983).
• Tarski, A. (1936): “On the Concept of Logical Consequence”, pp. 409-420 in Tarski (1983).
• Tarski, A. (1983): Logic, Semantics, Metamathematics, 2nd ed. Indianapolis: Hackett Publishing.
• Tennant, N. (1997): The Taming of the True. Oxford: Clarendon Press.
• Van Dalen, D. (1999): “The Intuitionistic Conception of Logic”, pp. 45-73 in Varzi (1999).
• Varzi, A., ed. (1999): European Review of Philosophy, Vol. 4, The Nature of Logic, Stanford: CSLI Publications.

Author Information

Matthew McKeon
Email: mckeonm@msu.edu
Michigan State University
U. S. A.