The DND-System (p. 74)

Process

Okay, so we already have:

Alphabet

$$ \Sigma_1=\{-,\text{D},\text{N}\} $$

Inference Rules

$$ \begin{prooftree} \AxiomC{} \RightLabel{ax$_{\text{DND}}$ *($x,y$ not empty)} \UnaryInfC{$\Gamma\vdash xy\text{DND}x$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma\vdash x\text{DND}y$} \RightLabel{R1} \UnaryInfC{$\Gamma\vdash x\text{DND}xy$} \end{prooftree} $$

And we’ve also gotten the hint that we need to come up with some kind of divisor-freeness concept.

Hmmm. I think I can think of this kind of like building a recursive function …

My Solution

First, we add new symbols to our alphabet:

$$ \Sigma_2=\Sigma_1\cup\{\text{P},\text{X}\} $$

Intuitively thinking of $\text{P}{-}^a\text{X}{-}^b$ as “$a$ has no divisors between 1 and $b$ (inclusive) besides 1”, we can now add another set of rules:

$$ \begin{prooftree} \AxiomC{} \RightLabel{ax$_{\text{PX}}$} \UnaryInfC{$\Gamma\vdash \text{P}x\text{X}{-}$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma\vdash\text{P}x\text{X}y$} \AxiomC{$\Gamma\vdash y{-}\text{DND}x$} \RightLabel{R2} \BinaryInfC{$\Gamma\vdash\text{P}x\text{X}{y-}$} \end{prooftree} $$

And finally, our prime rule(s), thinking of $\text{P}{-}^a$ as “$a$ is prime”:

$$ \begin{prooftree} \AxiomC{} \RightLabel{Two} \UnaryInfC{$\Gamma\vdash \text{P}{--}$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma\vdash \text{P}x{-}\text{X}x$} \RightLabel{P$_F$} \UnaryInfC{$\Gamma\vdash \text{P}x{-}$} \end{prooftree} $$

This entire system is now roughly equivalent to the following Haskell program:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
-- Define a datatype for the hyphens, automatically deriving Ord, Eq and Show.
data Hyp = One | Succ Hyp
  deriving (Ord, Eq, Show)

-- Define subtraction for Hyp. We need this to implement the rules later.
sub :: Hyp -> Hyp -> Hyp
sub One      _          = error "encountered non-positive number …"
sub (Succ x) One        = x
sub (Succ x) (Succ y)   = sub x y

-- Define a conversion from an amount of hyphens to the Hyp datatype for ease
-- of testing.
toHyp :: Int -> Hyp
toHyp x
  | x < 1               = error "non-positive number"
  | x == 1              = One
  | otherwise           = Succ (toHyp (x-1))

-- Implement the DND-related rules.
dnd :: Hyp -> Hyp -> Bool
dnd x y
  | x == y              = False                         -- make fn return false
                                                        --   instead of fail if
                                                        --   if x divides y.
  | x  > y              = True                          -- ax (DND)
  | otherwise           = dnd x (sub y x)               -- R1

-- Implement the RX-related rules.
px :: Hyp -> Hyp -> Bool
px x One                = True                          -- ax (PX)
px x (Succ y)           = (px x y) && (dnd (Succ y) x)  -- R2

-- Implement the prime rules.
prime :: Hyp -> Bool
prime (Succ One)        = True                          -- Two
prime (Succ x)          = px (Succ x) x                 -- P (F)

Which is probably a bit convoluted, but correct, if I’m not mistaken.

Note
I do have to admit here that I had originally forgotten to include the rule “Two” and only thought to add it when writing down the above program.

The Author’s Solution

It’s pretty similar to mine, but it differs in a few points, making it a tad more elegant in my estimation. It works as follows (paraphrased into my system):

We add three new symbols to our alphabet:

$$ \Sigma_3 = \Sigma_1\cup\{\text{D},\text{F},\text{P}\} $$

And extend our rules as follows:

$$ \begin{gather*} \begin{prooftree} \AxiomC{$\Gamma\vdash{--}\text{DND}z$} \RightLabel{R3} \UnaryInfC{$\Gamma\vdash z\text{DF}{--}$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma\vdash z\text{DF}x$} \AxiomC{$\Gamma\vdash x{-}\text{DND}z$} \RightLabel{R4} \BinaryInfC{$\Gamma\vdash z\text{DF}x{-}$} \end{prooftree} \\[1em] \begin{prooftree} \AxiomC{} \RightLabel{Two} \UnaryInfC{$\Gamma\vdash \text{P}{--}$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma\vdash z{-}\text{DF}z$} \RightLabel{P$_H$} \UnaryInfC{$\Gamma\vdash \text{P}z{-}$} \end{prooftree} \end{gather*} $$

Note
The author’s DF-string ${-}^a\text{DF}{-}^b$ can be intuitively thought of as “the number $a$ is divisor-free up to $b$, i.e. no number between $2$ (inclusive) and $b$ (inclusive) divides $a$.”