Natural Deduction flagging system (Virginia Klenk)

Question

I am wondering if anyone can clarify a detail that's been bugging me. Here are the flagging restrictions for Virginia Klenk's natural deduction system:

RI. A letter being flagged must be new to the proof; that is, it may not appear, either in a formula or as a letter being flagged, previous to the step in which it gets flagged.

R2. A flagged letter may not appear either in the premises or in the conclusion of a proof.

R3. A flagged letter may not appear outside the subproof in which it gets flagged.

I am not sure if R3 includes subproofs introduced by use of assumptions for conditional and indirect proof.

If we have, for example:

1. ∃xPx (premise)

   __________Assumption

2. | Q

3. | Pa (∃I 1, flag a)

   ---

4. Q -> Pa (2-3 conditional proof)

5. ∃x(Q -> Px) (4 ∃G)

Is this a legal move? I recognize 5 follows logically from 1 here, but I'm wondering if the move at line 4 is allowed in this system. That is, make an assumption, apply ∃I, discharge. (R2 eliminates the possibility of an existentially instantiated variable occurring in the conclusion of any finished proof.) The way in which "subproof" was used in the chapter leads me to suspect she means only "flagged subproof", as opposed to conditional/indirect subproofs but I can't tell for sure.

Answer 1

Indeed you cannot raise the flagged variable inside the conditional proof if you intend it to occur outside that context.

Rather, you must introduce it earlier, then reiterate into the subproof.

 1.|_ ∃x Px         Premise
 2.|  Pa            Existential Instantiation 1, flag [a]
 3.|  |_ Q          Assumption
 4.|  |  Pa         Reiteration 2
 5.|  Q -> Pa       Cond. Proof 3-4
 6.|  ∃x (Q -> Px)  Existential Generalisation 5

It may seem a minor detail, but the rules are very strict. Validity is only maintained by following them precisely.

RI. A letter being flagged must be new to the proof; that is, it may not appear, either in a formula or as a letter being flagged, previous to the step in which it gets flagged.

Check: The variable 'a' does not occur prior to line 2.

R2. A flagged letter may not appear either in the premises or in the conclusion of a proof.

Check: The variable does not occur on line 1 (premise) or line 6 (conclusion)

R3. A flagged letter may not appear outside the subproof in which it gets flagged.

Check: The 'subproof' in which it is flagged is the proof itself.

Further: it was flagged with an existential instantiation, so may be validly be used for existential generalisation.