# Proof in predicate calculus

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)}

## Answers and Replies

CompuChip
Science Advisor
Homework Helper
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
Science Advisor
Homework Helper
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).