2
$\begingroup$

I propose the following restriction on universal instantiation: UI may not be used to introduce new variables. The variable specified should be an "old" variable, i.e. it must already have been introduced by either an active premise or by existential instantiation (E-elimination). (An active premise is one that has not been closed-off or discharged by what I call a conclusion statement.)

The primary benefit of this restriction is to eliminate the need to consider dependencies among variables that are created with existential instantiation. Such considerations never seem to come up in "real mathematics." The restriction I propose seems to be implicit even in the most rigorous mathematical proofs, if not in standard formal logic.

With this restriction in place, dependencies among variables need not be considered because the only variables on which you could then make universal generalizations are those introduced in a premise that has subsequently been closed-off or discharged by what I call a conclusion statement. The conclusion statement and subsequent statements that are derived from it and also refer to these variables can always be universally generalized regardless of the presence of any other variables that were introduced by E-elimination.

I have implemented this restriction in my proof checker/editor (available free at http://www.dcproof.com). Play around with it. Try to "break it" if you can. Work through the brief tutorial to learn the system.

Another benefit, from a pedagogical perspective, has been the elimination from my program of several what must have been confusing warning messages about dependencies among variables. It also simplifies the requirements for universal generalizations (A-introduction).

Following is a summary of the rules of inference I use in my system that are relevant to the handling of free variables:

  1. Free variables may be introduced only by means of a premise (assumption) or by existential specification (E-elimination).

  2. Existential specification (E-elimination) allows an unused free variable to be specified for any active, existentially quantified statement.

  3. Universal specification (A-elimination) allows any free variable introduced by an active premise or any algebraic expression in such free variables to be specified for any active, universally quantified statement.

  4. Existential generalization (E-introduction) may be applied to any free variable or any algebraic expression in one or more free-variables that is found in any active statement.

  5. Universal generalizations (A-introduction) may be applied to any free variable that (a) is found in an active statement, and (b) is not referred to by any active premise, and (c) was not introduced by existential specification (E-elimination). (There are no considerations given for any dependencies among variables.)

  6. Free variables introduced after a premise statement and before the corresponding conclusion statement may not appear in that conclusion statement.

In my program, I use color-coding for free variables. Green indicates that a Universal Generalization is possible. Red indicates that a Universal Generalization is not possible. When first introduced, all free variables are red. A free variable that was introduced by a premise is changed to green when that premise is closed-off (or discharged) by a conclusion statement. It is effectively reintroduced, changing back to red if it is referred to in subsequent premise.

Your comments would be appreciated.

Improve this question
$\endgroup$
1
$\begingroup$

You can always add some tautology as an assumption (say $x \rightarrow x$) and then later discharge it, so it seems like your restriction is valid.

Check "Structural Proof Theory", a book by von Plato and Negri, which discusses such issues; it also sponsors a proof editor PESCA by Aarne Ranta.

Improve this answer
$\endgroup$
5
  • $\begingroup$ I can generate P -> P by entering any premise P and immediately invoking the conclusion rule. Is that what mean? And what do you mean by "your restriction is valid?" I would like to know if this restriction and ignoring any consideration of dependencies among variables like this might lead to any mathematically invalid proofs. I can't foresee any such problems, but this is not my area of expertise. (Note, I have added more detail.) $\endgroup$ – Dan Christensen Nov 29 '10 at 16:55
  • $\begingroup$ You can add as an assumption $P(x) \rightarrow P(x)$, so that you can use $x$ in UG. Since $P(x) \rightarrow P(x)$ is a tautology, you can later on discharge it. So it seems any proof can be rewritten to respect your restriction. $\endgroup$ – Yuval Filmus Nov 29 '10 at 22:32
  • $\begingroup$ Yes, that would work. You could also begin with the assumption P(x). Anything to introduce a free variable. $\endgroup$ – Dan Christensen Nov 30 '10 at 14:21
  • $\begingroup$ In practice, every mathematical theory starts by introducing some free variable, e.g. the set of natural numbers, the set of points in a space, etc. $\endgroup$ – Dan Christensen Nov 30 '10 at 14:33
  • $\begingroup$ On second thought, it is not quite so easy. Even if we introduce a free variable at the beginning, I cannot prove Ex Ay R(x,y) -> Ay Ex R(x,y). Not directly anyway. I would not be able to do the final universal generalization because the initial premise would be referring to the variable I would need to generalize. Even without this initial premise, however, I could directly prove Ex Ay [P(x) -> R(x,y)] -> Ax [P(x) -> Ey R(x,y)] Fortunately, in mathematical practice, universal generalizations are always of the form Ax [P(x) -> Q(x)]. $\endgroup$ – Dan Christensen Nov 30 '10 at 15:26
1
$\begingroup$

Follow-up

Much to my chagrin at the time (happy ending though!), I discovered that restricting Universal Instantiation alone was not enough to avoid problems with dependent variables. By indirect methods you could still use UI to introduce new free variables as follows:

  1. Ax P(x)         (Premise)
  2. ~P(y)            (Premise)
  3. P(y)               (UI, 1)
  4. P(y) & ~P(y) (Join 2,3)
  5. ~~P(y)          (Conclusion, 2)
  6. P(y)               (Remove ~~)

I managed to close off this possibility, however, by formalizing what mathematicians habitually seem to do when writing proofs:

When you want to prove something is true in general, you introduce an assumption with one or more new free variables in it, say P(x). Then you prove, say Q(x). Then, if Q(x) is not a contradiction, you can then generalize Ax (P(x) => Q(x)). In this case, you must ensure that no free variables introduced in the interim occur free in Q(x). If Q(x) is a contradiction, then Ax ~P(x).

By implementing this rule in my program, the conclusion on line 5 becomes:

Ax ~~P(x) (Conclusion, 2)

My new conclusion rule will automatically generalize on variables introduced in the corresponding premise (line 2 in this case). There is now no other way introduce universal quantifiers. It just doesn't seem to be necessary.

In addition to automatically doing universal generalizations, the new conclusion rule will also automatically do existential generalizations if necessary so that no new free variables show up in the conclusion. See the example at:

http://www.dcproof.com/EA-AE.html

This HTML document was generated using my program. Comments are in a blue font.

My DC Proof program may not serve everyone's need, but if students want to write mathematical proofs in, say, number theory, algebra or analysis, it can serve as an excellent introduction to the rules that mathematicians actually use when writing proofs. In my opinion, there is simply no need to burden such students with esoterica about dependent variables that never seem to come up outside of rarefied philosophical discussions.

You can download Version 2.0 of my program at my website http://www.dcproof.com

Dan

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.