As part of a bigger project I am researching a propositional logic, without a negation. And I would like to know, whether this already exists, to avoid double work and have proper references.

In this propositional logic, every theorem consists of exactly one implication $\rightarrow$ of two boolean expressions that consists of propositional variables, $\wedge$, $\vee$, $true$, $false$.

For instance an expression in normal proposition logic:

$$(a \wedge \neg b) \rightarrow (c \wedge \neg d)$$

Must be expressed in this system in two theorems:

$$a \rightarrow (b \vee c)$$ $$(a \wedge d) \rightarrow b$$

Every propositional expression can be transformed in multiple theorems of this system. That can easily be seen by turning an expression in CNF. Although, this form is more relaxed than CNF.

Although it doesn't have a not, $\neg a$ can be expressed as $a \rightarrow false$

So, the idea is that any sub-expression on the left is negative charged and on the right side positive. This allows of easy deep inference. If:

$$\alpha \rightarrow \beta$$ and $$\gamma \rightarrow \delta$$ and $\beta$ is a sub-expression of $\gamma$ then $\beta$ can be replaced by $\alpha$: $$ \gamma_{\beta/\alpha} \rightarrow \delta $$

I have been searching on the internet, but couldn't find anything in this direction. Does anyone has seen something like this, or something where I should look?

Note, due to the absence of negation, you don't have the discussion of excluded middle.

  • 3
    $\begingroup$ It looks like Horn Clauses to me. Or more general, geometric logic. $\endgroup$ Jul 13 '15 at 22:46
  • 1
    $\begingroup$ Your implications are a notational variant for monotone sequents, so you might want to look into the monotone sequent calculus. $\endgroup$ Jul 14 '15 at 10:30

As you've already noticed, this is essentially the conjunctive normal form, with the conjuncts separated as individual formulas of the sort usually called "clauses", i.e., disjunctions of atomic and negated atomic formulas. The only difference is notational, in that instead of writing a clause as $a_1\lor\dots\lor a_k\lor(\neg b_1)\lor\dots\lor(\neg b_l)$, you write it in the equivalent form $(b_1\land\dots\land b_l)\to(a_1\lor\dots\lor a_k)$. I think you could find lots of material about such a set-up, since this sort of splitting of a CNF into clauses is the starting point for the "resolution" method of proof, which is rather basic in automated theorem proving.

  • 2
    $\begingroup$ It is not the same as CNF, because the sub-formulas on the right and the left can be of any complexity, as long as it doesn't contain 'not'. $\endgroup$
    – Lucas K.
    Jul 14 '15 at 12:13

Check paper called "Lectures on the Curry-Howard Isomorphism". It seems to be pretty comprehensive introduction to different kinds of logics.


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.