I have attempted to solve the following but I have no means to check it....or does wolfram do this ? I do not know if my handling of the operators (scope) is occrect...do you know? for all x: upended A operator (universality)
there exists an x: inverted E operator (existence)
for all x(P(x) -> R(x)), for all x(P(x) v not_Q(x)); there exists an x(Q(x)) hold under partial correctness: there exists an x(R(x))
proof:
I disagree with @MattClarke in that the structure of your reasoning is reasonable. It does not adhere to the rules of natural deduction. For example, your boxed proof assumes
Q
and~Q
(I am using~
for negation) and concludesP
. But there is no natural deduction rule that allows you to use more than one assumption inside a box (and even if there was, and such a rule could be justified, then the result of the boxed proof is not justP
as you seem to claim, but rather the implication(Q /\ ~Q) --> P
, which is trivial, since there is already a natural deduction rule that allows us to deduce anything from a contradiction).From the OP it is not really clear to me what exactly you want to prove. I am just assuming that from the three premises
ALL x. (P(x) --> R(x))
,ALL x. (P(x) \/ ~Q(x))
, andEX x. Q(x)
you want to proveEX x. R(x)
.Since the formula you want to prove starts with an existential quantifier it will be obtained by exists-introduction. But first we start with the premises:
The rule for exists-elimination opens a box (boxes will be indicated by braces
{
and}
) and allows us to conclude a formula that is provable under the assumption that there is a witness for the existential formula to which the rule is applied, i.e.,at this point we apply a disjunction-elimination which amounts to the case analysis whether
P(y)
holds or~Q(y)
holds (at least one of which has to be true since we haveP(y) \/ ~Q(y)
). Each case gets its own box