- Thread starter
- #1

1) m be a constant

2) P ,K be one place operation symbols

3) F be two places operation symbol

4) H,G be two places predicate symbols

Let, the following assumptions:

1) $\forall A\forall B [ H(A,m)\Longrightarrow G[P(A),B]\Longleftrightarrow G[K(B),A]\wedge H(B,m)]$

2) $\forall A\forall B[ H(A,m)\wedge H(B,m)\Longrightarrow H(F(A,B),m)]$

3)$\forall A\forall B\forall C\forall D[ G[A,B]\wedge G[C,D]\Longrightarrow G[F(A,C),F(B,D)]]$

4)$\forall A\forall B [ G[F(K(P(A)),K(P(B))),K(F(P(A),P(B)))]]$

5)$\forall A\forall B\forall C [ G[A,B]\wedge G[A,C]\Longrightarrow G[B,C]]$

6) $\forall A [ G(A,A) ]$

Then prove :

$\forall A\forall B [ H(A,m)\wedge H(B,m)\Longrightarrow G[ P(F(A,B)),F(P(A),P(B))]]$