When can I discharge an assumption? or better put, When can I not discharge an assumption?

Question

It's homework, so I won't give the example, but when is it legal for me to discharge an assumption? Basically, I'm introducing a conditional to prove a theorem that does not rest on any assumptions, and I want to make sure the consequent follows from the antecedent. But, I had to use two reductio ad absurdum arguments to get there, and I feel like I'm stuck with an assumption that was necessary to set up the contradiction. Any advice, or should I just keep at it? Is it legal to include the main assumption in the line that has the contradiction in an reductio ad absurdum argument???

My Professor answered the question about whether lines 1-4 were legal, but he did not get back to me regarding how legal lines (11) and (12) were (90 students worth of homework to grade probably).

Any guidance on how to discharge all my premises or any rules to look at in the Fitch style with the limitations my professor gave us??

Also, I'm not allowed to sequent introduction or use theorem introduction.

I'm having trouble making sure not only that the consequents of every conditional I introduce is generated by the antecedent + making sure that line (1) plays a role in generating line (11) while discharging all my assumptions.

Ultimately, line 12 not resting on any assumptions seems wrong by the way I did it. Please help.

That's basically my problem.

Thanks LemonTree!! I was able to make a formal proof for it.[

Also, Lemontree, I added line I was missing, and I fixed the furthermost right column. Thanks!

Answer 1

In general, the conclusion will depend on all assumptions not discharged by the end. In particular, your conclusion still depends on the assumptions A -> B (your line 4 is not an actual application of (- I), so that assumption is not discharged), B -> A and -(A -> B).
Assumptions may be discharged exactly in the cases the rules tell you: The antecedent in a (-> I), the unnegated assumption in a (- I), the negated assumption in a (RAA), the disjuncts in a (v E).

Try to approach your proof more systematically. For example, on lines 3 to 5 you are deriving A -> B... from the assumption A -> B, which you already have on line 2. You can spare yourself this kind of detour and just work with the assumption straightaway. Always keep in mind what you're currently trying to prove.
Your current approach won't lead to success, because you never actually derive a contradiction that would make it possible to introduce a negation which allows you to discharge an assumption.

It is a useful technique to work by the hourglass strategy: Start your proof backwards, disassembling the conclusion by reverse applications of introduction rules on the main operator until you can get no further, then switch to the top and work your way down from the premises by successive applications of elimination rules until you hopefully meet in the middle. Eventually, you will have a kind of hourglass shape on the complexity of formulas, with long-ish formulas (the premises) on the top, successively dissected by elimination rules to smaller pieces in the middle, followed by introduction rules reassembling the information back to a new complex formula (the conclusion) at the bottom. First half (E) rules, second half (I) rules. This is what most non-detoured natural deduction proofs will look like, and it helps in finding your proof to try and achieve that shape.

You want to prove a conditional -(A -> B) -> -(A <-> B), so the last step to have happend is likely an application of (-> I). (-> I) means you assume the antecedent (-(A -> B)) and from that derive the succedent (-(A <-> B)), after which you can discharge the assumption -(A -> B).
Next on how to derive -(A <-> B). The main operator is a negation, so the second-to-last step is likely a (- I). That means you assume the unnegated formula A <-> B, derive a contradiction from it, and hence conclude the negation -(A <-> B), thereby discharging the assumption A <-> B.

Informally, the proof proceeds as follows:

• Assume -(A -> B).
• Assume A <-> B.
• Then in particular, A -> B.
• But by assumption -(A -> B); contradiction.
• So the assumption A <-> B must have been wrong, and it holds that -(A <-> B).
• Since if -(A -> B) then -(A <-> B), we have -(A -> B) -> -(A <-> B).

Can you translate this into a formal proof?

Also, you should probably explicitly mark your subproofs as such by adding indentation and vertical lines every time you open a new assumption level and visually exit it once the assumption is discharged (but this depends on how your teacher introduced the notation).

Answer 2

The Natural Deduction rules for discharging an assumption are

1. Conditional Introduction: Derive Q in that context of assumption P, Discharge that assumption to infer P -> Q. This is a Conditional Proof.

   2     P       Assumption
   1(,2) Q       Derived in context of 1 and possibly 2
   1     P -> Q  Conditional Introduction: discharge assumption 2 to infer in context of 1
   

Note The derivation of Q is usually in the raised context as well as the lower, but technically need only be in the lower context. However, some proof checkers will insist that it does have to be in both, in which case the rule of Reiteration may be of use.

2. Negation Introduction: Derive a contradiction under assumption of P, discharge that assumption to infer ~P. This is an Indirect Proof.

   2      P       Assumption
   1(,2)  #       a contradiction/falsum derived in context of 1 and possibly 2
   1      ~P      Negation Introduction: discharge assumption 2 to infer in context of 1
   

3. Negation Elimination: Derive a contradiction under assumption of ~P, discharge that assumption to infer P. This is a Proof by Reduction to Absurdity / Reductio Ad Absurdum (RAA).

   2      ~P      Assumption
   1(,2)  #       a contradiction/falsum derived in context of 1 and possibly 2
   1      P       Negation Elimination: discharge assumption 2 to infer in context of 1
   

Note: Some systems call the rule to 'eliminate' a double negation by name of Negation Elimination. In such systems a proof by RAA is just a combination of Negation Introduction and this rule.

   2      ~P      Assumption
   1(,2)  #       contradiction/falsum derived in context of 1 and possibly 2
   1      ~~P     Negation Introduction: discharge assumption 2 to infer in context of 1
   1      P       (Double) Negation Elimination

---

I've used # as a falsum symbol, indicating that any contradiction will suffice. These are usually derived by conjunction introduction of two contrary statements.

---

So, to derive `~(A > B) > ~(A <> B)

   (1)  1    ~(A > B)                Assumption 1
   (2)  2    (A <> B)                Assumption 2
   (3)  2    (A > B) ^ (B > A)       <> Elimination (2)
   (4)  2    (A > B)                 ^  Elimination (3)
   (5)  1,2  (A > B) ^ ~(A > B)      ^ Introduction (1,4)
   (6)  1    ~(A <> B)               ~  Introduction (2,5) discharges assumption 2
   (7)  .    ~(A > B) > ~(A <> B)    > Introduction (1,6) discharges assumption 1