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.
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
││ └───║└───╚═══
│└───────╚════════
└─────────────────
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 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.
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}
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
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