4(b) (with Wheels Fell Off condition)

I don't have numbers for the lines yet, but here's the bones of my current strategy.

Exists-x (~P(x) || Q(x)) ......... premise. (I'm pretty sure that's right. )

Open up an "Arb-Box"... x₀ ~P(x₀) || Q(x₀)
.... deal with the cases here? Or take it to the next level?

Open up a box in which to get a contradiction of P(x₀) && Q(x₀)
...
...
It ends in "bottom".

So after that inner box we have ~ P(x₀) && Q(x₀) ....... ~i (the previous box)
....
This is a "Chi" to end the exists-+-"arb-that-exists" box, so we're allowed to take it out? ... This is NOT such a "Chi", is it? A little bell rings saying you can't use the arbitrary x in your Chi....

OK. Enough doubt! Carry on.

The idea Was, come out of the box with ~ P(x) && Q(x), which I'm almost certain is wrong.

Obviously were it not wrong, one would easily move from there to "Exists" to reach the conclusion sought.

There you go. I won't edit this. Mistakes are often far more interesting than correct answers.

Hmm ... Looking at it, I already see a whole bunch of extra "unforced errors" there. Well let them also be... The most interesting critique will obviously be the one that goes to the very root of it all, though, obviously.

Doh!

It's Q 9.5 of Assignment 2! (Which I got wrong).

The brief version here is :
1. Chi must be free of arbs. It must be a "plain-var" expression.
2. This is very easy to obtain in the same box in which you got your ~i from "bottom". You have an expression Phi[x₀/x] so on the next line you're entitled to use "exists i", using that Phi.

I'll leave it all cryptic or in a total mess like this so as to leave a good problem to practice solving on (as long as you've managed to forget what was in the assignments).

Ok, here goes my attempt:

Line 1: there exists x ( ~P(x) || Q(x))
Line 2: x0. ~P(x0) || Q(x0). Assumption. x0/x
Line 3: ~P(x0) assumption
Line 4: (P(x0) and ~Q(x0). Assumption
Line 5 P(x0). And e 4
Line 6: bottom ~e3,5
Line 7: ~(P(x0) and ~Q(x0)) ~i4-6
Line 8: Q(x0). Assumption
Line 9: P(x0) and ~Q(x0)
Line 10: ~Q(x0) and e 9
Line 11: bottom. ~e8,10
Line 12: ~(P(x0) and ~Q(x0)) ~i 9-11
Line 13: ~(P(x0) and ~Q(x0)). ||e 2, 3-7, 8-12
Line 14: there exists x of the above line ....exists x I 13
Line 15: same as line 14 ... Exists x e 1, 2-14

That was my go, sorry for late reply slow, I was tryibg to figure out all my mistakes in the assignments yesterday. Wasn't pleased with my assignm marks.

Thanks for the feedback, Tazz.

Assuming the various boxes open and close at the appropriate places, I'd say your solution is right. It's also different to the one given for the assignment, so it might be interesting for you to examine where you differ. (Many ways to skin a cat).

I got this one wrong in the assignment. My mistake was to leap out of the box with an x₀, which is not allowed. The box is there mainly to restrict the scope of that x₀, so we can't have the thing jumping out then.

In other words the essence of either proof (your one, or the other alternative from the answer book) is that one must first use "exists-e" to move from the substitution line to a pure x line as in your line 14. Once one has a line 14 like yours, one has a suitable Chi to take out of the box.

Splendid! No flies on you!