When is a disjunctive wff true

If is a non-primitive constant of the language, then typically it will be introduced by an abbreviative definition. In presentations of classical systems in which the conditional constant or and the negational constant are taken as primitive, the disjunctive constant might be introduced in the abbreviation of a wff or as.

Intuitively, the former would correspond to a rule of conversation that permitted us to assert A or B for any B given the assertion that A. Thus if we are told that Nicholas is in Paris, we can infer that Nicholas is either in Paris or in Toulouse.

Intuitively, the latter rule would correspond to a rule that, given the assertion that A or B , would permit the assertion of anything that is permitted both by the assertion of A and by the assertion of B. For example, given the assertion on certain grounds that Nicholas is in Paris or Toulouse, we are warranted in asserting on the same grounds plus some geographical information, that Nicholas is in France, since that assertion is warranted a by the assertion that Nicholas is in Paris together with some of the geographical information and b by the assertion that Nicholas is in Toulouse together with the rest of the geographical information.

More generally we may sum the matter up by saying that the rule corresponds to the conversational rule that lets us extract information from an or -sentence without the information of either of its clauses. In the example, we are given the information that Nicholas is in Paris or Toulouse, but we are given neither the information that Nicholas is in Paris nor the information that he is in Toulouse.

Now the truth-definition can be regarded as an extension of the valuation from the atoms of the language to the entire set of wffs with 1 understood as the truth-value, true, and 0 understood as the truth-value, false. The tabulated graph of this function, as dictated by the truth-definition, is called the truth-table for disjunction. That table is the following:. This truth-function is referred to variously as exclusive disjunction, as disjunction after the succession of values in its main column , and as logical difference.

The wff is true when exactly one of , is true; false otherwise. To make matters explicit, the earlier discussed truth-function is called inclusive, or non-exclusive or disjunction.

The fact that English or is not binary does not accord so well with the claim made by many textbook authors that there are uses of or that require representation by disjunction.

To be sure, is associative, so that a notational liberalization would be possible, parallel to the one described for. But, as Hans Reichenbach seems first to have pointed out in Reichenbach [] , the truth-definition for 1 , The truth-definition as given by the table requires that exactly one of , has the value 1.

Let have the value 1; then has the value 0. Then and have the same value. That is, either both and have the value 0, or both and have the value 1. In the former case exactly one of , , has the value 1; in the latter, all three have the value 1. That is, the disjunction will take the value 1 if and only if an odd number of disjuncts have the value 1. A simple induction will prove that this result holds for an exclusive disjunction of any finite length.

Now there is no naturally occurring coordinator in any natural language matching the truth-conditional profile of such a connective. There is certainly no use of or in English in accordance with which five sentences A , B , C , D , and E can be joined to form a sentence A or B or C or D or E , which is true if and only if either exactly one of the component sentences is true, or exactly three of them are true or exactly five of them are true.

Most of the texts make no claims about exclusive disjunctive uses of either English or Latin or -words beyond the two-disjunct case. But it is a fair presumption that the belief in exclusive disjunctive uses of or in English includes just such three-disjunct uses of or. Such a use of or , would be one in accordance with which three sentences A , B , and C can be joined to form a sentence A or B or C , which is true if and only if exactly one of the component sentences is true.

Though not a disjunctive use of or , this would be a general use representable as disjunction in the two-disjunct case. The question as to whether there is such a use of or in English, or any other natural language goes to the very heart of the conception of truth conditional semantics. However, we can see that it is when we consider its truth table:. 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. 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.

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. 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.

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. 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. 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. We can test the validity of this argument by constructing a combined truth table for all three statements. 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:. 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. 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.

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. The validity of this argument can be made more obvious by representing the chain of reasoning leading from the premises to the conclusion:.

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. 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 The system makes use of the language PL. 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.

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.

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. 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.

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:.

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:. This argument has six distinct statement letters, and hence constructing a truth table for it would require 64 rows.

Happily, the derivation of the conclusion of the premises using our inference and replacement rules, while far from simple, is relatively less exhausting:. 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. This is done by constructing a sub-derivation within a derivation in which the antecedent of the conditional is assumed as a hypothesis.

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.

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. 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.

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. 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.

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. 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 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.

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. Note that according to this definition, every wff of the form is an axiom. 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. 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.

Whatever happens to be, there will be a derivation in PC of the same form:. Hence, we call a theorem schema of PC, because all of its instances are theorems of PC. 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!

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. 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. 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:. To such a system it would be necessary to add an additional inference rule , a rule of substitution or uniform replacement.

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. 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. Meredith , 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. 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 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. 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.

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.

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. 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.

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. Let us suppose instead that is contingent.

Let us construct a wff in the following way. 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. 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. Metatheoretic result 2 a. 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. 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.

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. 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. 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. 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. This may be much clearer with an example. Consider the following derivation for the result that :. It is possible to transform the above derivation into one that uses no premises and that shows that is a theorem of PC.

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:. 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. 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. 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. 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. 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. 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.

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.

Suppose that is a tautology. This means that every possible truth-value assignment to its statement letters makes it true. 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.

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. 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. 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. 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.

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. There are eight possible truth-value assignments to these letters, and since is a tautology, all of them make true.

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:. 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. Corollary 4. 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.

Above, we saw that all tautologies are theorems of PC.