Additional Notes Regarding ProofBuilder

by Hugh McGuire

The material here augments the basic manual for ProofBuilder with additional explanations, background information, and pedagogical points.  The section numbers here refer to the section numbers there.

3. Starting a Proof

If you are an instructor, you may find it very convenient to make Web pages from which students can copy/paste formulas to be used in ProofBuilder.  Making students type the formulas themselves doesn't really teach them anything, and if they do try to type them, they may occasionally make typographical errors which could interfere with the proof construction which they are supposed to be learning; e.g. they may waste time trying to prove formulas that are subtly different from those which you may have intended.

3.7 Automatic simplifications

If you want, send e-mail to me and I can provide the list of simplifications using whichever symbols you may prefer.  (I can do this easily thanks to "global search and replace".  ;-)

7.2 To apply an equation or equivalence or inequality, it needs to have South polarity

 To apply an equation or equivalence or inequality, it needs to have South polarity because otherwise deduction might be unsound, i.e. otherwise you might be able to prove things that aren't really universally true.  To show the necessity for this policy, the following improper material shows how one could 'prove' something that is not universally true by violating the policy: though the equation labeled (2) doesn't have South polarity, it is applied to the expression labeled (4), yielding the expression labeled (5).
Improper 'proof' of the following formula: 
    a = c  ∨  c = a

(#)   Suppositions Theorem/Subgoals
      We start working with the formula being proved
as follows:
(1)     
a = c  ∨  c = a
      That formula can be separated into two
alternative goals; first:
(2)     
a = c
      or alternatively:
(3)     
c = a
       
      We'll work on transforming the left-hand side of formula (3)
to the right-hand side as follows:
(4)     
c
          =      by (2)
(5)     
a
      And that satisfies the earlier goal (3); i.e. we have:
(6)     
true
      That concludes this improper 'proof'.

7.4 Rewrite selection

If you want, send e-mail to me and I can provide the list of rewritings using whichever symbols you may prefer.  (I can do this easily thanks to "global search and replace".  ;-)

7.6 For the bivalence deduction, a proposition needs to occur with each polarity

 The result of the deduction Invoke bivalence would be inconsequential if you were to apply it to a proposition that doesn't occur with both polarities in the relevant formula.  For example, suppose we are attempting to construct a proof for the formula P, i.e. suppose we are trying to prove that it is universally true.  The result of going ahead improperly and applying the deduction Invoke bivalence to that goal formula would be the new goal false ∧ true, which simplifies to false; but this does not help to prove that P is universally true.