Is the following a correct logical proof?

Question

1. A → (F ∧ P)
2. ~A → (S ∧ R)
3. ~R

∴ P

4.     assume ~P
5.         assume A
6.         F ∧ P (1, 5, modus ponens)
7.         P (6, simplification)
8.     ~A (4, 7, reductio ad absurdum)
9.     S ∧ R (2, 8, modus ponens)
10.     R (9, simplification)
11. P (3, 10, reductio ad absurdum)

The focus for my doubt here is at step 8 where I use the initial assumption at line 4 and the derivation of its negation at line 7 to infer that ~A is in fact the case given the two assumptions. My question is really: am I allowed to use the outer assumption towards negating my inner assumption?

I realize this can also be done by assuming A in the proof and then going from there, I just wanted to make sure this technique is licensed in general.

Answer 1

From ~ A → (S ∧ R), ~(S ∧ R) → A or ((~S) $\lor$ (~R)) → A.

But we are given ~R.

Therefore A.

Answer 2

Every step almost ends up as correct up to a point.

The last line needs to have the same scope as the set of premises {1, 2, 3}. That is the only incorrect step.

Yes, you can use the outer assumption towards negating your inner assumption. Natural deduction systems assume a rule of repetition which allow you to repeat any assumption from an outer domain in a domain within that outer domain (the term 'domain' here as I recall originally got used by Jaskowski). Or if they don't assume a rule of repetition, they assume that any formula in an outer domain can get used to derive a formula in an inner domain. This works more in natural deduction systems with axioms.

All natural deduction systems either have the formula (p $\rightarrow$ (q $\rightarrow$ p)) as an axiom or as a theorem. This allows you to use an outer assumption $\alpha$ and re-derive $\alpha$ within the scope of the inner assumption using modus ponens twice.

Thus, you can derive the contradiction within the scope of your assumption 'A' and thus discharge it using reductio ad absurdum. That is, every step of your proof comes as valid up to a point.

That doesn't quite answer if this consists of a correct proof though, because in order to determine whether or not we have a correct proof, we need to have the exact definition of what a proof consists of for this formal system.

Additionally, you have many steps which are NOT correct in another sense. They qualify as correct up to a point, but I do say confidently that they don't fit the definition of a proof. A proof consists of a sequence of well-formed formulas which follow the formation rules exactly. But, many of the sequences of symbols that you have written are simply NOT well-formed formulas. And thus, your proof only works as correct up to a point.

That said, I'm sure someone would try and argue that converting what got written above can get converted to a proof easily and thus the above comes as "convincing" enough to qualify as a proof. But, a proof consists of something objective, and since you haven't written well-formed formulas and opted for abbreviations, you haven't written something which satisfies the definition of a proof.