# Proof in predicate calculus 2

Let:

1) P be one place operation

2) H be two place operation

3) G be two place predicate

4) k, m be two constants

Let :

The following assumptions :

1) $\forall x [\neg G(x,k)\Longrightarrow G[H(P(x),x),m]]$

2)$\forall x\forall y\forall z[G(x,y)\Longrightarrow G[H(z,x),H(z,y)]]$

3)$\forall x\forall y\forall z [G(x,y)\wedge G(y,z)\Longrightarrow G(x,z)]$

4)$\forall x\forall y [G(x,y)\Longrightarrow G(y,x)]$

5)$\forall x\forall y [G[H(x,y),H(y,x)]]$

6)$\forall x[ G[H(x,m),m]]$

Then formally prove that:

Then formally prove : $\forall x\forall y\forall z[\neg G(x,k)\Longrightarrow(G[H(x,y),H(x,z)]\Longrightarrow G(y,z))]$

CompuChip
Homework Helper
That's the same one as here, luckily you've formatted it a bit better this time (Y).