Substitution

We cannot replace bound variables under any circumstances.  It is easy to see why - we run the risk of changing the meaning of the formula.  For example, if we substitute y for the x in TEx P(x)  we would get TEx P(y).  It is entirely possible that the first might be true and the second might be false - in fact, if y represents a constant such that P(y) is false, the second formula is necessarily false.

Substituting for free variables is always legal.  We write "PHI[t/x]" to mean "replace all free instances of x in PHI with t".  Note that if  PHI does not contain any free instances of x, then the substitution has no effect.

Even though it is legal, substituting for free variables is not always safe.  Suppose that in PHI, a free instance of x occurs within the scope of a quantified variable y.  If we replace x with a term that includes the variable y, then this variable is now bound by the quantifier.  It is easy to see that by giving up this freedom we run the risk of changing the circumstances in which the formula is true.

We say that a term t is free for x in PHI if none of the free instances of x in PHI are within the scope of any quantifier that applies to any variable that appears in t.  This seems like a complex idea, but it is easy to absorb if we remember that it just means that it is safe to substitute t for x in PHI.


New Proof Rules for Predicate Calculus


 We follow the text very closely for this material.  The new rules are

Rules for Equality

=i       "equality introduction"

Basically, this rule says that we can always add "t = t" to our proofs, where t is any term.

=e      "equality elimination"

This one is more interesting, because it lets us apply substitution in our proofs.  The idea is that if we have "t1 = t2" in our proof, and we also have a formula of the form PHI[t1/x]   (i.e. a formula in which t1 has been substituted for all the free instances of x), then we can add the formula given by PHI[t2/x].  This makes sense because if t1 = t2, they should have the same effect on the truth of PHI.  Note that when we talk about these substitutions, we are requiring that both t1 and t2 be free for x in PHI.

The trick with using this rule is recognizing when we have a useful formula of the form PHI[t1/x] in our proof.


Rules for Universal Quantification

FA x e       "for all x elimination"

Given FA x PHI , we can substitute anything we want for the free instances of x in PHI (as long as what we substitute is a term which is free for x in PHI).  It is important to realize that PHI does not include the FA x that precedes it.  For example, if we have "FA x (P(x) -> Q(x))" then PHI is "P(x) -> Q(x)" and in PHI, both occurrences of x are free.

FA x i      "for all x introduction"

Our method for introducing a universal quantifier is to create a new, completely unconstrained variable (traditionally called x0) and attempt to prove some formula that includes x0 (ie a formula of the form PHI[x0/x]).  In writing our proofs, we open a box which looks just like an assumption box, but which I think makes more sense as the scope of the variable x0.

When we have proved PHI[x0/x] within the box, we can close the box and state "FA x PHI".  We can do this because we didn't put any constraints on x0, so whatever properties it has are ones that it shares with all objects in the universe.  Hence the lines of the proof within the box would work no matter what actual value we assigned to x0.  That's just another way of saying that the conclusion is true for all x.

Rules for Existential Quantification

TE x i      "there exists x introduction"

If we have PHI[t/x]  in a proof (ie. a formula which would result from replacing all the free x's in PHI with t) then we know that there is some value that makes PHI true.  Thus we can introduce the formula "TE x PHI"

This may seem unuseful because it is giving up some information - we are going from an assertion that PHI is true for a specific value to an assertion that PHI is true for some unknown value.  It is actually very useful to us because often the specific value for which PHI is true will be a "local" variable defined within an assumption box.  We can't carry that variable outside the box, but after we generalize the statement "PHI[x0/x]"  to "TE x PHI", we can carry that statement outside the box.



It is important to note that throughout all of these discussions and explanations, whenever I write "PHI[t/x]", it is understood that this particular sequence of characters is not a formula, and would not appear as a line in our proof.  "PHI[t/x]" represents a formula, namely the one that would result from replacing all free x's in PHI by t.  This is the formula that would appear in the proof.


"there exists" elimination:

We can think of this as a generalization of the the "or elimination" rule that we already know.  In this case, we start with a statement of the form "TE x PHI" - ie we know there is at least one value of x that makes PHI true.  So we open up an assumption box where the assumption is "let x0 be a value of x for which PHI is true" - x0 must be a new variable.  Then we continue applying rules inside the box until we reach a desired conclusion CHI.  As long as CHI does not contain any reference to x0, we can close the box and assert that CHI is true outside the box.  This is valid because x0 is just a place-holder for whichever value of x is the one that makes PHI true - as long as x0 is a new variable without any ties to anything outside the box, the final conclusion CHI must be true regardless of the specific value of x0 - that is, we are able to derive CHI just from knowing that x0 exists, not from knowing anything about its value.