# 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.

• What reason would he have to want to omit negation and falsity? Jun 1, 2016 at 23:59
• @NoahSchweber Robinson arithmetic omits induction, and is still recursively incompletable and essentially undecidable. This shows that induction is not responsible for those phenomena. You can omit negation and falsehood, and still get essentially the same classical logic. This shows that negation itself is not responsible for the interesting features of classical logic. Omitting also falsehood prevents the impression that you could just define negation by implication to falsehood. Still, falsehood is only a single element, and adjoining it back is easy and unproblematic. Jun 2, 2016 at 3:41
• If you remove the rules for negation and $\bot$ from the logic, you will generally obtain a system known as minimal logic, which is strictly weaker than classical logic. en.wikipedia.org/wiki/Minimal_logic Jun 5, 2016 at 11:38
• @CarlMummert Yes, minimal logic was my motivation for also removing falsehood. Minimal logic is actually minimally weaker than intuitionistic logic, but the difference is so small that I consider them still essentially the same (intuitionistic) logic. But just like for monoids and semigroups, the minimal gained generality is rarely worth the effort this causes in terms of more convolved definitions and theorem statements. (Noah Schweber's answer nicely demonstrates this, at least it wasn't as clear to me before.) Jun 5, 2016 at 13:10

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.
• I admit that I haven't proved my statement: "You can omit negation and falsehood, and still get essentially the same classical logic." Especially my replacement (or translation) for falsehood was a bit weak. A better approach to see that they are essentially the same might be to translate negation as in $\lnot A$ by $A\to p$, where $p$ is a free propositional variable. So all the homomorphisms and properties with respect to homomorphisms will stay the same. (Note that Gentzen already has implication in his language, so negation becomes sort of redundant.) Jun 2, 2016 at 6:12
• @ThomasKlimpel I think you're misunderstanding my comment about homomorphisms. Let me put it this way: for any fixed language, there's a single structure which satisfies all first-order sentences, in that language, without negation (one element, all relations are total)! That is, there are no inconsistent theories if we get rid of $\neg$. How is this the "essentially the same" as first-order logic? (Note that this also means that the consistency question - which Gentzen definitely cared about! - is trivial for first-order theories without negation, unless rephrased in a more convoluted way.) Jun 2, 2016 at 17:57
• This comment shows an interesting fact about what is meant by consistency. If a classical first order theory is inconsistent, then the only possible Boolean valued models take values in the one element Boolean algebra (where $\bot=\top$). The same fact remains true if we remove negation from the language. If you exclude (=don't allow) the one element Boolean algebra in case that the language has negation, and suddently allow it if negation is removed from the language, then this has very little to with whether we still have essentially the same classical logic or not. Jun 2, 2016 at 20:00
• It depends on whether you think that the sentence $(x=x) \to p$ is satisfied (or write $\top\to p$, if you prefer). If the logic has more than one value, then it has a value different from $\top$, and the sentence would be false because $p$ could assume that value. Jun 2, 2016 at 20:32