# A Two-dimensional Notation for Elementary Logic

Note: the box-drawing characters used in this paper may not render properly in some browsers.

In this paper I describe a graphical notation for elementary logic and provide a K script containing four sets of functions:

• Translate a formula in the propositional calculus to box notation,
• Render a formula in box notation,
• Reduce a formula in box notation to conjunctive normal form,
• Determine via Resolution whether a formula in box notation is a tautology.

## Translation

Begin by translating the formula to be reduced into box notation:

```(┬)           ┬

(┴)           ┴             │
└──

(~)           ~A            │ A
└───

(~~)          ~~A           ║ A
╚═══

(&)           A & B         A  B

(→)           A → B         │ A │ B
│   └───
└───────

(|)           A | B         ││ A │ B
│└───└───
└────────

(↔)           A ↔ B         │ A │ B │ B │ A
│   └───│   └───
└───────└───────
```

Standard box notation is limited to representing conjunction and negation:

```p & q           p  q

~P              │ p
└───
```

The method described in this note supplies a meaning to two-dimensional arrays of boxes: A column of boxes is interpreted as disjunction, and a set of such columns, written horizontally, is interpreted as conjunction. Thus, for example, the matrix

```p     r     u
q     s
t
```

has the meaning "(p or q) and (r or s or t) and u."

Using the translation functions supplied, we translate:

```(p → q) → ((~q) → (~p))
```

into:

```  contrapositive:onlyif[onlyif[p;q];onlyif[not q;not p]]
contrapositive
,(,(`p
,`q)
,,(,`q
,,`p))

`0:rep contrapositive

││ p │ q ║│ q ║ p
││   └───║└───╚═══
│└───────╚════════
└─────────────────
```

## Representation

The K translation functions:

```not:,:
and:(::)
or:{not and@not'x}
onlyif:{not and(x;not y)}
iff:{and(onlyif[x;y];onlyif[y;x])}
p:`p;q:`q;r:`r;s:`s;t:`t
false:not true:`
```

Observe that 'and', and 'or' are implemented as monadic functions with list arguments. This is because the corresponding operators in box notation are polyadic. For example,

```  `0:rep or(not p,q,r,s;not s)
│║ p  q  r  s ║ s
│╚════════════╚═══
└─────────────────
```

Expressions involving or consisting wholly of the truth-constants are also possible:

```  `0:rep onlyif[false;or(true;false;not false)]
││  ║│  ║  ║│
│└──║└──╚══║└──
│   ║      ╚═══
│   ╚══════════
└──────────────
```

The conjunctive normal form of a translated formula is a ragged matrix, a list of lists of propositional symbols and negations of propositional symbols. More precisely, if a propositional symbol has depth 0, then its negation -- the enlist of the symbol -- has depth 1. So a list of symbols and their negations has maximum depth 2, and a list of such lists has maximum depth 3.

## Reduction

Reduction takes an initial matrix consisting of one column and one row. To guarantee that this is so, we force the top-level structure of the formula to shape 1 1 (one column, one row) by means of double negation, which can have no effect on the meaning of the formula.

Given the initial matrix, we repeatedly apply two rules:

```(~)      Φ                   Φ

│ A .. Z            │ A
└────────           └────

Ψ                   :

│ Z
└────

Ψ

(~~)     Φ                   ..  Φ  ..

║ ..  A  ..         ..  A  ..
╚═══════════
..  Ψ  ..
Ψ
```

where Φ and Ψ represent vertical arrangements of zero or more elements.

Intuitively, the (~) rule takes a disjunction, one of whose components is the negation of n conjuncts, and replaces that component with n components, each of which is the negation of one of the conjuncts; and the (~~) rule takes a disjunction, one of whose components is the double-negation of n conjuncts, and replaces that disjunction with n disjunctions, each of which contains exactly one of the conjuncts.

In linear notation, the two rules correspond to the generalized De Morgan identities:

```(~)     Φ | ~(A & .. & Z) | Ψ
------------------------
Φ | (~A) | .. | (~Z) | Ψ

(~~)    Φ | ~~(.. & A & ..) | Ψ
-----------------------
.. & (Φ | A | Ψ) & ..
```

The K functions which implement the reduction rules are:

```red:{y;:[(#x)=i:(|/'0<n:typ''x)?1;(x;!0);1=|/m:n i;red1[x;i;m?1];red2[x;i;m?2]]}
typ:{:[(@x)|(1=#x)&@*x;0;1<#*x;1;2]}
red1:{((y#x),(,((z#x y),(,:'*x[y;z]),(z+1)_ x y)),(y+1)_ x;1,y,z)}
red2:{((y#x),@[x y;z;:;]'[(),{1=#x;,x;x]}@**x[y;z]],(y+1)_ x;2,y,z)}```

Each step in the reduction is annotated with the reduction rule and the row and column of the previous step to which the rule has been applied.

## Compression

In order to achieve the most compact, truth-functionally equivalent form, we also require four compression rules:

```(&)      Φ Ψ         Ψ Φ

(|)      A           B
B           A

(&&)     Φ Φ         Φ

(||)     A           A
A

```

Intuitively, & and | are commutative and idempotent. We apply these rules to the rows and columns of the normal form as a final step:

```cmp:{?({x@<x}@?:)'x}
```

## Conjunctive Normal Form

For example, the reduction of the contrapositive to normal form is:

```
║ p │ q
║   └───
╚═══════

║││ q ║ p
║│└───╚═══
║└────────
╚═════════

(~~)   C:0  R:0      p        │ q
└───

║││ q ║ p ║││ q ║ p
║│└───╚═══║│└───╚═══
║└────────║└────────
╚═════════╚═════════

(~~)   C:0  R:1      p        │ q
└───

││ q ║ p  ║││ q ║ p
│└───╚═══ ║│└───╚═══
└──────── ║└────────
╚═════════

( ~)   C:0  R:1      p        │ q
└───

║ q       ║││ q ║ p
╚═══      ║│└───╚═══
║└────────
╚═════════
║│ p
║└───
╚════

(~~)   C:0  R:1      p        │ q
└───

q        ║││ q ║ p
║│└───╚═══
║└────────
╚═════════
║│ p
║└───
╚════

(~~)   C:0  R:2      p        │ q
└───

q        ║││ q ║ p
║│└───╚═══
║└────────
╚═════════
│ p
└───

(~~)   C:1  R:1      p       │ q
└───

q       ││ q ║ p
│└───╚═══
└────────
│ p
└───

( ~)   C:1  R:1      p   │ q
└───

q   ║ q
╚═══

│ p  ║│ p
└─── ║└───
╚════

(~~)   C:1  R:1      p   │ q
└───

q    q

│ p  ║│ p
└─── ║└───
╚════

(~~)   C:1  R:2      p  │ q
└───
q   q

│ p │ p
└───└───

--------------------

│ p │ p
└───└───
p  │ q
└───
q   q

```

## Resolution

Annotation: line number, inputs to resolution.

```
0                   │ r
└───

1                    p
q

2                    p
r

3                   │ p
└───
r

4                    r
s

5                    r

│ q
└───

6                   │ s
└───
│ q
└───

7    2    0          p

8    3    0         │ p
└───

9    3    1          r
q

10   3    2          r

11   4    0          s

12   5    0         │ q
└───

13   5    1          r
p

14   6    1         │ s
└───
p

15   6    4         │ q
└───
r

16   8    1          q

17   8    7

```