Digressing from issues about the choice of language(s), another post about principles for selecting among natural deduction systems — another choice point, and (though I suppose relatively minor) one not considered by Pelletier and Hazen.
Take the most trite of examples. It’s agreed that if P then R. I need to convince someone that if P and Q then R (I’m dealing with a dullard here!). I patiently spell it out:
We are given if P then R. So just suppose that P and Q. Then of course P will be true, and hence (given what we agreed) R. So our supposition leads to R, OK? – hence as I said, if P and Q then R.
You want that set out more formally? Here goes, indenting sub-proofs Fitch-style!
Job done!
Except that in many official versions of Fitch-style proofs, this derivation is illegitimate. We can’t appeal to the initial premiss at (1) in order to draw the modus ponens inference inside the subproof: rather, we have to first re-iterate the premiss in the subproof, and then appeal to this reiterated conditional in applying modus ponens.
This requirement for explicit reiteration seems to go back to Jaśkowski’s first method of laying out proofs; and it is endorsed by Fitch’s crucial Symbolic Logic (1952). Here are some other texts using the same graphical layout as introduced by Fitch, and also requiring inferences in a subproof to appeal only to what’s in that subproof, so that we have to use a reiteration rule in order to pull in anything we need from outside the subproof: Thomason (1970), Simpson (1987/1999), Teller (1989).
Now, such a reiteration rule has to say what you can reiterate. For example: you can reiterate items that occur earlier outside the current subproof, so long as they do not appear in subproofs that have been closed off (and then, but only then, these reiterated items can be cited within the current subproof). But it is less complicated and seems more natural not to require wffs actually to be rewritten. The rule can then simply be: you can cite “from within a subproof, items that occur earlier outside the current subproof, so long as they do not appear in subproofs that have been closed off” — which is exactly how Barwise and Etchemendy (1991) put it. Others not requiring reiteration include Hurley (1982), Klenk (1983) and Gamut (1991). (Bergmann, Moor and Nelson (1980) have a rule they call reiteration, but they don’t require applying a reiteration rule before you can cite earlier wffs from outside a subproof.)
So: why require that you must, Fitch-style, reiterate-into-subproofs before you can cite e.g. an initial premiss? What do we gain by insisting that we repeat wffs within a subproof before using them in that subproof?
It might be said that, with the repetitions, the subproofs are proofs (if we treat the reiterated wffs as new premisses). But that’s not quite right as in a Fitch-style proof it is required that the premisses be listed up front, not entered ambulando. So we’d have to re-arrange subproofs with the new supposition and the reiterated wffs all up front: and no one insists that we do that.
Anyway: at the moment I’m not seeing any compelling advantage for going with Fitch/Thomason/Simpson/Teller rather than with Barwise and Etchemendy and many others. Going the second way keeps things snappier yet doesn’t seem any more likely to engender student mistakes, does it? But has anyone any arguments for sticking with a reiteration requirement?
Here is another discussion to which I came late because of the holidays. I see no reason at all to worry about these matters: Dag Prawitz devised in the early 1970s a notation for linear derivations in natural deduction, inspired by Copi’s book, found in his Swedish compendium “ABC i symbolisk logik” that I used in my teaching for decades. The notation is found in my “Elements of Logical Reasoning” (CUP 2013), and there is a translation algorithm from linear to tree derivations, the latter exactly those of Gentzen’s original system of natural deduction. The translation is an important pedagogical device for the learning of tree derivations. Consider, now, what it gives: Any linear derivation in Prawitz “ABC” style translates into a correct tree derivation in Gentzen style. There is nothing at all to discuss or ponder about left.
I suppose I could add to my first paragraph that S5 permits ‘pulling in’ any statement P from outside to become “◇P” under the “⬜”. Intuitively, this is because if P is true here then in any world (the “⬜” denotes that context) one must admit that P is possible. So immediately we get a Fitch-style system for S5 in a natural way from the intuitive idea, and it also gives a neat illustration of a non-trivial reiteration rule.
I agree that it is silly to require reiterating a statement just because it is ‘pulled into’ a subcontext, in classical logic, because here the whole notion of subcontext means that whatever is true in the surrounding context is of course true inside a subcontext as well. There are nevertheless two issues. Firstly, if you introduce a subcontext for universally quantified variables, then not every statement can be pulled into it, due to name conflict. Variable shadowing does not solve this. Secondly, if you wish to extend Fitch-style proof to non-classical logics, then it is no longer true that you can always ‘pull in’ any statement deduced outside. The simple modal logic S4 can easily be captured by a Fitch-style system, but clearly deduced statements cannot always ‘pulled under’ the “⬜”, since it is not a subcontext but rather a different context.
Therefore, for pedagogical sake reiteration should be non-compulsory as it is simply wasting time and space and energy, but it is in some sense not trivially silly when it comes to non-classical logics.
Here is a rather off-the cuff reaction to the query, which may miss the point; if so, apologies.
Consider the tautology p->(q->p). To derive it, first suppose p, then suppose q. Now, if we can reiterate p we simply do so and then apply CP twice. But if we can only cite p, in the sense of appealing to it as a premise in the application of a rule, and not stating it as an end in itself then, unless we have a primitive rule of identity, we are going to have to go through some hoops to get p. One contortion would be to conjoin the first supposition with the second, and then strip off the second one. OK, it works, but it is inelegant.
I agree that a permissive rule that allows reiterations is desirable (after all, you want to be able to warrant P, so P without going through hoops, as you say!).
But my concern — and I’ve edited very slightly to make this clearer (sorry!) by changing “reiteration rule” to “reiteration requirement” a couple of times — was with the Fitch-style insistence that you must re-iterate into a subproof before you can e.g. appeal to an initial premiss there.
Maybe the reason has to do with computer programming? The easiest way to mark a line as useable might be to repeat it within a subproof? Premises are always useable, so no need to mark them as such, but as soon as a proof contains subsubproofs it may get more difficult for an algorithm to track what is useable and what isn’t.
By the way, what do you think of other slight differences between rule system for Fitch-style ND. For example, is there a single rule for conjunction elimination or a left-elimination and a right-elimination rule? Or may one add as line 6 to the toy example $latex (P\wedge Q)\rightarrow P$? It seems pointless to require an additional subproof to get to this line, but strictly speaking standard formulations of conditional intro don’t allow to add this line since the last line of the subproof is R and not P.
1) But isn’t it exactly as difficult for an algorithm or a student to track what can be reiterated-and-then-cited and track what can be cited (without being actually rewritten)?
2) As to whether there a single rule for conjunction elimination or a left-elimination and a right-elimination rule, I guess this really is a mere matter of presentation — a double-barrelled rule or two rules, who’s counting? :)
3) Yes you are right, in a standard system, once Conditional Proof has been invoked, the initial supposition has been discharged and can’t be used again, so to derive another conditional with the same antecedent you’d need to start a second subproof with the same supposition again (and indeed maybe repeat some of the same line of derivation). I suppose you could have a Multiple Conditional Proof rule that says, given a subproof starting with supposition $latex A$, then you can finish the subproof, discharge the supposition, and infer in one fell swoop any and all of the conditionals $latex A \to C_n$ for as many of the wffs $latex C_n$ in the subproof that you like. But how often would this short cut rule to avoid multiple subproofs for conditionals with the same antecedent ever be used? So here, a general desire to keep rules simple wins, I think!