home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #23 / NN_1992_23.iso / spool / sci / math / 12977 < prev    next >
Encoding:
Internet Message Format  |  1992-10-09  |  3.5 KB
  1. Path: sparky!uunet!portal!lll-winken!elroy.jpl.nasa.gov!swrinde!zaphod.mps.ohio-state.edu!sol.ctr.columbia.edu!destroyer!cs.ubc.ca!unixg.ubc.ca!kakwa.ucs.ualberta.ca!alberta!piotr
  2. From: piotr@cs.UAlberta.CA (Piotr Rudnicki)
  3. Newsgroups: sci.math
  4. Subject: Re: too intuitive to prove
  5. Message-ID: <piotr.718649044@sedalia>
  6. Date: 9 Oct 92 16:44:04 GMT
  7. References: <1992Oct8.053608.24694@u.washington.edu>
  8. Sender: news@cs.UAlberta.CA (News Administrator)
  9. Organization: University of Alberta, Edmonton, Canada
  10. Lines: 86
  11. Nntp-Posting-Host: sedalia.cs.ualberta.ca
  12.  
  13. menasian@milton.u.washington.edu (Gregor Menasian) writes:
  14.  
  15. >A group of us are working on a problem that is far too obvious for us to
  16. >grasp.  We need to prove, either formally or informally, that a relaion R
  17. >on a set A is symmetric if and only R=R^(-1)
  18.  
  19. >We're looking for either ideas to start us off or a complete proof.  
  20. >(a complete proof is, of course, perfered)
  21.  
  22. >Our biggest problem is that the proof must be formal.  
  23.  
  24. >Thanks, 
  25. >We call our selves the mutants.
  26.  
  27. Although normally considered obvious, this and similar problems
  28. seem extremely difficult for freshmen. They do not know how to
  29. structure a proof, let alone fill in gaps that require some gymnastics.
  30.  
  31. In our 1st year course on ligic in computer science we give our students
  32. an opportunity to practice their skills in structuring proofs.
  33. They do it with the company of a proof checker that checks their proofs.
  34. The language of the proof-checker is a `raw' first order logic, even
  35. without functional notation!
  36.  
  37. Send me e-mail if you want to know more about our experience.
  38.  
  39. Here is a solution to the problem asked above:
  40.  
  41. -------------------------
  42.  
  43. !! MIZAR-MSE UNIX   version 2.2  Dep of Comp Sci, Univ of Alberta
  44. !!                        on  9 Oct 92   at  10:43:20      
  45. !!
  46.  
  47. environ                 
  48.  reserve r,r',r'' for relation; 
  49.                                 == domain and range are the same set A;
  50.  reserve x,x',x'',y,y',y'' for elementofA;
  51.  
  52. symmetry:               
  53.   for r holds symmetric[r] iff (for x, y st is[x,r,y] holds is[y,r,x]); 
  54.  
  55. converse:
  56.   for r, r' holds converse[r,r'] iff (for x, y holds is[x,r,y] iff is[y,r',x]);
  57.         
  58. relequality:
  59.   for r,r' holds r = r' iff (for x, y holds is[x,r,y] iff is[x,r',y]);
  60.         
  61. begin
  62.         
  63. for r, r' st converse[r,r'] holds symmetric[r] iff r = r'
  64.   proof let r, r' be relation such that
  65.     1: converse[r,r'];
  66.     2: symmetric[r] implies r = r'
  67.          proof
  68.            assume 21: symmetric[r];
  69.              22: for x, y holds is[x,r,y] iff is[x,r',y]
  70.                    proof let x, y be elementofA;
  71.                      221: is[x,r,y] implies is[y,r,x]  by 21, symmetry;
  72.                      222: is[y,r,x] implies is[x,r',y] by 1, converse;
  73.                      223: is[x,r',y] implies is[y,r,x] by 1, converse;
  74.                      224: is[y,r,x] implies is[x,r,y] by 21, symmetry;
  75.                     thus is[x,r,y] iff is[x,r',y] by 221, 222, 223, 224
  76.                    end;
  77.            thus r = r' by 22, relequality
  78.          end;
  79.     3: r = r' implies symmetric[r]
  80.          proof
  81.            assume 31: r = r';
  82.              32: for x, y st is[x,r,y] holds is[y,r,x]
  83.                    proof let x, y be elementofA such that
  84.                      321: is[x,r,y];
  85.                      322: is[x,r',y] by 31, 321, relequality;
  86.                     thus is[y,r,x] by 1, 322, converse
  87.                    end;
  88.            thus symmetric[r] by 32, symmetry
  89.           end;
  90.    thus symmetric[r] iff r = r' by 2, 3
  91.   end
  92. !!
  93. !! Thanks, OK
  94. !! ----------
  95.  
  96.  
  97. --
  98. Piotr (Peter) Rudnicki
  99.