From: piotr@cs.UAlberta.CA (Piotr Rudnicki)
Newsgroups: sci.math
Subject: Re: too intuitive to prove
Date: 9 Oct 92 16:44:04 GMT
Organization: University of Alberta, Edmonton, Canada

menasian@milton.u.washington.edu (Gregor Menasian) writes:

>A group of us are working on a problem that is far too obvious for us to
>grasp.  We need to prove, either formally or informally, that a relaion R
>on a set A is symmetric if and only R=R^(-1)

>We're looking for either ideas to start us off or a complete proof.  
>(a complete proof is, of course, perfered)

>Our biggest problem is that the proof must be formal.  

>Thanks, 
>We call our selves the mutants.

Although normally considered obvious, this and similar problems
seem extremely difficult for freshmen. They do not know how to
structure a proof, let alone fill in gaps that require some gymnastics.

In our 1st year course on ligic in computer science we give our students
an opportunity to practice their skills in structuring proofs.
They do it with the company of a proof checker that checks their proofs.
The language of the proof-checker is a `raw' first order logic, even
without functional notation!

Send me e-mail if you want to know more about our experience.

Here is a solution to the problem asked above:

-------------------------

!! MIZAR-MSE UNIX   version 2.2  Dep of Comp Sci, Univ of Alberta
!!                        on  9 Oct 92   at  10:43:20      
!!

environ                 
 reserve r,r',r'' for relation; 
                                == domain and range are the same set A;
 reserve x,x',x'',y,y',y'' for elementofA;

symmetry:               
  for r holds symmetric[r] iff (for x, y st is[x,r,y] holds is[y,r,x]); 

converse:
  for r, r' holds converse[r,r'] iff (for x, y holds is[x,r,y] iff is[y,r',x]);
        
relequality:
  for r,r' holds r = r' iff (for x, y holds is[x,r,y] iff is[x,r',y]);
        
begin
        
for r, r' st converse[r,r'] holds symmetric[r] iff r = r'
  proof let r, r' be relation such that
    1: converse[r,r'];
    2: symmetric[r] implies r = r'
         proof
           assume 21: symmetric[r];
             22: for x, y holds is[x,r,y] iff is[x,r',y]
                   proof let x, y be elementofA;
                     221: is[x,r,y] implies is[y,r,x]  by 21, symmetry;
                     222: is[y,r,x] implies is[x,r',y] by 1, converse;
                     223: is[x,r',y] implies is[y,r,x] by 1, converse;
                     224: is[y,r,x] implies is[x,r,y] by 21, symmetry;
                    thus is[x,r,y] iff is[x,r',y] by 221, 222, 223, 224
                   end;
           thus r = r' by 22, relequality
         end;
    3: r = r' implies symmetric[r]
         proof
           assume 31: r = r';
             32: for x, y st is[x,r,y] holds is[y,r,x]
                   proof let x, y be elementofA such that
                     321: is[x,r,y];
                     322: is[x,r',y] by 31, 321, relequality;
                    thus is[y,r,x] by 1, 322, converse
                   end;
           thus symmetric[r] by 32, symmetry
          end;
   thus symmetric[r] iff r = r' by 2, 3
  end
!!
!! Thanks, OK
!! ----------


--
Piotr (Peter) Rudnicki
Newsgroups: sci.math