# Modeling Natural Deduction Derivations

I am teaching logic: propositional logic, first order logic, and some Alloy. I wanted to show a neat application of Alloy. Since I made the students do a lot of derivations (proofs) by Natural Deduction, I came up with this Alloy model that will automatically construct such proofs for Propositional Logic. The students were impressed by what Alloy could do, so I thought I’d share.

The model defines the syntax for a propositional logic formula, and then defines the structure of a derivation, which is a recursive (tree-like) structure. Each node is the application of one of 12 rules, has some number (<=3) of children (premises, or sub-derivations), and a conclusion, which is a sequent of the form S |- f, where S is a set of formulas (the antecedents) and f is a formula (the consequent). Then there is a series of examples where I describe the desired sequent and ask Alloy to find a derivation of it.

``````/* Alloy model of Natural Deduction for Propositional Logic
Stephen Siegel, University of Delaware, Nov. 2021
This model will find ND derivations for sequents in PL, i.e.,
judgments of the form S |- f, where S is a set of PL formulas
(the antecedents) and f is a PL formula (the consequent).
*/

-- derivations are trees but can be ordered for readability,
-- though this can increase runtime significantly.
-- children of node d always occur before d in the total order...
open util/ordering[Derivation]

/* PL Formulas */
abstract sig Formula { }              -- all PL formulas
one sig False extends Formula { }     -- the formula "False"
sig Prop extends Formula { }          -- propositions
abstract sig Op {}
one sig NOT, AND, OR, IMPLIES extends Op {}
sig CompoundFormula extends Formula { -- formulas formed by a connective
op: one Op,                         -- the operator
arg1: one Formula,                  -- argument 1 (required)
arg2: lone Formula                  -- argument 2 (optional)
}{
op = NOT iff no arg2                -- only NOT takes 1 argument
}
-- no formula can occur as a sub-formula of itself...
fact wellFormedFormula { no f: Formula | f in f.^( arg1 + arg2 ) }

/* Derivations */

abstract sig Rule {} -- enumeration of the rule schema for ND
one sig Ax, RAA, EAnd1, EAnd2, IAnd, EOr, IOr1, IOr2, EImp, IImp, ENot, INot
extends Rule {}
sig Derivation { -- a derivation is a recursive (tree-like) structure:
rule: one Rule, -- the rule of which this derivation is an instance
premise1, premise2, premise3: lone Derivation, -- at most 3 sub-derivations
antecedents: set Formula, -- left side of sequent of conclusion
consequent: one Formula -- right side of sequent of conclusion
}
fun antes[d: Derivation]: set Formula { d.antecedents }
fun form[d: Derivation]: one Formula { d.consequent }
fun premise[]: Derivation->Derivation { premise1 + premise2 + premise3 }
fact wellFormedDerivation { -- each derivation is the application of a rule
all d: Derivation | {
d.premise in prevs[d] -- use only if ordering Derivation
ax[d] or eAnd1[d] or eAnd2[d] or iAnd[d] or eOr[d] or iOr1[d] or
iOr2[d] or eImp[d] or iImp[d] or eNot[d] or iNot[d] or raa[d]
}
}

-- use this to say every Derivation is used in the derivation
-- that means the scope for Derivation must be exact, rather
-- than upper bound
pred exactRoot[d: Derivation] { d.*premise = Derivation }

-- When ordering,
-- the scope is specified exactly rather than as an upper bound,
-- so need to do something with the derivations that are not used.
-- say all derivations not reachable from root d just stutter d
pred isRoot[d: Derivation] {
all d1: Derivation - d.*premise | {
d1.rule = d.rule
d1.premise1 = d.premise1
d1.premise2 = d.premise2
d1.premise3 = d.premise3
d1.antecedents = d.antecedents
d1.consequent = d.consequent
}
}

/* Derivation rules */

-- Rule 1: Ax: S,f |- f
pred ax[d: Derivation] {
d.rule = Ax and no d.premise and form[d] in antes[d]
}

-- Rule 2: Reductio-Ad-Absurdum: if S,!f |- False then S |- f
pred raa[d: Derivation] {
d.rule = RAA and no d.premise2 + d.premise3
let d1 = d.premise1 |
form[d1] = False and some g: CompoundFormula |
g.op = NOT and g.arg1 = form[d] and antes[d1] = antes[d] + g
}

-- Rule 3: Eliminate-and-1: if S |- f&g then S |- f
pred eAnd1[d: Derivation] {
d.rule = EAnd1 and no d.(premise2 + premise3)
antes[d.premise1] = antes[d]
let h = form[d.premise1] | h.op = AND and h.arg1 = form[d]
}

-- Rule 4: Eliminate-and-2: if S |- f&g then S |- g
pred eAnd2[d: Derivation] {
d.rule = EAnd2 and no d.(premise2 + premise3)
antes[d.premise1] = antes[d]
let h = form[d.premise1] | h.op = AND and h.arg2 = form[d]
}

-- Rule 5: Introduce-And: if S |- f and S |- g then S |- f&g
pred iAnd[d: Derivation] {
d.rule = IAnd and no d.premise3
let d1 = d.premise1, d2=d.premise2, h=form[d] |
antes[d1] = antes[d2] and antes[d1] = antes[d] and
h.op = AND and h.arg1 = form[d1] and h.arg2 = form[d2]
}

-- Rule 6: Eliminate-Or: if S |- f1|f2 and S,f1 |- h and S,f2 |- h then S |- h
pred eOr[d: Derivation] {
d.rule = EOr
let S = antes[d], d1 = d.premise1, d2=d.premise2, d3=d.premise3 |
antes[d1] = S and antes[d2] = S + form[d1].arg1 and antes[d3] = S + form[d1].arg2
and form[d1].op = OR and form[d2] = form[d] and form[d3] = form[d]
}

-- Rule 7: Introduce-Or-1: if S |- f then S |- f|g
pred iOr1[d: Derivation] {
d.rule = IOr1 and no d.premise2 + d.premise3
antes[d.premise1] = antes[d]
form[d].op = OR and form[d].arg1 = form[d.premise1]
}

-- Rule 8: Introduce-Or-2: if S |- f then S |- g|f
pred iOr2[d: Derivation] {
d.rule = IOr2 and no d.premise2 + d.premise3
antes[d.premise1] = antes[d]
form[d].op = OR and form[d].arg2 = form[d.premise1]
}

-- Rule 9: Eliminate-Implies: if S |- f->g and S |- f then S |- g
pred eImp[d: Derivation] {
d.rule = EImp and no d.premise3
let d1 = d.premise1, d2 = d.premise2 | {
antes[d1] = antes[d] and antes[d2] = antes[d]
form[d2].op = IMPLIES and form[d2].arg1 = form[d1]
form[d] = form[d2].arg2
}
}

-- Rule 10: Introduce-Implies: if S,f |- g then S |- f->g
pred iImp[d: Derivation] {
d.rule = IImp and no d.premise2 + d.premise3
let d1 = d.premise1, h=form[d] |
h.op = IMPLIES and antes[d1] = antes[d] + h.arg1 and form[d1] = h.arg2
}

-- Rule 11: Eliminate-Not: if S |- !f and S |- f then S |- g
pred eNot[d: Derivation] {
d.rule = ENot and no d.premise3
let d1 = d.premise1, d2 = d.premise2 |
antes[d1] = antes[d] and antes[d2] = antes[d] and
form[d2].op = NOT and form[d2].arg1 = form[d1]
}

-- Rule 12: Introduce-Not: if S,f |- False then S |- !f
pred iNot[d: Derivation] {
d.rule = INot and no d.premise2 + d.premise3
let d1 = d.premise1 |
form[d].op = NOT and antes[d1] = antes[d] + form[d].arg1 and
form[d1] = False
}

/* Examples */

-- A |- A    (simple application of Ax rule)
pred ax1[d: Derivation] {
isRoot[d]
let f = antes[d] | one f and f=form[d] and f in Prop
}

-- A & B |- B & A   (and is commutative)
pred andCommute[d: Derivation] {
isRoot[d]
let f = antes[d], g = form[d] |
one f and g.op = AND and f.(arg1+arg2) in Prop and f.op = AND and
g.arg1 = f.arg2 and g.arg2 = f.arg1 and f.arg1 != f.arg2
}

-- A & (B | C) |- (A & B) | (A & C)  (and distributes over or)
pred dist1[d: Derivation] {
isRoot[d]
let f = antes[d] |
one f and f.op = AND and f.arg2.op = OR and
let a = f.arg1, b = f.arg2.arg1, c = f.arg2.arg2, g = form[d] | {
a+b+c in Prop
a != b and a != c and b != c
g.op = OR
g.arg1.op = AND and g.arg1.arg1 = a and g.arg1.arg2 = b
g.arg2.op = AND and g.arg2.arg1 = a and g.arg2.arg2 = c
}
}

-- |- P | !P  (Law of the Excluded Middle)
pred LEM[d: Derivation] {
isRoot[d]
no antes[d]
let f = form[d], p = f.arg1, f2 = f.arg2 |
f.op = OR and p in Prop and f2.op = NOT and f2.arg1 = p
}

-- |- !(A & B) -> (!A | !B)
pred deMorgan1[d: Derivation] {
exactRoot[d]
no antes[d]
let f = form[d], f1 = f.arg1, f2 = f.arg2, f11=f1.arg1,
f21 = f2.arg1, f22 = f2.arg2, a = f11.arg1, b = f11.arg2 |
a != b and a+b in Prop and f.op = IMPLIES and
f1.op = NOT and f11.op = AND and
f2.op = OR and f21.op = NOT and f21.arg1 = a and f22.op = NOT and f22.arg1 = b
}

/* Runs.  Solving times shown for Plingeling on MacBook Pro M1 */

run ax1                                               -- 1s
run andCommute for  2 Prop,  5 Formula,  4 Derivation -- 1s
run dist1      for  3 Prop,  9 Formula, 13 Derivation -- 7s
run LEM        for  1 Prop,  5 Formula,  9 Derivation -- 10s
run deMorgan1  for  2 Prop,  10 Formula, 15 Derivation -- varies wildly

``````

When you view an instance as a Table, it looks almost exactly like a Natural Deduction proof you would write. Here is Alloy’s proof of the Law of the Excluded Middle:

Suggestions for improvements are most welcome.

2 Likes

Hi Steve,

cool!

In a certain sense your approach is a constructive proof of the completeness of natural deduction for propositional logic: Your Alloy spec is transformed into a propositional formula and the SAT solver gives the deduction steps. Thus: whenever S |= f then there exists a derivation S |- f.

For my course ‘Logic and formal methods’ i developed the lwb Logic WorkBench’, a set of tools for the propositional logic, first order logic and linear temporal logic written in Clojure. in case you are interested, go to Logic Workbench and A simple GUI for lwb.

The following is a proof of the law of the excluded middle interactively build with the natural deduction module of lwb. It’s almost the same derivation as that generated by Alloy.

`````` --------------------------------------------------
------------------------------------------------
1:  | (not (or P (not P)))                 :assumption
| ----------------------------------------------
2:  | | P                                  :assumption
3:  | | (or P (not P))                     :or-i1 
4:  | | contradiction                      :not-e [1 3]
| ----------------------------------------------
5:  | (not P)                              :not-i [[2 4]]
6:  | (or P (not P))                       :or-i2 
7:  | contradiction                        :not-e [1 6]
------------------------------------------------
8: (or P (not P))                          :raa [[1 7]]
--------------------------------------------------
``````

Kind regards,
Burkhardt

Neat! I downloaded lwb and am playing with it. Seems like a great tool. It really helps to get instant feedback rather than doing everything with pen and paper.

The instant feedback is an advantage and a disadvantage at the same time. With lwb the students tend to just try the rules instead of first thinking about the strategy of a proof. So my mantra is: first think about the propositions and why they are correct, and then begin to use lwb. Use it as a tool to check the correct application of the rules and to avoid simple errors.

1 Like