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

Answer 2

The structure of your deduction is reasonable, but there are steps missing to take you from the quantified statements to a particular and then back to quantified.

It is not correct to say that P-->Q is "equivalent" to the first premise: that's misrepresenting a predicate statement as a propositional statements. What you can say is that if the first premise holds true for all x, then it is certainly true for one specific x. So universal instantiation of the first premise can give you P(a)-->R(a). Similarly, since the third premise tells us that there is at least one x such that Q(x), we can say let's call one of those x's "a" and so claim Q(a).

Once you get to the point where you have proved R(a) you can then use existential generalisation to get your final conclusion.