Formal Proof for Predicate Calculus 2: Solving Complex Operations and Predicates

[solakis]

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]

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

Any progress on the answer?

 

[solakis]

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

Any progress on the answer?

That is a completely different problem.

No, no any answer yet.