5
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ What reason would he have to want to omit negation and falsity? $\endgroup$ – Noah Schweber Jun 1 '16 at 23:59
  • $\begingroup$ @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. $\endgroup$ – Thomas Klimpel Jun 2 '16 at 3:41
  • $\begingroup$ 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 $\endgroup$ – Carl Mummert Jun 5 '16 at 11:38
  • $\begingroup$ @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.) $\endgroup$ – Thomas Klimpel Jun 5 '16 at 13:10
2
$\begingroup$

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.

$\endgroup$
12
  • $\begingroup$ 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.) $\endgroup$ – Thomas Klimpel Jun 2 '16 at 6:12
  • $\begingroup$ @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.) $\endgroup$ – Noah Schweber Jun 2 '16 at 17:57
  • $\begingroup$ 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. $\endgroup$ – Thomas Klimpel Jun 2 '16 at 20:00
  • 1
    $\begingroup$ @ThomasKlimpel I'm not talking about Boolean-valued models, I'm talking about standard, 2-valued models. Any set of sentences in first-order logic without negation is satisfied in a structure with one element - this isn't a triviality about the number of truth values! At this point I'm still completely unclear what you mean by "essentially the same logic" - I am truly not being deliberately thick, can you please clarify? $\endgroup$ – Noah Schweber Jun 2 '16 at 20:17
  • $\begingroup$ 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. $\endgroup$ – Thomas Klimpel Jun 2 '16 at 20:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.