# Proof in predicate calculus

1. Jun 22, 2012

### stauros

Given :

a)

1) c is a constant

2) P and K are one place operation symbols

3) G and H are a two place predicate symbols

b)

The following hypothesis

1)for all A { G(A,A) }

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

Then prove :

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

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

2. Jun 23, 2012

### dcpo

How you formally work this through depends on what system you're asked to work with, but a strategy would be to let B=P(A).

3. Jun 23, 2012

### stauros

Thanks dcpo .So i put B=P(A) in 2 and i get :

{ H(A,c) =>( G[P(A),P(A)] <=> ( G[K(P(A)),A] and H(P(A),c)))}
is that correct?

The proof is in predicate calculus ,so every line of the proof has to be accounted for and justified

4. Jun 23, 2012

### dcpo

Well, what you need to say depends on how formal you have to be, and on what deduction system you have to use, but what you have is the basis for a rigorous 'everyday' proof, so long as you make explicit the role of the $\forall A(G(A,A))$ hypothesis. If you haven't been given an explicit formal deduction system to work with that should be enough.

5. Jun 23, 2012

### stauros

The proof as i said is an ordinary proof in predicate calculus with the usal 4 general laws i.e

1) Universal Elimination
2) Universal Introduction
3) Existential Elimination
4) Existential Introduction

Plus the rules of statement calculus

6. Jul 7, 2012

### xxxx0xxxx

Well, we ain't supposed to be doing homework problems here, but the proofs are extremely simple.

for proof 1: Your notation is inconsistent, so can't help until you clean that up.

for proof 2: $$\forall A (H(A,c) \Rightarrow H(P(A),c))$$
Assuming A, H(A,c), and P(A) exist immediately gives result H(P(A),c) from b 1 and 2.

7. Jul 14, 2012

### stauros

Sorry to ask but do you know how a proof is done in predicate calculus?

I mean have you done any predicate calculus?

8. Jul 19, 2012

Um yeah ...