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:
| Pa (∃I 1, flag a)
Q -> Pa (2-3 conditional proof)
∃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.