Proving Uniqueness in Predicate Calculus with G and F Functions

[solakis]

Given the following :

1)\forall x\forall y\forall z G(F(F(x,y),z),F(x,F(y,z)))


2)\forall xG(F(x,c),x)


3)\forall x\exists yG(F(x,y),c)


4)\forall x\forall yG(F(x,y),F(y,x)).


5) \forall x\forall y\forall z ( G(x,y)\wedge G(x,z)\Longrightarrow G(y,z))

Where G is a two place predicate symbol. F ,is a two place term symbol and c is a constant.


Prove :\exists! y\forall xG(F(x,y),x)

\exists ! y means : there exists a unique y

 

[praeclarum]

Is this a homework question, or just for fun, or what?

And I am assuming that E! x ph <-> E. y A. x ( x = y <-> ph ), right?

 

[solakis]

This is a problem given to me by a friend ,that i could not solve out.

This two place predicate and term is very confusing.

 

[praeclarum]

Is "c" a constant or a variable? Because if it is a variable, then you can prove a contradiction given the conclusion and given that there are at least 2 distinct values of x.

We could prove that A. y A. x G ( F ( x , y ) x ) given 2, which contradicts the conclusion.

 

[solakis]

I have mention it already in my opening post that c is a constant

 

[xxxx0xxxx]

Well, existence is straight forward:

From 2) and c

\exists c \wedge \forall x G(F(x,c),x) \Rightarrow \exists y \forall x G(F(x,y),x)

uniqueness is left as an exercise:

\forall u(\forall x G(F(x,u),x) \Rightarrow u=c)

 

[micromass]

When you take G the equality, then your list of axioms is that of a commutative group. The thing you need to prove is that the identity element is unique.

Take two identity's c and c', then

3) G(F(c',c),c')

and

3) G(F(c,c'),c)

and

4) G(F(c,c'),F(c',c))

So by (5), we get that G(c,c')

But that doesn't give equality, however...

 

[micromass]

OK, what about this counterexample:

Take \mathbb{Z}_0 as universe. Take

G(x,y)~\text{if and only if}~\frac{x}{y}\geq 0

and F(x,y)=x*y and c=1.

Then y=1 and y=2 both satisfy the hypothesis.