Classical logic without negation and falsehood It seems to me that Gerhard Gentzen's sequent calculus could just omit negation and falsehood, and still prove any classical tautology in a suitable form. (For a specific formula, falsehood gets replaced by the conjunction of all relevant propositional variables. For predicate logic, falsehood gets replaced by the conjunction of the universally quantified predicate symbols, including for example $\forall x\forall y\ x=y$. One could also introduce a constant $F$ and axioms like $F\to\forall x\forall y\ x=y$. More details about the consequences of removing falsehood can be found here.) This doesn't seem possible for his natural deduction calculus, where the law of excluded middle is used to arrive at classical logic.
Why hasn't he adapted the relevant rule from his sequent calculus to his natural deduction calculus:
$\begin{array}{l} A\to(B\lor C) \\
\hline (A\to B)\lor C\end{array}$
At first sight, this rule doesn't look worse than
$\begin{array}{l}  \\
\hline A \lor \lnot A\end{array}$
or
$\begin{array}{l} \lnot \lnot A \\
\hline A \end{array}$, and it would have mirrored his sequent calculus more closely. Of course, in the sequent calculus he didn't need to write $\lor$, and this made this deduction rule look even more attractive. But being able to omit both negation and falsehood seems attractive to me, independent of how attractive the rules themselves appear.
The only reason I could come up with is that he developed his natural deduction calculus first, became dissatisfied with it, then developed his sequent calculus, and didn't find it important to further improve his natural deduction calculus, because it had other irreparable flaws anyway.
 A: First, I would like to strongly disagree with the third sentence of your recent comment - just because (basically) the same proof system is complete for a restricted logical language when restricted appropriately, doesn't mean that that restricted logic is in any way similar to what you started with. This becomes especially clear once we consider the semantics - e.g. if $T$ is a first-order theory without negation, then it has a model (consisting of one element, with all relations total), so there are no inconsistent theories at all. It's also evident if we consider the algebraic structure of a logic.
This isn't to say that this fact isn't interesting - just that it shouldn't be overstated.
Second, as to why Gentzen didn't do this: of course this is speculation, but I believe Gentzen was already interested in full first-order logic, and was trying to develop a proof theory for that. I think Gentzen would have viewed negation as a natural part of first-order logic, and seen no reason to get rid of it. Note that his interest in intuitionistic logic (e.g. http://gdz.sub.uni-goettingen.de/dms/load/img/?PID=GDZPPN002044374) doesn't really contradict this, since weakening the laws around negation isn't really getting rid of negation so much as analyzing it. Of course, this is mostly speculation on my part - I'm asserting a negative - but I think Gentzen wouldn't have seen much of a point to omitting negation in this way, and so (if it occurred to him) didn't do it.
