Don't even understand what it is trying to say: Predicate calculus

Hi, I have a question (natural deduction),

and the question says :

construct a natural deduction proof, where y is not free in A. What does it mean by 'where y is not free in A'?

This question shall not use algebraic laws. Just introduction and elimination rules.

Thank you.

Re: Don't even understand what it is trying to say: Predicate calculus

Quote:

Originally Posted by

**gomdohri** What does it mean by 'where y is not free in A'?

You need to consult your source (textbook or lecture notes). They must have a definition. Or see here in Wikipedia.

Do you need a Fitch-style or tree-like natural deduction derivation?

Informally, the derivation looks as follows.

1. Assume E y. ( A -> P(y)).

2. Assume A.

3. From 1 take y and the proof of A -> P(y) (existential elimination).

4. From 2 and 3 conclude P(y) by MP.

5. From 4 conclude Ey. P(y).

6. Close the assumption A from 2.

Note that to prove the converse implication you need to use the rule of double-negation elimination or the law of excluded middle.

Edit: After you construct a formal derivation, make sure you understand where the assumption that y is not free in A is used. This is the point of the exercise. If you need help with this, feel free to ask.