Natural deduction: is this a sound proof?

Question

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:

Answer 1

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 concludes P. 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 just P 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)), and EX x. Q(x) you want to prove EX 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:

 1 ALL x. (P(x) --> R(x)) premise  
 2 ALL x. (P(x) \/ ~Q(x)) premise  
 3 EX x. Q(x)             premise

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.,

 4 { for an arbitrary but fixed y that is not used outside this box
 5 Q(y)                   assumption  
 6 P(y) \/ ~Q(y)          ALL-e 2

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 have P(y) \/ ~Q(y)). Each case gets its own box

 7 {  
 8 P(y)                   assumption  
 9 P(y) --> R(y)          ALL-e 1  
10 R(y)                   -->-e 9, 8  
11 }  
12 {
13 ~Q(y)                  assumption  
14 bottom                 bottom-i 5, 14  
15 R(y)                   bottom-e 15  
16 }  
17 R(y)                   \/-e 6, 7-11, 12-16  
18 EX x. R(x)             EX-i 17  
19 }  
20 EX x. R(x)             EX-e 3, 4-19