Rules for discharging subproofs

[ibenami]

When discussing the scope of subproofs - It is stated and explained "Any rule whose citation requires mentioning individual lines can mention any earlier lines, except for those lines which occur within a closed subproof." Examples are given of citing lines that are within a subproof from outside a subproof, and called 'naughty'. However, when using the Conditional Introduction Rule, while 'discharging' a subproof, that line clearly cites lines from within the subproof. There is no mention of why this is allowed in those circumstances - especially since the Conditional Introduction Rule is not formulated with regard to a subproof (contrast to this definition in SL from "The Logic Book" by Bergmann et al:) Whereas in our book, it defines the Conditional Introduction Rule all within one scope. Perhaps this should be addressed somehow? (I am only a beginning student of logic, not an expert, but this seems unclear to me).

[rzach]

->I cites the beginning and ending lines of the subproof, with a dash between, e.g., the ex on p. 109 cites ->I 2-4. The prohibition is against citing individual lines in closed subproofs, as eg the "naughty" ->E 5, 4 in that example. Does that clear it up?

Should we add a sentence after the box at the top of p. 110 to make this explicit (eg, "Note that this prohibition applies to citing individual lines within closed subproofs. Of course, we can cite the entire subproof (from its first to its last line) after it is closed, as we do on line 5 of the preceding example. However, subproofs may themselves occur in closed subproofs, and then we can no longer cite them; see below.")?

The ->I rule (p. 107) is the same as the one in the Logic Book. Can you elaborate what you have in mind?

[ibenami]

(Sorry, you are right - the Conditional Introduction rule is the same as the other book).

You write

Of course, we can cite the entire subproof (from its first to its last line) after it is closed,..

To me it is this implicit rule (or exception?) of being able to cite the entire subproof which is confusing.It raises some more questions as well -

• Does it have to be the entire subproof that is cited?

• If I have a proof, with a subproof , spanning lines 10-15. I cite the entire subproof with a Conditional Introduction in order to assert that line 10 implies line 15.

  • Can I later cite the subproof again to show that line 10 implies line 13?
    • (Shouldn't be a reason not to logically, but i'm not sure what the rules here are. Do I have to restate the entire subproof and stop at 13?)
  • Can I use it with another subproof with the Disjunction Elimination Rule?

  (I also don't think that differentiating citing individual lines from citing the whole subproof solves the problem - the I could just cite the whole proof and Reiterate some line within it?)

It seems to me that the rule at this point is that the inside of a subproof cannot be cited from outside of it, unless it is specifically used with the Conditional Introduction or the Disjunction Elimination?

Whatever the rules are they seem to me implicit and not so obvious, especially when the rules are seemingly "broken" even within the very discussion of those rules. To me at least it would be clearer if these exceptions were somehow spelled out (even though I am aware of how and why they work in practice - just as the discussion on parentheses, which may seem "obvious" but may be important to spell out)

Thanks!

[rzach]

I have added some additional discussion which I hope makes all the conditions for citing lines and subproofs clear. (The answer to your questions are: no and yes. ->I requires that the last line of the subproof be the consequent of the conditional proved. But you're right and there is no logical reason why you couldn't allow it as long as line 13 is on the same scope line as line 10.) The rule you mentioned, that the inside of a subproof can't be cited from outside of it, is in section 15.5.