Propositional logic without negation

Question

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.

Answer 1

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.

Answer 2

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