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.