Can G[P(A),c] imply G(A,c) be proven using predicate calculus axioms?

[solakis]

Let:

1)P be one place operation

2)K be one place operation

3) c be a constant


let :

1) G be a two place predicate

2) H be a two place predicate

Let :

The following axioms or assumptions)

1)for all A { H(A,c)v H(c,A)v G(A,c)}

2)for all A { H(A,c)=> G[P(A),A]}

3)for all A {H(c,A) => G[P(A),K(A)]}

4)for all A {G[K(A),c] => G(A,c)}.

5)for all A,B,C { [G(A,B) and G(A,C)]=> G(B,C)}

Then formally prove :

for all A {G[P(A),c] => G(A,c)}

 

[CompuChip]

Sounds like an interesting exercise, I'll try it later.
Have you finished it yet, or are you just fishing around for the answer? :-)

 

[CompuChip]

Just got home from work and had a serious look at the problem.
It's an interesting problem.
I found the way to do it, but I haven't written down the complete formal proof because I don't really feel like proving OR elimination for three variables at this point (i.e. { A v B v C, A => D, B => D, C => D } |= D).