too intuitive to prove

[John C. Baez]

In article <1992Oct8.0...@u.washington.edu> mena...@u.washington.edu 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)

This is an "unravel the definitions and bingo!" sort of proof. I
suggest you write down the definition of R being symmetric very
carefully in terms of conditions on R(x,y) for all x,y in A, and
similarly write down the definition of R = R^{-1}, and you will see
that they are the same.

[Piotr Rudnicki]

mena...@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

[Bryan Carpenter]

In <1992Oct8.0...@u.washington.edu> mena...@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.

``R symmetric'' defined by a R b <=> b R a, and ``R^-1'' defined by
a R^-1 b <=> b R a, seem like good starting points.

>Thanks,
>We call our selves the mutants.

Bryan