Assign 5 quest 2 part d) solution

[Adrian Nicoara]

I was going over the solutions for past assignments.
I have a question regarding the solution for ex 2 part d of assign 5:
From lines 7 to 12 of the proof, would it not be easier to introduce:

7 ? y . (x,y) in S Domain 6
8 ? y . (x,y) in R /\ not (x in dom S) \/ (x,y) in S \/_I 7

and then continue the proof the same way?
Or is that an invalid step?

Thanks.

[Nancy Day]

Post by Adrian Nicoara
I was going over the solutions for past assignments.
7 ? y . (x,y) in S Domain 6
8 ? y . (x,y) in R /\ not (x in dom S) \/ (x,y) in S \/_I 7
and then continue the proof the same way?
Or is that an invalid step?

That's an invalid proof step because to use \/_I you have to \/ a wff with
the entire line. You can't change something inside the scope of
a quantifier. Recall that all natural deduction proof steps must
be applied to the entire line. I showed an example in one of the
lectures on natural deduction of how applying a nat ded rule to
only part of the line can give you an invalid result.

Transformational proof is the one where we can apply the rules to
subformulas.

cheers, nancy
--------------------------------------------------------------------
Nancy Day, Associate Professor
CS245 Winter 2009 Instructor
http://www.student.cs.uwaterloo.ca/~cs245
David R. Cheriton School of Computer Science, University of Waterloo

[Adrian Nicoara]

Right, got it now.
Thanks :)

Post by Nancy Day

Post by Adrian Nicoara
I was going over the solutions for past assignments.
7 ? y . (x,y) in S Domain 6
8 ? y . (x,y) in R /\ not (x in dom S) \/ (x,y) in S \/_I 7
and then continue the proof the same way?
Or is that an invalid step?

That's an invalid proof step because to use \/_I you have to \/ a wff with
the entire line. You can't change something inside the scope of
a quantifier. Recall that all natural deduction proof steps must
be applied to the entire line. I showed an example in one of the
lectures on natural deduction of how applying a nat ded rule to
only part of the line can give you an invalid result.
Transformational proof is the one where we can apply the rules to
subformulas.
cheers, nancy
--------------------------------------------------------------------
Nancy Day, Associate Professor
CS245 Winter 2009 Instructor
http://www.student.cs.uwaterloo.ca/~cs245
David R. Cheriton School of Computer Science, University of Waterloo