# Proof on symmetry

1. Aug 25, 2012

### Kolmin

1. The problem statement, all variables and given/known data

$R$ is simmetric iff $R=R^{-1}$

2. Relevant equations

$( \forall x \forall y ((x,y) \in R \rightarrow (y,x) \in R)) \leftrightarrow R=R^{-1}$

3. The attempt at a solution

My problem is with my formulation in [2.] of the statement I have to prove.

Is that formulation right or the right one is $( \forall x \in A \forall y \in A ((x,y) \in R \rightarrow (y,x) \in R)) \leftrightarrow R=R^{-1}$?

The difference is significative, at least for my purpose. In the first case, I can prove it, in the second one, I cannot (or I am not able), so I would like to know if the second one is redundant.

2. Aug 25, 2012

### Bacle2

What is A? And, just to makesure, what is the definition of symmetric you're starting with? I know this is a standard term, but maybe your definition is slightly different?

3. Aug 25, 2012

### Kolmin

Well, that's the problem.

Given a set $A$, a relation $R$ on $A$ is symmetric if $\forall x \in A \forall y \in A(xRy \rightarrow yRx)$.

So, here we are.The formulation in [3.] should be the correct one to translate the statement in [1.] in logical terms, but - at the same time - it is problematic cause I am free to derive the $[ \rightarrow ]$ part of the proof only if there is not $A$ in the definition. Then, is it redundant or not?

PS: Not sure you read my previous thread, but the all problem arises cause I am trying to use the software Proof Designer, which is a tool that can be use to implement the learning system presented in the book How to prove it: a structured approach to develop proof-skills. This software (and the books) are great, but the (positive!) side-effect is that human flexibility is not the point here.

4. Aug 26, 2012

### Kolmin

Just for the curious reader, who is studying How to prove it and who is frustrated by the lack of results obtained with Proof Designer, I think I found a way to fix the problem.

We define the theorem that has to be proved in the following way: $$\forall x \in A \forall y \in A((x,y) \in A \times A \rightarrow (y,x) \in A \times A) \leftrightarrow A \times A = (A \times A)^{-1}$$.
Then we define $R=A \times A$ and the problem is solved.

PS: $A$ obviously is not redundant, so my question was simply wrong!