Semiformal proof in predicate logic,
Greek Knuckleballs and Lucky Charms:
some metaphors and notation for dealing with quantifiers

Steve Grantham

Department of Mathematics and Computer Science
Boise State University
June 25, 1996


The traditional practice in the teaching of proof techniques has been to couple formality of proof with that of notation: very formal proof is emphasized within the domain of predicate logic, while less formal techniques are typically taught in more familiar, concrete mathematical contexts. In this paper I advocate teaching ``semiformal proof" within the austere and self-contained setting of predicate logic, and I propose several metaphors and notational conventions intended to help students understand the role of universal and existential quantifiers in those proofs. These ideas are illustrated with a couple of representative examples of the type of proof I have in mind.

1 Introduction

I will assume as an axiom that it is desirable for students to learn how to construct well written, logically correct mathematical proofs. The purpose of this paper is to suggest some possible ways to proceed towards that goal.

One question which should be addressed at the outset is the level of formality we have in mind for these proofs. Ideally, we would like students to be able to construct proofs at a variety of such levels---from very sketchy and intuitive outlines to strictly formal derivations---and to be able to move among these various levels with ease and confidence. This is a tall order, however, and my primary focus here will be on the broad ``middle range" of formality and rigor that is characteristic of ``everyday mathematics."

This is difficult to define precisely, but what I have in mind is the type of proof that most mathematicians would consider complete and rigorous, but that is not strictly formal in the sense of being a purely syntactical derivation using a very precise and circumscribed set of rules of inference. In other words, I have in mind the type of proof found in a typical textbook in algebra, analysis, number theory, etc. I will call proofs of this type ``semiformal." Although strictly formal methods certainly have their place, I believe that it is difficult for students to understand or appreciate them without first developing an intuitive feel by mastering the basics of proof at the semiformal level.

My impression is that the preponderance of current practice in teaching basic proof techniques may be characterized as follows: semiformal proof is usually taught within some specific, familiar mathematical context (for example number theory, calculus, geometry, ...), while more formal methods are taught within the more austere arena of pure logic. While both these approaches have their merits, they also have some drawbacks.

The main problem with learning about proof techniques within a familiar mathematical context stems from that very familiarity: many students encounter a fundamental difficulty in trying to differentiate clearly between what they know---that is, which ``facts" they are allowed to assume and use in their proofs---and what they are required to prove. Students' initial exposure to the basic concepts and facts in these areas often has come via a pedagogical approach that does not emphasize (or perhaps even mention) logical structure. Consequently, the statements they are asked to prove often may seem to them as obvious (or more so) as the ones they are allowed to use!

The main problem with formal proof in the setting of pure logic is the length and tedium involved in proofs of even simple and obvious results by these methods. This precludes tackling examples with much intrinsic interest or complexity. The proofs typically attacked in this sort of setting are rarely much more complex than, say, proving Socrates' mortality from the premises that he is a man and that all men are mortal. Although such examples may help students to understand formal syntax and rules, they do little to develop their intuition and ability to derive less obvious conclusions from more complex premises.

What I would like to advocate here is a hybrid of these two approaches: semiformal proof in the setting of predicate logic. My belief is that this hybrid approach can help prepare students both for semiformal proofs in more specific mathematical contexts, and for more formal proof techniques. The main advantage of this approach is that in such a setting, the predicates used are unencumbered by any preconceived interpretation, and all premises to be used in a proof must be given explicitly. Hence there should be no question in the student's mind as to what is known and what must be proved.

There are tradeoffs, of course---the more concrete contexts provide the advantage of comforting familiarity and some intuition as to where to start and how to proceed. And ultimately we do want students to develop the ability to identify implicit assumptions and to distinguish between what they may assume and what must be proved. But for purposes of understanding the core elements of the logical structure of proof, the setting of predicate logic offers some distinct advantages.

2 The Notion of Semiformal Proof in Predicate Logic

In order to illustrate more precisely the type of problem I have in mind when advocating teaching semiformal proof in the setting of predicate logic, let us look at a couple of examples. We use standard logical notation.

Example 2.1 Consider the following list of premises:

A_1: for all x ([for all y T(x,y)] OR [there exists z R(x,z)])
A_2: there exists x for all y for all z [R(y,z) IMPLIES P(x,y)]
A_3: for all x there exists y Q(x,y)
A_4: for all x for all y for all z ([P(x,z) AND Q(x,y)] IMPLIES T(z,x))

Determine whether the conclusion

B: there exists a for all b T(b,a)

follows from the premises A_1--A_4.

Example 2.2 Consider the following list of premises:

P_1: there exists x for all y T(y,x)
P_2: for all x (A(x) IMPLIES R(x,x))
P_3: for all x (B(x) IMPLIES there exists y S(y,x))
P_4: for all x for all y ( [S(x,y) AND NOT A(y)] IMPLIES R(y,x))
P_5: for all x for all y ( T(x,y) IMPLIES [A(x) OR B(x) OR R(x,y)] )

Determine whether or not each of the conclusions

Q_1: for all x there exists y R(x,y)
Q_2: for all x there exists y R(y,x)

follows from the premises P_1--P_5.

Clearly these examples are considerably more complex than the canonical ``Socrates is mortal" type of example mentioned earlier, and strictly formal proofs would be very tedious in these cases. However, it is certainly within the abilities of many college freshmen or sophomores to come up with the type of semiformal proofs (or counterexamples) that I have in mind. There are no hidden assumptions: all premises are clearly laid out, and the various predicates involved have no ``meaning" beyond that which the premises give them. This lack of extraneous or distracting details allows us to focus our attention on logical structure, and in particular on techniques for dealing with quantifiers.

The first step in getting students to understand the structure of proofs is to make sure that they understand what it means to say that a conclusion does (or does not) follow from a certain set of premises. In particular, it is important for them to realize that a ``meta-universal quantifier" and a ``meta-implication" are involved in the assertion that the conclusion does follow: for every interpretation, if all of the premises are true in that interpretation (i.e., if the interpretation is a model of the premises), then the conclusion also must be true. [This is one feature that tends to distinguish examples in this setting from many of the ones traditionally used when proofs are discussed in more familiar, concrete mathematical contexts: in the latter case, there is often only one ``model" under consideration, and the premises (many or all of which may be implicit) are in fact true in that model, so it is simply a matter of proving that the conclusion holds (or fails) in that single model.]

Likewise, students must understand that the assertion that the potential conclusion does not follow from the premises involves a ``meta-existential quantifier" (and a ``meta-conjunction"): there exists at least one interpretation in which the premises are all true but the conclusion fails.

Understanding even these simple points is a challenge for many students; when we lay out the premises and the conclusion explicitly, it makes it easier to focus attention on these issues. It certainly helps if the students have already been exposed to the general concepts of logical validity and logical entailment earlier in the course, before tackling proofs per se}.

Before proceeding to a detailed discussion of general principles and notation for attacking problems of the type given above, a few words are in order about the use of visual aids in understanding statements of predicate logic. In the examples above, all predicates are either unary or binary; while there is nothing that precludes dealing with predicates of higher ``-arity," the fundamental principles and techniques of proof can certainly be developed quite sufficiently using only unary and binary predicates. It is natural to use a combination of Venn diagrams and digraphs to represent such predicates visually. That is, the objects in a universe of discourse can be represented as points or vertices; unary predicates can be represented by ``Venn blobs" (i.e., circles etc.) which contain those objects having the specified property; and binary predicates can be represented by directed arrows from one vertex to another (or from a vertex to itself). (If we have more than one binary predicate, then we will want somehow to distinguish among various types of arrows, either by labeling the arrows with the name of the predicate, or by using different colors or ``styles" of arrows.) Let's assume that the students are already familiar with this method of representing unary and binary predicates by the time they begin to grapple with proofs.

In particular, it will generally be helpful, as a first step in understanding a problem of the type given above, to rephrase and sketch both the premises and the potential conclusion in terms of the visual aids just mentioned. For instance, in Example~\ref{example_1 the premises may be translated as follows:

A_1 says that each vertex either sends T-arrows to every vertex, or sends an R-arrow to at least one vertex.

A_2 says that there is a single vertex which sends a P-arrow to the ``tail vertex" of every R-arrow.

A_3 says that every vertex sends at least one Q-arrow.

A_4 says that whenever a vertex x sends out both a P-arrow and a Q-arrow, it receives a T-arrow from the vertex to which it sends the P-arrow.

We can illustrate each of these premises with one or more sketches, so long as we keep in mind that the sketches we draw constitute only a partial picture of what any interpretation satisfying the premises must look like. It is important for students to understand that coming up with a single picture that incorporates all these sketches into a consistent whole is tantamount to constructing a model satisfying all the premises---and that, although it is important to be able to do this, there will generally be many different such models. It is equally important for them to understand that we cannot prove that the conclusion follows in general simply by examining a few such models (unless those few are the only ones, which we would need to verify), but that if the conclusion does not follow then it does suffice to find single appropriate model which serves as a counterexample.

Likewise, the potential conclusion in Example 2.1 may be translated as:

There is a single vertex which receives T-arrows from every vertex (including itself).

Again, we can draw a picture which illustrates this situation, but it is important for the student to understand that our goal is to determine whether or not the configuration represented by this picture is forced to occur in any interpretation satisfying the premises.

Now that we have seen a couple of brief examples of the type of problem to be considered, let us proceed to a discussion of general principles for dealing with quantifiers. Of course, these examples will also involve the logical connectives (conjunction, disjunction, negation, implication, biconditional, etc.), and there are some issues involved in learning to deal with them correctly, but they tend to be less problematic and will not be the main focus of our discussion, In the approach I have in mind, (and that I have used in the classroom) students would already have tackled similar problems within the more restricted domain of propositional logic, where the focus is exclusively on the logical connectives, before taking on the more challenging topic of proof in predicate logic.

We will organize our discussion of the major issues involved in dealing with quantifiers as follows:

In the next four sections, we will deal with these questions in the order just given; the discussion will be phrased in a way intended to be reasonably accessible and self-explanatory to the typical student.

Our answers to these four questions---in particular, the first two---will involve the two notational conventions mentioned in the title of this paper. The main idea behind these conventions is that our proofs will involve introducing names for objects in the universe of discourse, and these objects will fall into two categories: ``arbitrary" and ``special." Instead of denoting these objects (whether arbitrary or special) by the same symbols (x, y, z, etc.) that we use as formal (usually quantified) variables in our premises and conclusions, we will use some different symbols. There are two reasons for this. The first is simply to reduce the chances of confusion and name conflict that could occur if we use the same type of symbol both for particular objects and formal variables. The second is to distinguish clearly between the two different categories of objects, since they play quite distinct roles in our proofs.

3 Universal Quantifiers in Conclusions: Greek Knuckleballs

The answer to our first question is pretty straightforward: to prove a universally quantified statement of the form

for all x P(x),
we need to consider an arbitrary object in our universe of discourse and prove that this object must have property P.

What should we call the arbitrary object which we wish to prove has property P ? A natural choice would be `x'. There is nothing wrong with this choice per se. However, if our premises happen also to contain statements in which x appears as a bound variable, there is a possibility of confusion. For example, suppose that one of the premises is

for all t there exists x R(t,x)
It would certainly be a mistake to assume that the x appearing in this premise is the same as the arbitrary object x which we want to prove has property P. If our premises happened to contain a statement in which x appeared as a free variable, the situation would be even more confusing. In this case, x would already refer to some specific but unknown object, and it would be outright wrong also to use this name for an arbitrary object.

To avoid such conflicts, we need to choose notation and the names of variables carefully, and change the names of bound variables if necessary. The specific notational approach that I wish to suggest is to make a typographical distinction between formal variables and objects in the universe of discourse by using Greek letters to denote arbitrary objects in the universe of discourse. That is, when we want to prove a statement of the form "for all x P(x)" we will proceed by introducing a Greek letter---ALPHA, for example---to denote an arbitrary object in the universe, and then trying to prove that P(ALPHA) must be true.

Here is an analogy that may be helpful. We imagine that the ``arena of proof" is a baseball batting cage, and that these arbitrary objects from the universe of discourse are hurled at us by a ``pitching machine" that can throw all sorts of pitches at us. We have to be able to handle any kind of pitch that is thrown---fastball, curveball, knuckleball, slider, whatever. Fortunately, we will be told what pitch is coming before it is thrown, so we may choose an appropriate strategy for handling it, but we must be prepared for anything. Our argument may branch into cases depending on the type of object hurled at us, or we may simply be able to handle any type of pitch with a single type of swing. So these Greek letters represent arbitrary pitches we must handle, and we have no control over what pitch is thrown.

In particular, the only good reason ever to introduce one of these arbitrary objects into a proof is because we have to}---that is, because we want to prove some universally quantified statement. It is the statement to be proved that hurls the arbitrary objects at us; all we are doing with the Greek letters is giving those objects names.

Of course, some statements that we wish to prove may have more than one universal quantifier; in this case we will need to use different Greek letters for the different (or, more precisely, potentially different) objects that the machine may hurl at us. For example, if the statement we wish to prove has the form

for all x for all y R(x,y)
then we will need to let ALPHA and BETA represent arbitrary objects in the universe---objects that might or might not be equal to one another---and try to prove that R(ALPHA, BETA) is true. Pushing our analogy a bit, we can think of this as two ``parallel" pitches that we have to be able to handle with one swing of the bat, regardless of whether they are the same or different types of pitch.

4 Existential Quantifiers in Premises: Lucky Charms

The situation for existential quantifiers is essentially the ``dual" of that for universals. That is, we will introduce names for certain objects because of existential quantifiers appearing in the premises}, not in a potential conclusion. And these objects have the potential of being our ``friends": we may use them if we find it helpful to do so, but we are not obligated to ``deal with them."

For example, suppose that one of our premises is

there exists t W(t)
Since we are assuming our premises are true, this means that we know there is at least one object with property W---i.e., there is a witness for the existential quantifier. Clearly such an object is not arbitrary; the fact that it has property W makes it ``special." Therefore it does make sense to introduce a name for this object---or more precisely, for one such object, since there might be lots of them.

Again, we could just use the same name that appears as the bound variable---in this case, t---but this carries with it dangers analogous to those mentioned earlier. Hence it may again be useful to introduce yet another different type of symbol to denote a witness for the existential quantifier there exists t.

To be specific, the convention I propose is to use nonalphabetic, nonnumeric symbols such as HEART, CLUB, DIAMOND, SPADE, CIRCLE, STAR, and so forth---for this purpose. These may be a little hard to draw and pronounce, but they are certainly distinctive! We will call these symbols lucky charms.

As with the Greek knuckleballs, there is an analogy that may be helpful here. We will think of these existentially quantified premises not as pitching machines trying to throw something past us, but as ``vending machines" that dispense a product which we may find useful. For example, we may think of a premise

there exists t W(t)
as a vending machine that dispenses some object which has property W when we put in a quarter. (The quarter doesn't really represent any particular ingredient of the proof, other than the effort of using the premise!) This vending machine may or may not dispense the same object every time. That is, if there are 7 different objects in the universe which have property W , then we might get any one of those when we stick a quarter into the machine. But we will call whatever object the machine dispenses something like STAR or HEART. The most important thing to understand is that these ``lucky charms" dispensed by the vending machines aren't just any old objects in the universe. Rather, they are ``special" objects, and each one comes with a ``certificate of authenticity" guaranteeing that it has the property corresponding to the machine that dispensed it.

We may, of course, have premises which begin with multiple existential quantifiers; this causes no real complications as long as we again keep in mind that different symbols might represent the same object. For example, if one of our premises is the statement

there exists x there exists y L(x,y)
then we can introduce ``lucky charms" as witnesses for both existential quantifiers---for example, we could let SPADE and CLUB be objects (not necessarily distinct) for which L(SPADE,CLUB) holds.

Things get more complicated when our premises contain alternating quantifiers, since when we have a universal quantifier followed by an existential, the choice of witness for the existential quantifier is allowed to depend on how the universal quantifier was instantiated. If we have a premise which begins with an existential quantifier followed by a universal, then we can again go ahead and choose a witness for the existential; for example, if one of our premises is the statement

there exists x for all y M(x,y)
then we can choose an object DIAMOND for which the statement
for all y M(DIAMOND,y)
holds, and this statement now, in effect, becomes a new premise---that is, it is a statement which we know is true and hence may use in the same way we would use a premise. [In the next section we will discuss how we use universally quantified statements that appear as premises.]

If, on the other hand, we have a premise which begins with a universal quantifier followed by an existential, for example blockquote>for all x there exists y R(x,y) then we cannot choose a name for the witness for the there exists y until we have substituted the name of some particular object for x---i.e., until we have instantiated the universal quantifier. Hence, we again find it necessary to address the question as to how to use universally quantified statements that appear as premises.

5 Universal and Alternating Quantifiers in Premises

We have seen that in order to prove a universally quantified statement of the form "for all x P(x)", we introduce a symbol like ALPHA to represent an arbitrary object, and we try to prove that P(ALPHA) is true. Now let us consider how we can use a universally quantified statement that appears as (or is derived from) a premise. Suppose, for example, that one of our premises is the statement

for all x Q(x).
The crucial thing for students to understand is that there is no point in introducing a new arbitrary object \gamma merely for the sake of using it to instantiate the universal quantifier in this premise, thus deducing that \gamma has property Q . Instead, we want to instantiate that quantifier with previously introduced objects. For example, if we have already introduced objects called ALPHA, BETA, and STAR, then we may conclude that each of the statements Q(ALPHA) , Q(BETA) , and Q(STAR) is true. Whether any of these facts will be useful is another question---and indeed, a critical one. But at least there is a chance that they will be useful!

In particular, let us return to the case where we have a premise which begins with a universal quantifier followed by an existential, for example

for all x there exists y R(x,y).
As noted, we cannot choose a name for the witness for the there exists y until we have substituted the name of some particular object for x---i.e., until we have instantiated the universal quantifier. In such a situation, our vending machine analogy may be extended to say that the machine represented by this premise will not spit out a lucky charm until we have not only put in a quarter, but also specified the object we wish to use for x . (We can think of the machine as having one or more ``input slots" into which we feed object of the universe, as well as the slot for the quarter.) And the ``certificate of authenticity" for the lucky charm we receive will state clearly the object(s) for which it ``works."

Again, we are allowed to instantiate the universal quantifier in this statement with any object we want, but determining which one(s) will be useful for this purpose is not always such an easy task. However, we can again observe that there is never any point in introducing a new object solely for the purpose of ``plugging it into" this universal quantifier; we should restrict our attention to objects that have already been introduced.

When we are working in the realm of pure logic, then there are only two ways that objects should ever need to be introduced into a proof---namely the two ways we have already discussed. [If we are working within a specific universe, such as the set of natural numbers, then we also have the option of plugging in specific, concrete objects like 2 or 47.] Thus, when have a vending machine with ``object input slots" (corresponding to premises beginning with a universal quantifier followed by an existential), the objects that we plug into those should either be previously introduced arbitrary objects (Greek knuckleballs), or else lucky charms that have been obtained on earlier trips to vending machines.

Thus in the situation where we have "for all x there exists y R(x,y)" as one of our premises, one way to use this premise would be to substitute a previously introduced arbitrary object ALPHA for x, obtaining the statement

there exists y R(ALPHA,y)
At that point, we could let HEART, for example, denote an object in the universe for which R(ALPHA,HEART) is true. The critical thing we must then keep in mind is that the object HEART depends on the object ALPHA. We may want to denote this by using a ``functional" notation like HEART(ALPHA) to indicate the dependence, or we may just want to keep a mental note of this dependence in our minds. But in either case we cannot simply ignore it.

The other way to use the premise would be to instantiate the universal quantifier "for all x" with a previously introduced ``special object," say STAR, obtaining the statement

there exists y R(STAR,y)
We could then let DIAMOND, for example, denote an object in the universe for which R(STAR,DIAMOND) is true. While it is true that the object DIAMOND depends on the object STAR, this dependence is not as crucial here, since if STAR denotes one particular object in the universe, then so does DIAMOND. However, if STAR itself was obtained by the sort of process outlined in the previous paragraph, and hence depends in turn on an arbitrary object BETA, then that dependence is inherited by DIAMOND, and it may be wise to indicate these dependencies by notations of the form
These issues are especially important in the context of proving conclusions that themselves involve alternating quantifiers.

6 Proving Existentially Quantified Conclusions

Finally, let us consider how we go about proving a potential conclusion which contains an existential quantifier. For example, suppose the conclusion to be proved is

there exists t Z(t)
We certainly can't expect to proceed as we did in the universal case, by picking an arbitrary element ALPHA and proving that Z(ALPHA) holds. If we could do that, we would have proved the stronger claim
for all t Z(t) .
It's possible that this might actually work---that the stronger statement for all t Z(t) might be true---but we certainly can't count on it. Instead, we must show that some particular object satisfies property Z . But where are we to find this particular object? In the examples of the type we are considering here, the only real hope is that it will be one of the objects that we have obtained as a witness for some existentially quantified premise. [In the broader context of ordinary mathematics, we often have a larger pool of potential witnesses from which to draw. For example, if our universe of discourse is the set of integers, we have the possibility of using not only objects obtained from the explicit premises of the problem, but also specific numbers like 0, -1 , 42, or 1327, as well as objects obtained by combining both of these types of objects via operations like addition, subtraction and multiplication---like ALPHA + 3 for example, or 37 X HEART.

To push the machine analogy a bit further, what we are essentially trying to do is to show how to construct a vending machine that produces the desired object, using as ``components" the various machines provided by the premises. We must not only describe how to construct the machine, but we must also verify that the object it produces ``works" in the appropriate fashion.

Again, the picture becomes more complicated when alternating quantifiers are involved. Suppose, for example, that the conclusion to be proved is

for all x there exists y for all z B(x,y,z)
To see what is necessary to prove this, we work from the outside in. Since the outermost layer of structure is a universal quantifier, we choose an arbitrary object ALPHA and seek to prove that
there exists y for all z B(ALPHA,y,z)
This reduces our original goal to the subgoal of proving this existentially quantified statement; in order to find a witness for the existential quantifier "there exists y", we will somehow need to use the premises. Furthermore, it is permissible (and is likely to be necessary) for the choice of witness to depend on ALPHA. Once we have found such a witness, call it SPADE---or SPADE(ALPHA) to indicate the dependency on ALPHA---we must then try to prove that
for all z B(ALPHA,SPADE,z)
So we have reduced our subgoal, and hence our original goal, to the new subsubgoal of proving this universally quantified statement. In order to do this, we must consider another arbitrary object BETA (which may or may not be equal to ALPHA or SPADE---we cannot assume anything about this one way or another) and we must prove that
holds. Note in particular that our choice of SPADE is not allowed to depend on BETA, since it must be chosen before BETA is specified.

In terms of machines, this means that we are trying to construct a machine that takes whatever arbitrary object(s) a pitching machine throws into its input slot, and produces an object that has the desired properties relative to the given object(s). Granted, this is a rather mixed metaphor, but perhaps it is of some use.

7 Summary of Basic Principles and Conventions

At this point I have outlined the basic principles, notational conventions and metaphors I am suggesting for helping students to understand the overall structure of ``semiformal" proofs in the arena of predicate logic. Table 7.1 summarizes this discussion of how to deal with quantifiers in both premises and conclusions when trying to construct a proof in predicate logic.

Universal Existential

Instantiate with any object
already introduced; some
judgment is necessary to
decide which instantiations
might be useful.
Introduce a special symbol like
to denote an object with
the specified property.

Introduce a Greek letter like
ALPHA to denote an arbitrary
object, and try to prove that
the property holds for ALPHA.
Try to show that some object
obtained as a witness for
some existential quantifier
in the premises has
the desired property.
Table 7.1

It is only fair to acknowledge that these principles, conventions and metaphors often seem a little vague and mysterious when first presented. In order to understand them, students need to work through a number of specific examples. Even then, these conventions are no guarantee of success, but they do seem to be of some help in getting students to understand and keep track of the ``status" of each object that is mentioned in a proof, and to see what the general outline of the proof's structure must look like (even if they still have difficulty fleshing out that outline into a complete proof). Moreover, these conventions can certainly help diagnose mistakes and misconceptions that arise in the course of an attempted proof.

8 Some Specific Examples

Now that we have discussed the general principles involved in semiformal proof in predicate logic, as well as the notational conventions we wish to use, let's return to the two examples given earlier and see how we might attack them. For convenience, we restate the examples here.

Example 8.1

Consider the following list of premises:

A_1:for all x ([for all y T(x,y)] OR [there exists z R(x,z)])
A_2: there exists x for all y for all z [R(y,z) IMPLIES P(x,y)]
A_3: for all x there exists y Q(x,y)
A_4: for all x for all y for all z ([P(x,z) AND Q(x,y)] IMPLIES T(z,x))
Determine whether the conclusion
B: there exists a for all b T(b,a)
follows from the premises A_1--A_4.

Recall that earlier we rephrased each of the premises and the potential conclusion in terms of various objects sending and receiving certain types of arrows, in order to try to develop some intuition for those statements. For many students, drawing such pictures---and seeing how they fit together---is the crux of solving the problem. It is awkward, however, to describe or illustrate exactly this process in a static medium; the ``dynamic evolution" of the pictures is an essential feature of the process, and that evolution is likely to proceed a little differently for each student. I will leave it as an exercise to the reader to draw appropriate sketches; here I will present only a narrative version of the proof. One caveat is that, without accompanying pictures, these narrative proofs may tend to a flavor of syntactical pattern matching; that is perhaps not all bad, inasmuch as it might provide some feeling for how more strictly formal proofs might work, and even how we might attempt to automate certain aspects of theorem proving. Most students, however, prefer the added intuition provided by drawing the pictures and getting a feel for how they may be pieced together.

One important point for students to learn is that (mixing metaphors a bit) they can usually expect to erect a considerable amount of ``scaffolding," and can often expect to encounter a few dead ends, in the process of constructing a proof. In a completely finished, well polished proof, most of the scaffolding and all of the dead ends will have been eliminated, leaving an elegant but perhaps deceptively simple residue. In the proofs I will give here, quite a bit of the scaffolding will be retained, in the form of comments intended to suggest to the student why a particular route was chosen. It seems worthwhile, especially when students are first learning the process, to leave some of this scaffolding, and even sometimes to point out some of the typical dead ends that might be encountered.

Another important point is that constructing a proof often involves working both ``forward" from the premises, and ``backward" from the conclusion, with the hope that these two approaches ``meet in the middle." There are many variations on this theme, some much more subtle than others; the examples given here will involve very simple manifestations of the idea.

With these observations, let's now turn to the task of attempting to prove that the conclusion in Example 8.1 does indeed follow from the premises.

Annotated Proof of Example 8.1

Let's begin by ``working backwards" from the desired conclusion and observing that, since this conclusion begins with an existential quantifier, our task is to find a single witness for that quantifier; in other words, the witness we choose for a in the conclusion cannot ``depend on the choice of b." The crucial question, of course, is how we go about finding that desired witness.

To begin answering that question, it is reasonable to ``work forwards" from the premises, observing that A_2 is the only one which contains an existential quantifier which is not within the scope of some universal quantifier. This suggests that the object whose existence is guaranteed by A_2 is as good a place as any to start looking for the witness we seek. (It may or may not ultimately turn out to be the witness we seek for the conclusion, but it will probably play an important role in any event.)

Accordingly, let us choose a name, say DIAMOND , for an object witnessing A_2, so that we have

A'_2: for all y for all z [R(y,z) IMPLIES P(DIAMOND ,y)]
Let's try to prove that this object DIAMOND is indeed the witness we seek---i.e., that for all b T(b,DIAMOND )---bearing in mind that we may have to revise this plan if it doesn't work out.

So consider an arbitrary element of the universe, say BETA ; we will try to show that

is true. There are two places in which the predicate T appears in the premises. Looking at A_1, it's reasonable to try instantiating x with BETA , obtaining
A'_1: [for all y T(BETA ,y)] OR [there exists z R(BETA ,z)]
Now, if the first statement of this disjunction is true, then we're done, for then we can instantiate y by DIAMOND , obtaining (BETA,DIAMOND ) as desired. So we now must consider the case where that first disjunct fails and hence "there exists z R(BETA ,z)" holds.

We may as well go ahead and choose a witness for this statement, i.e., an object SPADE = SPADE(BETA) for which

holds. Again, the notation SPADE(BETA) serves to indicate that the choice of SPADE might depend on the object BETA. Since this statement involves R, it is reasonable to look next at the only other premise where R appears, A_. Remembering that DIAMOND is by definition a witness for the existential quantifier "there exists x in A_2", the obvious thing to try is to instantiate y with BETA and z with SPADE(BETA) in statement A'_2, yielding
from which we may conclude
This in turn suggests using A_4, instantiating x by DIAMOND and z by BETA (recalling that the order among consecutive universals is unimportant, so that we may switch the order of for all y and for all z in A_4) to obtain

This is very promising, for all we need now is to find a y for which Q(DIAMOND ,y) is true. And of course, this is exactly what A_3 guarantees we can do: instantiating x in A_3 by DIAMOND we get

there exists y Q(DIAMOND ,y),
so we can choose awitness, say STAR, so that
Then we can instantiate y in statement A'_4 by STAR, obtaining
Since P(DIAMOND , BETA ) and Q(DIAMOND, STAR) are both true, we conclude T(BETA , DIAMOND ) and we're done.

Example 8.2

Consider the following list of premises:

P_1: there exists x for all y T(y,x)
P_2: for all x (A(x) IMPLIES R(x,x))
P_3: for all x (B(x) IMPLIES there exists y S(y,x))
P_4: for all x for all y ( [S(x,y) AND NOT A(y)] IMPLIES R(y,x))
P_5: for all x for all y ( T(x,y) IMPLIES [A(x) OR B(x) OR R(x,y)] )

Determine whether or not each of the conclusions

Q_1 : for all x there exists y R(x,y)
Q_2 : for all x there exists y R(y,x)
follows from the premises P_1--P_5.

Again it is useful to begin by rephrasing the premises and potential conclusions:

P_1 says that every object receives at least one T-arrow.
P_2 says that every object with property A has an R-loop (i.e., sends an R-arrow to itself).
P_3 says that every object with property B receives at least one S-arrow.
P_4 says that whenever we have an S-arrow between two (not necessarily distinct) vertices, whose ``receiving vertex" fails to have property A, then there must be an R-arrow in the opposite direction as the S-arrow.
P_5 says that whenever we have a T-arrow between two (not necessarily distinct) vertices, then either there is an R-arrow in the same direction between those two vertices, or the sending vertex has at least one of properties A or B.
Hence a general ``schematic diagram" for any model of these premises will have two ``Venn blobs" (one for A and one for B) and three different types of arrows. Our potential conclusion Q_1 says that every object sends an R -arrow, while Q_2 says that every object receives an R-arrow.

Again, although this is still a relatively simple example, many students would find it very helpful to draw a number of pictures in order to get a better feel for how the premises fit together and whether or not the conclusions follow from them. We will again omit these pictures, however, leaving their construction as a highly recommended exercise.

Annotated Proof of Example 8.2:

Keeping in mind the theme of working both backwards and forwards, we might start by working backwards and observing that both of our potential conclusions begin with universal quantifiers. Hence it is reasonable to introduce a name for an arbitrary object, say ALPHA, hence reducing the problems of proving the two conclusions to those of proving the statements

Goals: there exists y R(ALPHA,y) and
there exists y R(y,ALPHA)
respectively. At this point we have two choices. One choice is to continue working somewhat backwards, scanning the premises to see which ones involve the predicate R , and determining suitable instantiations of some or all of the universal quantifiers involved in those premises. The other choice is first to look for some additional ``toeholds" among the premises that might help us ``work forwards."

When we are faced with choices of this type, it is usually true that either approach could work, though often one is likely to be more straightforward and less convoluted than the other. It takes some experience to develop a feel for which route is likely to get us to the desired destination faster. As a general rule of thumb, we expect ``finished" proofs to be presented primarily in a ``forward" manner, though that does not necessarily mean that that is the best way to discover the proof initially. Again, students should be made aware that they can't always expect to write a ``clean" proof in a single iteration.

In the example under consideration, probably the cleanest approach is to work forwards by choosing a witness---say CLUB---for the existential quantifier there exists x in premise P_1 , so that we have

P'_1: for all y T(y,CLUB)
In fact, this step could just as well be taken before the arbitrary object ALPHA is even introduced; this would have the modest advantage of removing any possible suspicion that the object CLUB might depend on ALPHA.

Once we have chosen the witness CLUB, we have two objects at our disposal, and both of them are reasonable candidates for substitution into the many universally quantified statements we know are true. Instantiating any of the universal quantifiers in premises P_2, P_3, or P_4, with either CLUB or ALPHA is of questionable value, since we have no guarantee that any of the hypotheses of the implications thus obtained would be true. The same observation is also true for P_5, except that finding an instantiation that makes the resulting T(*,*) hypothesis true seems much more promising, in view of P'_1.

These considerations suggest that a reasonable next step would be to instantiate the universal quantifier for all y in statement P'_1 with either ALPHA or CLUB (so why not both?), obtaining the statements

Of these two statements, the former looks more useful. Specifically, it now seems reasonable to instantiate the universal quantifiers for all x and for all y in premise P_5 with ALPHA and CLUB, respectively, obtaining the statement
Since the hypothesis of this implication is true, we can deduce that the conclusion must be also. That is, we have
Now if the third of these three disjuncts holds, we are at least moderately happy: we will have shown that there exists y R(ALPHA,y) is true in this case. So now we need to consider the case where R(ALPHA,CLUB) fails and hence either A(ALPHA) or B(ALPHA) (or both) is true.

If A(ALPHA) holds, then premise P_2 (with the obvious instantiation) immediately gives us R(ALPHA,ALPHA), so there exists y R(ALPHA,y) is true in this case as well.

If A(ALPHA) fails, then B(ALPHA) must hold, so premise P_3 (again with the obvious instantiation) gives us

there exists y S(y,ALPHA).
The obvious next step is to choose a witness, say HEART = HEART(ALPHA), for this statement, so that we have S(HEART,ALPHA). And now premise P_4 is perfectly poised to come to our aid: instantiating the universal quantifiers for all x and for all y in that premise with HEART and ALPHA, respectively, we get
Since the hypothesis of this implication is true, we may conclude that R(ALPHA,HEART), so there exists y R(ALPHA,y) is true in this third case as well.

In summary, we have shown that, given any arbitrary object ALPHA, we will find ourselves in one of three cases, and in each such case the statement there exists y R(ALPHA,y) is true. Hence we have indeed shown that conclusion Q_1, for all x there exists y R(x,y), follows from the premises. [It is important for the student to understand that our choice of witness---indeed, even the manner in which this witness is chosen---definitely depends on the arbitrary object ALPHA.]

At this point it seems that we have pretty much extracted all the information available from the premises, and we have not succeeded in proving conclusion Q_2, for all x there exists y R(y,x). However, it must be emphasized to students that this failure does not constitute a proof that the conclusion does not follow from the premises, and that they must find a counterexample in order to verify that.

In this case (as is true in many of these simple examples), a very simple counterexample can be found: let the universe of discourse consist of just two objects, say 1 and 2, neither of which has property A nor property B . Let there be both T-arrows and R-arrows from 1 to itself and from 2 to 1, but no S-arrows. Then it is easy to verify that all the premises hold (note that P_2, P_3, and P_4 hold vacuously), but conclusion Q_2 fails since object 2 receives no R-arrow.

9 Transfer of Techniques to More Concrete Settings

Although the focus in this paper has been on semiformal proof in predicate logic, the ultimate goal is for students to be able to transfer the ideas and skills developed in that context to a wide variety of settings. The notational conventions introduced here tend to look even more bizarre when used in more concrete and familiar mathematical contexts, but I believe they are still of some pedagogical value, at least in the early stages of the transition. One setting in which they can be used fairly effectively is in proving elementary results about limits (either of sequences or of functions with continuous domains, though my taste runs toward the former as providing a better starting point). I believe that the most difficult feature of the formal definition of limit is its logical structure, involving as it does two alternations of quantifier followed by an implication. I also believe that the conventions introduced here can be of some value in helping students understand that logical structure.

It should also be acknowledged that the transfer can also work in the other direction, to some extent. That is, one way to ease students into examples of the type discussed above, whose formality and abstractness can sometimes be intimidating, is first to consider settings in which the predicates are given more familiar and intuitive characterizations, but all premises must still be explicitly stated. For instance, I have used examples in which the universe is understood to be a certain set of people, and we have unary predicates meaning that a person is a cyclist or a gymnast, or a bozo or a chucklehead, and binary predicates meaning that one person amuses, is married to, or is taller than another. Just as in the more abstract examples, an explicit list of premises is given, along with a list of potential conclusions, and students are asked to determine whether or not the conclusions follow from the premises, providing proofs or counterexamples as appropriate. One advantage of this approach is that it can also provide students with additional practice in translating statements between ordinary English and the language of predicate logic.

10 Conclusion

None of the ideas, principles, conventions or metaphors presented here is profound or revolutionary, nor is any of them a panacea. To paraphrase Euclid, there is no royal road to proof; it's an inherently difficult activity, and as G\"{o}del, Church, Turing et~al.~have shown us, that difficulty is very real. However, I do believe that the ideas presented here can be of some value in helping students and teachers focus on several essential aspects of the logical structure of proof. I have been using and refining these and related ideas in the classroom for several years, and I have noticed significant (though admittedly not universal nor even strictly monotone) improvement in students' mastery of basic principles of proof as a result. Much work still remains to be done, and there is plenty of room for improvement---especially in the area of transferring the skills developed in the predicate logic setting to more concrete and complex mathematical settings.