Logic without negation and falsehood

In the last post, consideration related to partial functions lead us to present a logic without truth and implication, using the binary minus operation as a dual of implication and substitute for unary negation. But logic without implication and equivalence is strange. So in this post we want to omit negation and falsehood instead.

(This post got surprisingly long. Sometimes I got slightly sidetracked, for example the discussion of the parity function and its sequent rules could have been omitted. But I already tried to remove most of those sidetracks. The real reason for the size explosion are the examples of axiomatic theories in predicate logic. But those had to be discussed, since they make it clear that one can really omit falsehood without loosing anything essential.)

The classical sequent calculus

Before starting to omit logical operations, let us first recall the classical sequent calculus including as many logical operations as barely reasonable. If we limit ourself to constants, unary operations, and binary operations, then we get:

Constants for truth ( $\top$ ) and falsehood ( $\bot$ )
An unary operation for negation ( $\lnot$ )
Binary operations for: or ( $\lor$ ), and ( $\land$ ), implication ( $\to$ ), minus ( $-$ ), nand ( $|$ ), nor ( $\overline{\lor}$ ), equivalence ( $\equiv$ ), and xor ( $\oplus$ ). The remaining binary operations add nothing new: reverse implication, reverse minus, first, second, not first, not second, true, and false

We work with sequents $A_{1},\ldots,A_{r}\vdash B_{1},\ldots,B_{s}$ , and interpret the propositions $A_i$ (and $B_j$ ) as subsets of some universe set $X$ . We interpret the sequent itself as $[A_{1}]\cap\ldots\cap [A_{r}]\ \subseteq\ [B_{1}]\cup\ldots\cup [B_{s}]$ . Let $\Gamma,\Delta, ...$ stand for arbitrary finite sequences of propositions.

Left structural rules	Right structural rules
$\begin{array}{c} \Gamma\vdash\Delta\\ \hline \Gamma,A\vdash\Delta \end{array}(WL)$	$\begin{array}{c} \Gamma\vdash\Delta\\ \hline \Gamma\vdash A,\Delta \end{array}(WR)$
$\begin{array}{c} \Gamma,A,A\vdash\Delta\\ \hline \Gamma,A\vdash\Delta \end{array}(CL)$	$\begin{array}{c} \Gamma\vdash A,A,\Delta\\ \hline \Gamma\vdash A,\Delta \end{array}(CR)$
$\begin{array}{c} \Gamma_{1},A,B,\Gamma_{2}\vdash\Delta\\ \hline \Gamma_{1},B,A,\Gamma_{2}\vdash\Delta \end{array}(PL)$	$\begin{array}{c} \Gamma\vdash\Delta_{1},A,B,\Delta_{2}\\ \hline \Gamma\vdash\Delta_{1},B,A,\Delta_{2} \end{array}(PR)$

Axiom	Cut
$\begin{array}{c} \ \\ \hline A\vdash A \end{array}(I)$	$\begin{array}{c} \Gamma\vdash\Delta,A\quad A,\Sigma\vdash\Pi\\ \hline \Gamma,\Sigma\vdash\Delta,\Pi \end{array}(Cut)$

Left logical rules	Right logical rules
$\begin{array}{c} \ \\ \hline \bot\vdash\Delta \end{array}(\bot L)$	$\begin{array}{c} \ \\ \hline \Gamma\vdash\top \end{array}(\top R)$
$\begin{array}{c} \Gamma\vdash A,\Delta\\ \hline \Gamma,\lnot A\vdash\Delta \end{array}(\lnot L)$	$\begin{array}{c} \Gamma,A\vdash \Delta\\ \hline \Gamma\vdash \lnot A,\Delta \end{array}(\lnot R)$
$\begin{array}{c} \Gamma,A,B\vdash\Delta\\ \hline \Gamma,A\land B\vdash\Delta \end{array}(\land L)$	$\begin{array}{c} \Gamma\vdash A,B,\Delta\\ \hline \Gamma\vdash A\lor B,\Delta \end{array}(\lor R)$
$\begin{array}{c} \Gamma,A\vdash\Delta\quad\Sigma,B\vdash\Pi\\ \hline \Gamma,\Sigma,A\lor B\vdash\Delta,\Pi \end{array}(\lor L)$	$\begin{array}{c} \Gamma\vdash A,\Delta\quad \Sigma\vdash B,\Pi\\ \hline \Gamma,\Sigma\vdash A\land B,\Delta,\Pi \end{array}(\land R)$
$\begin{array}{c} \Gamma,A\vdash B,\Delta\\ \hline \Gamma,A- B\vdash \Delta \end{array}(- L)$	$\begin{array}{c} \Gamma,A\vdash B,\Delta\\ \hline \Gamma\vdash A\to B,\Delta \end{array}(\to R)$
$\begin{array}{c} \Gamma\vdash A,\Delta\quad\Sigma,B\vdash\Pi\\ \hline \Gamma,\Sigma,A\to B\vdash\Delta,\Pi \end{array}(\to L)$	$\begin{array}{c} \Gamma\vdash A,\Delta\quad\Sigma,B\vdash \Pi\\ \hline \Gamma,\Sigma\vdash A-B,\Delta,\Pi \end{array}(- R)$
$\begin{array}{c} \Gamma\vdash A,B,\Delta\\ \hline \Gamma,A\overline{\lor} B\vdash \Delta \end{array}(\overline{\lor} L)$	$\begin{array}{c} \Gamma,A,B\vdash\Delta\\ \hline \Gamma\vdash A\|B,\Delta \end{array}(\| R)$
$\begin{array}{c} \Gamma\vdash A,\Delta\quad \Sigma\vdash B,\Pi\\ \hline \Gamma,\Sigma,A\|B\vdash \Delta,\Pi \end{array}(\| L)$	$\begin{array}{c} \Gamma,A\vdash\Delta\quad\Sigma,B\vdash\Pi\\ \hline \Gamma,\Sigma\vdash A\overline{\lor} B,\Delta,\Pi \end{array}(\overline{\lor} R)$
$\begin{array}{c} \Gamma,A\vdash B,\Delta\quad\Sigma,B\vdash A,\Pi\\ \hline \Gamma,\Sigma,A\oplus B\vdash \Delta,\Pi \end{array}(\oplus L)$	$\begin{array}{c} \Gamma,A\vdash B,\Delta\quad\Sigma,B\vdash A,\Pi\\ \hline \Gamma,\Sigma\vdash A\equiv B,\Delta,\Pi \end{array}(\equiv R)$
$\begin{array}{c} \Gamma\vdash A,B,\Delta\quad\Sigma,A,B\vdash\Pi\\ \hline \Gamma,\Sigma,A\equiv B\vdash\Delta,\Pi \end{array}(\equiv L)$	$\begin{array}{c} \Gamma\vdash A,B,\Delta\quad\Sigma,A,B\vdash\Pi\\ \hline \Gamma,\Sigma\vdash A\oplus B,\Delta,\Pi \end{array}(\oplus R)$

The rules for equivalence were taken from here, where they are also proved. Observe that $(A\equiv B)\equiv C=(A\oplus B)\oplus C = A\oplus(B\oplus C)$ . Clearly $A_1 \oplus \dots \oplus A_r$ is the parity function, which is famous for its computational complexity. It is easy to derive the rules for it (from the rules given above), but those rules have $2^r$ sequents above the line.

The rules for $A_1 \lor \dots \lor A_r$ and $A_1 \land \dots \land A_r$ are obvious. The rules for $A_1 \to \dots \to A_r \to B$ and $A - B_1 - \dots - B_r$ are also obvious, if we agree that this should be read as $A_1 \to (\dots \to (A_r \to B).)$ and $(.(A - B_1) - \dots) - B_r$ . Then $A|B=A\to B\to\bot$ and $A\overline{\lor}B=\top-A-B$ , so there is no need for multi-argument versions of nand and nor.

Omitting falsehood from classical logic

If we want to omit falsehood, it is not sufficient to just omit falsehood ( $\bot$ ). The operations minus ( $-$ ) and xor ( $\oplus$ ) must be omitted too, since $\bot = A-A = A\oplus A$ . Also nand ( $|$ ) and nor ( $\overline{\lor}$ ) must be omitted, since $\bot = A \overline{\lor}(A\overline{\lor}A)$ and $\bot = (A|(A|A))|(A|(A|A))$ . (They are functionally complete, so the only surprise is the length of the formulas). And if we want to keep truth ( $\top$ ) or any of the remaining binary operations (or ( $\lor$ ), and ( $\land$ ), implication ( $\to$ ), or equivalence ( $\equiv$ )), then also negation ( $\lnot$ ) must be omitted.

But without negation, how can we express the law of excluded middle or double negation? Both $A\lor \lnot A$ and $\begin{array}{c} \lnot\lnot A \\ \hline A \end{array}$ use negation. If we look at proof by cases, then $\begin{array}{c} \lnot A \to A \\ \hline A \end{array}$ or rather its generalization $\begin{array}{c} (A\to B) \to A \\ \hline A \end{array}$ suggests itself, which is called Peirce’s law. And the sequent calculus suggests $\begin{array}{c} A\to(B\lor C) \\ \hline (A\to B)\lor C\end{array}$ , which expresses a nice algebraic property of classical logic. But how do we prove that we get classical logic, and what does that mean?

At least classical tautologies like $((A\to B)\to B) \to (A\lor B)$ not using any of the omitted operations should still be tautologies. If “still be tautologies” is interpreted as being provable in the classical sequent calculus, then this follows from cut elimination. The cut elimination theorem says that the rule (Cut) can be avoided or removed from proofs in the sequent calculus. Since for all other rules, the formulas above the line are subformulas of the formulas below the line, only operations occurring in the sequent to be proved can occur in a cut-free proof.

However, my intended interpretation of “still be tautologies” is being provable in the natural deduction calculus. But let us not dive into the natural deduction calculus here, since this post will get long anyway. We still need to clarify what it means that we get classical logic. The basic idea is that logical expressions involving falsehood can be translated into expressions avoiding falsehood, which still mean essentially the same thing. But what exactly can be achieved by such a translation? Time for a step back.

Boolean functions of arbitrary arity

A Boolean function is a function of the form $f : B^k \to B$ , where $B = \{0, 1\}$ is a Boolean domain and $k$ is a non-negative integer called the arity of the function. Any Boolean function can be represented by a formula in classical logic. If we omit falsehood, a Boolean function with $f(1,\dots,1)=0$ certainly cannot be represented, for otherwise our goal to remove falsehood would have failed. The question is whether we can represent all Boolean functions with $f(1,\dots,1)=1$ , and whether the complexity of this representation is still comparable to the complexity of the representation where falsehood is available.

A two step approach allows to convert a given representation to one where falsehood is avoided. The first step is to replace $A-B$ by $(A\to B)\to\bot$ , $A\oplus B$ by $(A\equiv B)\to\bot$ , $A|B$ by $(A\land B)\to\bot$ , $A\overline{\lor}B$ by $(A\lor B)\to\bot$ , and $\lnot A$ by $A\to\bot$ . This step increases the size of the representation only by a small constant factor. The second step is to replace $\bot$ by the conjunction of all $k$ input variables. This step increases the size of the representation by a factor $k$ in the worst case. It works, since at least one of the input variables is $0$ , if $f$ is evaluated at an argument different from $(1,\dots,1)$ .

If one can define a new variable, then the factor $k$ can be avoided by defining $p:=\bigwedge_{i=1}^kA_i$ . However, the underlying idea is have a logical constant $p$ together with axioms $p\to A_i$ . This is equivalent to the single axiom $\bigwedge_{i=1}^k(p\to A_i)$ which simplifies to $p\to\bigwedge_{i=1}^k A_i$ .

Interpretation of logic without falsehood

When I initially wondered about omitting negation and falsehood from classical logic, I didn’t worry too much about “what it means that we get classical logic” and said

For a specific formula, falsehood gets replaced by the conjunction of all relevant logical expressions.

Noah Schweber disagreed with my opinion that “you can omit negation and falsehood, and still get essentially the same classical logic” and said

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.

So I replaced my harmless initial words by

One approach might be to translate $\lnot A$ as $A \to p$ , where $p$ is a free propositional variable. It should be possible to show that this works, but if not then we just keep falsehood in the language.

However, these new words are problematic, since $\lnot\lnot A \to A$ is a classical tautology, but $((A\to p)\to p)\to A$ is not. My initial words were not ideal too, since the meaning of “the conjunction of all relevant logical expressions” remained unclear.

The intuition behind my initial words was that falsehood is just the bottom element of the partial order from the Boolean algebra. Removing the explicit symbol (name) for the bottom element from the language should be harmless, since the bottom element can still be described as the greatest lower bound of “some relevant elements”. (However, removing the symbol does affect the allowed homomorphisms, since the bottom element is no longer forced to be mapped to another bottom element.)

The intuition behind my new words was an unlucky mix up of ideas from Curry’s paradox and the idea to use a free variable as a substitute for an arbitrary symbol acting as a potentially context dependent replacement for falsehood. We will come back to those ideas in the section on axiomatic theories in predicate logic without falsehood.

What are the “relevant logical expressions” for the conjunction mentioned above? Are $A\lor B$ , $A\to B$ , or $\forall x\forall y\ x=y$ relevant logical expressions? The first two are not, since $(A\lor B)\land B = B =(A\to B)\land B$ , i.e. the propositional variable $B$ itself is already sufficient. The third one is relevant, at least for predicate logic with equality. For propositional logic, it is sufficient to replace falsehood by the conjunction of all proposition variables occurring in the formula (and the assumptions of its proof). For predicate logic, it is sufficient to replace falsehood by the conjunction of the universally quantified predicate symbols, including the equality predicate as seen above (if present).

Axiomatic theories not using negation or falsehood

If the axioms or axiom schemes of an axiomatic theory (in classical first order predicate logic) don’t use negation or falsehood or any of the other operations we had to remove together with falsehood, then we don’t need to explicitly remove falsehood.

Let us look at the theory of groups as one example. If we denote the group multiplication by $\circ$ and the unit by $e$ , then the axioms are

$\forall{} x \forall{} y \forall{} z\ (x\circ y)\circ z=x\circ (y\circ z)$
$\forall x\ x\circ e = x$
$\forall x\exists y\ x\circ y=e$

We see that neither falsehood nor negation occurs in those axioms. This is actually a bit cheated, since it would seem that implication also doesn’t occur. It actually does occurs in the axioms governing equality. Here are some axioms for equality:

$\forall x\ x=x$
$\forall x\forall y\ (x=y \to y=x)$
$\forall x\forall y\forall z\ (x=y \to (y=z \to x=z))$

They only use implication, but something like the axiom schema

$x=y \to (\phi(x,x)\to\phi(x,y))$

is still missing. Here $\phi(x,y)$ is any formula, and may contain more free variables in addition to $x$ and $y$ . This doesn’t work for us, since this could also include formulas $\phi$ which use negation or falsehood! But at least for the theory of groups, the following two axioms (derived from instances of the axiom scheme) should be sufficient.

$\forall x\forall y\forall z\ (x=y \to x\circ z=y\circ z)$
$\forall x\forall y\forall z\ (x=y \to z\circ x=z\circ y)$

Here is a typical theorem of the theory of groups that should now be provable.

$\forall x\forall y\forall z\ (x\circ y = e \to (z\circ x = e \to y=z))$

Here is an informal proof: Since $x\circ y = e$ and $\forall x\forall y\ (x=y \to z\circ x=z\circ y)$ , we have $z\circ(x\circ y) = z\circ e$ . Since $z\circ(x\circ y)=(z\circ x)\circ y$ and $z\circ e = z$ , we have $(z\circ x)\circ y = z$ . Since $z\circ x = e$ and $\forall x\forall z\ (x=z \to x\circ y=z\circ y)$ , we have $e\circ y = z$ . If we could show $e\circ y = y$ (this was omitted in axioms given above), then the proof would be complete.

Axiomatic theories in predicate logic without falsehood

Let us next look at Robinson arithmetic, which is essentially Peano arithmetic without the induction axiom schema.

$(Sx=0)\to\bot$
$(Sx=Sy)\to x=y$
$y=0\lor\exists x\ Sx=y$
$x+0 = x$
$x + Sy = S(x+y)$
$x\cdot 0 = 0$
$x\cdot Sy = (x\cdot y) + x$

Here are the additional axioms for equality.

$x=y \to S(x)=S(y)$
$x=y \to x+z=y+z$
$x=y \to z+x=z+y$
$x=y \to x\cdot z=y\cdot z$
$x=y \to z\cdot x=z\cdot y$

Universal quantification has been omitted, but that should not worry us here. We see that the first axiom is the only one using falsehood. We could replace it by

$(Sx=0)\to\forall x\forall y\ x=y$

Or we could also introduce a constant $F$ and replace by the axioms

$F\to\forall x\forall y\ x=y$
$(Sx=0)\to F$

The second approach has the advantage that if we add the induction axiom schema to get Peano arithmetic, we can just replace falsehood by the constant $F$ . The first approach has the advantage that is shows that falsehood was never really required for the induction axiom schema.

The second approach comes closer to my motivations to remove falsehood from the language. I wanted to avoid negation and falsehood, because if there is no (bottom) element connecting everything together, then the damage caused by the principle of explosion can be restricted to specific domains of discourse. I also had the idea to use more specific propositional constants instead of falsehood. For ZFC set theory, one could use one propositional constant $F_=$ for the axiom asserting the existence of the empty set, and another propositional constant $F_\in$ for the axiom asserting regularity. However, as soon as one adds the axioms $F_= \to \forall x\forall y\ x=y$ and $F_\in \to \forall x\forall y\ x\in y$ , both constants will probably turn out to be equivalent.

Conclusions

Such a long post, for such a trivial thing as removing falsehood from the language. At least it should be clear now that one can really remove falsehood if desired, and what it means that one doesn’t loose anything essential. But is there anything to be gained by removing falsehood? The initial idea to remove falsehood came from the rule $\begin{array}{c} A\to(B\lor C) \\ \hline (A\to B)\lor C\end{array}$ (suggested by the sequent calculus), which characterises classical logic by a nice algebraic property (not involving negation or falsehood). The motivation to finish this post came from the realisation that implication is the central part of logic. I just read this recent post by Peter Smith on the material conditional, and realised that one really gains something by removing falsehood: the counterintuitive material conditional $P\to Q = \lnot P \lor Q$ goes away, and implication becomes the first class citizen it should have always been.

The counterintuitive part didn’t really disappear. The material conditional decomposes into the two sequents $P\to Q \vdash (P\to F)\lor Q$ and $(P\to F)\lor Q, F\to Q\vdash P\to Q$ . The proof sketch for those is $\begin{array}{c} P\to Q \\ \hline P\to(F\lor Q) \\ \hline (P\to F)\lor Q\end{array}$ and $\begin{array}{c}\begin{array}{c} (P\to F)\lor Q \\ \hline P\to(F\lor Q)\end{array} \quad \begin{array}{c} \ \\ F\to Q\end{array} \\ \hline P\to Q\end{array}$ . The proof of the second doesn’t even use the special properties of classical logic, but this part is the counterintuitive one: Why should $P\to Q$ be true, if $P\to F$ ? Well, the intuitive everyday logic is more a sort of modal logic than a propositional or predicate logic.

3 Responses to Logic without negation and falsehood

Paolo Logic says:

December 14, 2016 at 10:52 am

Cathoristic logic (https://arxiv.org/abs/1411.7158) is a logic without negation and implication. Negation is replaced by compatibility.

- gentzen says:
  
  December 19, 2016 at 11:45 am
  
  After reading the introduction, I got the impression that this is a nice paper with interesting mathematical and philosophical content. I especially like how it uses modal logic to allow the right level of expressiveness still allowing an efficient (quadratic time-complexity) decision procedure. I never heard of Richard Prideaux Evans before, but he seems to be an influential figure in AI. But I do know the second author Martin Berger, and I always appreciate his contributions on the Theoretical Computer Science StackExchange site.
  
Pingback: A subset interpretation (with context morphisms) of the sequent calculus for predicate logic | Gentzen translated