Assignment 2: Question 9

Ok, it's becoming more apparent that I'm going to have to do a tonne of work to pass this module.

For 9.1, how does one change the 'not P' into a 'P' in the goal? I feel like I'm missing something simple here because it's only supposed to be 5 marks...

Any advice would be awesome Thanks

Ok, don't worry - I think I know what I'm doing now. But yeah - still sooooo much work to put in I think...

Did you manage it?

I think there's a mistake in the question. I think the premise should have been: 'for all' (¬ P(x) V Q(x)).

In fact, on page 29, you can see just that. Examine the second to last provable equivalence on the right.

GerritB Wrote:
-------------------------------------------------------
> Did you manage it?

I managed it. The trick with these is to work forwards and backwards and then you only need to deal with a few lines in the middle.

9.5 made me scratch my head for a bit though

> I think there's a mistake in the question. I think
> the premise should have been: 'for all' (¬ P(x) V
> Q(x)).
>
> In fact, on page 29, you can see just that.
> Examine the second to last provable equivalence on
> the right.

Those formulas are equivalences, whereas this one might not be and is a sequent that you need to prove.

9.1 - I got there in the end by introducing a contradiction.

@ra - 9.5 is a head scratcher for me too...

Just wanted to let you know that this is an awesome resource for examples of how to do formal proofs with quantifiers.

For 9.5, the tricky bit is getting from R(a) to Q(a) in the Ve of Q(a) v R(a)
Assuming R(a) and you have P(a) from a previous step, you can use conjunction, then intro E.
This contradictes the second premise. So then just conclude Q(a).

Hope this helps.

_____________________________________
The sun is always shining, but it is far away.