# Is the following a correct logical proof?

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

∴ P

1.     assume ~P
2.         assume A
3.         F ∧ P (1, 5, modus ponens)
4.         P (6, simplification)
5.     ~A (4, 7, reductio ad absurdum)
6.     S ∧ R (2, 8, modus ponens)
7.     R (9, simplification)
8. 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.

• This comment is written under the assumption that your formal system works as the ones that I see the most often. If this isn't the case, you should specify exactly what rules you have and how they work. "Am I allowed to use the outer assumption towards negating my inner assumption?" If I understand your question, you are allowed to, yes. But the proof is wrong because $\neg A$ should have been derived outside the subproof starting at line 5. Then at the last step $P$ should be derived outside of $\neg P$ after deriving $\neg \neg P$. – Git Gud Aug 11 '15 at 19:31
• I see what you mean and have edited step 8 accordingly. Otherwise, this is essentially in line with what I learned in Gensler. – readyready15728 Aug 11 '15 at 20:06
• " Then at the last step P should be derived outside of ¬P after deriving ¬¬P." That all depends on the system involved. In some systems, if you can derive a contradiction, then you can discharge a negation into the complementary literal. CCNpKqNqp, and CCNpqCCNpNqp both come as tautologies which back up using such a rule of inference. – Doug Spoonwood Aug 13 '15 at 11:05

## 3 Answers

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.

• I have changed the indentation once more to fit a certain recommendation. As far as inference is concerned, this is exactly what I learned in Copi and, later, Gensler. I don't know whether there's a name for this particular style but the inferences are valid in the logical sense, so I will leave it be otherwise. – readyready15728 Aug 12 '15 at 19:28

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

But we are given ~R.

Therefore A.

• This doesn't answer the question. – Doug Spoonwood Aug 11 '15 at 21:36
• Given that we're doing proof by contradiction, it is entirely fitting that we can draw contradictory inferences from the starting assumption. – readyready15728 Aug 12 '15 at 20:17
• I don't see how this answers the question either. We are trying to derive P not A. – Frank Hubeny Feb 21 at 2:56

The OP has the following question:

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?

Line 4 is outside the subordinate proof starting on line 5. Lines 4 and 7 are contradictory which is what we want. However, one needs to add a new line which shows that contradiction in the subordinate proof. Then one can discharge the assumption $$A$$ on line 4.

Line 8 is likely incorrect without that extra line. However, that brings up the next question the OP has:

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.

One way to verify that a technique is correct is to use a proof checker. Such software will force the user to conform to its format requirements and rule justifications. However, that implementation of natural deduction inference rules need not be the only way those rules could be implemented.

Here is the proof in one proof checker: Note that line 8 is replaced by a symbol for contradiction (⊥). Some proof checkers may ask that this be entered as P ∧ ¬P.