Gotta prove 'em all!
Combinatory logic is to Hilbert systems as lambda calculus is to natural deduction.
Hilbert systems apply tautologies to one another to produce more tautologies. This is clumsy, so logicians devised natural deduction, where we can focus on one part of a deduction just as lambda calculus allow us to cordon off parts of a program in the body of a lambda abstraction.
I built the above game to teach myself natural deduction from Jean-Yves Girard, Proofs and Types. See also:
The existential elimination rule in Girard’s notes are surprisingly simple. Other sources describe substituting a unique constant term for the quantified variable (skolemizing) to start off the side deduction, and ensuring the conclusion reached from this hypothesis contains no occurrences of this placeholder term.
Girard mentions no such substitution, and merely requires that the quantified variable \(\xi\) is no longer free in the hypotheses or the conclusion. I’m unsure why others present a more complex rule, as they seem equivalent: when the existential is dropped, occurrences of the variable \(\xi\) that were bound become free. Unless the hypothesis is discharged in the side deduction, we are unable to bind \(\xi\) with a universal quantifier, which seems to be the only hazard.
Playing the game feels eerily like programming due to the Curry-Howard
correspondence. For example, a common manoeuvre is to introduce an implication
with zero discharges, then immediately eliminate the implication, so the result
is two live hypotheses \(x, y\) leading to the conclusion \(x\). In other
words, it’s a bizarre roundabout way of writing Haskell’s const function.
Curry-Howard also helps us understand why natural deduction is in fact awkward in practice. For example, in Haskell, given a function with type, say:
(t -> Int) -> Int -> (Int -> u -> Int)
we can write a function with type:
(t -> Char) -> Char -> (Char -> u -> Char)
by judicious insertions of ord and chr. It’s a slog, yet undeservedly so:
we can easily convert Int to Char and back, so why is it so much trouble to
convert the code?
Analogously, with natural deduction, given the hypotheses \(x \Rightarrow y\)
and its converse, one does not simply replace each \(x\) with a \(y\) in a
deduction. Instead, we have to break down a formula, replace the occurrences
piecemeal, then stitch it all up again. Just like traversing an abstract syntax
tree to add ord and chr.
Friendlier theorem provers like HOL Light have equational reasoning built into their rules.
Our game explores more than one type of logic, though in all of them, we represent falsehood with ⊥ and treat ¬a as syntax sugar for a⇒⊥. Other logics define ¬ to be a primitive logical operator.
This scheme makes proof easier to express than refutation, when we are perhaps better off giving the two concepts equal status. But we’ll tolerate this asymmetry for now.
The Law of Excluded Middle (LEM), or tertium non datur, and equivalent to proof by contradiction, or reductio ad absurdum. In our game the LEM rule captures the principle of double negation:
\[ ((a\Rightarrow \bot)\Rightarrow \bot) \Rightarrow a \]
LEM is the hallmark of classical logic. Some levels limit the player to introduction and elimination rules for implication, and the Law of Excluded Middle. Along with a false proposition, these yield all of classical propositional logic: implicational propositional calculus.
However,
the
LEM rule may be too strong. In particular, the corresponding types make no
sense for programming languages based on lambda calculus. For instance, if f
is a function that takes an integer but is buggy then LEM is sort of claiming
we can feed f to another buggy function to somehow cancel out the bugs and
magically produce an integer! On the other hand, LEM makes sense in
lambda-mu calculus.
Removing LEM entirely yields minimal logic, which as the name suggests, has limited use. Better to replace LEM with the weaker ⊥-elimination rule, which embodies the principle of explosion or ex falso quodlibet:
\[ \bot \Rightarrow a \]
This leads to intuitionistic logic. We cannot show a∨¬a, but we can get close with ¬¬(a∨¬a).
The game features famous landmarks of logic.
Principia Mathematica calls this the complement of reductio ad absurdum (pp. 103-104):
\[ ((a\Rightarrow \bot)\Rightarrow a)\Rightarrow a \]
\[ ((a\Rightarrow b)\Rightarrow a)\Rightarrow a \]
LEM is equivalent to Peirce’s law, thus classical propositional calculus can get by without false.
Łukasiewicz found this single axiom system for implicational propositional calculus.
\[ ( (a\Rightarrow b)\Rightarrow c)\Rightarrow ((c\Rightarrow a)\Rightarrow (d\Rightarrow a) ) \]
In classical logic, we can define ∨ in terms of ⇒ thanks to the following and its converse:
\[ a\vee b\Rightarrow (a\Rightarrow b)\Rightarrow b \]
Without LEM, we are unable to prove the converse.
One level shows that conjunction is symmetric, though this is untrue when speaking. We say "kit and caboodle" rather than the other way around. Steven Pinker explains why (around minute 34), though I bet for phrases like legal doublets, the ordering is dictated by tradition.
There are many distributive laws of propositional calculus. Our game only features one of them.
We start with a data type to represent logical formulas, along with routines for printing and parsing them.
data Term = Term String [Term] deriving Eq
instance Show Term where
showsPrec _ (Term fun args) = (fun++) . case args of
[] -> id
_ -> showParen True $ foldr (.) id $ intersperse (", "++) $ shows <$> args
data Expr = Expr :-> Expr | Expr :& Expr | Expr :+ Expr
| Predicate String [Term] | Bot | Top
| Forall String Expr | Exists String Expr deriving Eq
instance Show Expr where
showsPrec p = \case
Bot -> ("⊥"++)
Top -> ("⊤"++)
Predicate fun args -> (fun++) . case args of
[] -> id
_ -> showParen True $ foldr (.) id $ intersperse (", "++) $ shows <$> args
x :-> y -> showParen (p > 1) $ showsPrec 2 x . ("⇒"++) . showsPrec 1 y
x :+ y -> showParen (p > 2) $ showsPrec 2 x . ("∨"++) . showsPrec 2 y
x :& y -> showsPrec 3 x . ("∧"++) . showsPrec 3 y
Forall x t -> showParen (p > 0) $ ("∀"++) . (x++) . ('.':) . shows t
Exists x t -> showParen (p > 0) $ ("∃"++) . (x++) . ('.':) . shows t
jsEval "curl_module('../compiler/Charser.ob')"
import Charser
chainl1 p op = foldl (\x (f, y) -> f x y) <$> p <*> (many $ (,) <$> op <*> p)
chainr1 p op = go id where
go d = do
x <- p
(op >>= \f -> go (d . (f x:))) <|> pure (foldr ($) x $ d [])
isVar (h:_) = 'a' <= h && h <= 'z'
formula :: Charser Expr
formula = space *> expr <* eof where
expr = atm `chainl1` and' `chainl1` or' `chainr1` imp
var = (:) <$> lowerChar <*> many alphaNumChar
atm = spch '(' *> expr <* spch ')'
<|> spch '0' *> pure Bot
<|> spch '1' *> pure Top
<|> spch '#' *> (Predicate "" . (:[]) <$> term)
<|> Forall <$> (spch '\\' *> var <* spch '.') <*> expr
<|> Exists <$> (spch '_' *> var <* spch '.') <*> expr
<|> pred
args = spch '(' *> sepBy term (spch ',') <* spch ')' <|> pure []
term = do
s <- (:) <$> letterChar <*> many alphaNumChar
space
if isVar s then pure $ Term s [] else Term s <$> args
pred = do
h <- letterChar
t <- many alphaNumChar
space
Predicate (h:t) <$> args
imp = sp (string "->" <|> string "=>") *> pure (:->)
and' = sp (string "&" <|> string "*") *> pure (:&)
or' = sp (string "|" <|> string "+") *> pure (:+)
sp :: Charser a -> Charser a
sp = (<* space)
spch = sp . char
mustFormula :: String -> Expr
mustFormula = either undefined id . parse formula ""
mustFormula "a->b"
As with lambda expressions, natural deductions almost have a tree structure. In lambda calculus, we must keep track of where variables are bound. The Curry-Howard equivalent in natural deduction is keeping track of when hypotheses are discharged.
I chose SVG for this game. I thought it might be easiest to associate a translation transform with each parent node of the tree, because once child nodes are combined via some rule, there’s no need to move them independently. But then I realized I need to know the absolute position of each node so I can figure out what a mouse click is selecting.
I settled on a strange design with one level of nesting: each Deduction
contains its bounding box in absolute terms, and every Spot contains its box
in coordinates relative to the Deduction containing it. Thus transforming a
Deduction automatically moves all its Spots, and chasing mouse clicks only
requires one adjustment, at the cost of requiring every Spot in a Deduction
be retranslated every time a rule its root Deduction moves.
It seems I’m maintaining an SVG elements that mirrors the tree structure of
each deduction, while enjoying few of the benefits. In retrospect I might have
been better off defining onclick callbacks for each node to avoid computing
translations. I suppose part of me wanted to manipulate coordinates for some
reason.
I forget the source of our version of the Law of Excluded Middle. It seems a more popular incarnation is to step from \((a → \perp) → \perp\) to \(a\).
data Tree a = Node { rootLabel :: a, subForest :: [Tree a] } deriving (Show,Eq)
instance Functor Tree where
fmap f (Node a xs) = Node (f a) (fmap f <$> xs)
type Forest a = [Tree a]
data Pos a = Loc
{ _content :: Tree a
, _before :: Forest a
, _after :: Forest a
, _parents :: [(Forest a, a, Forest a)]
} deriving (Show,Eq)
data Spot = Spot
{ _id :: String
, _xywh :: [Int]
, _expr :: Expr
} deriving Show
data Deduction = Deduction
{ _did :: String
, _dim :: [Int]
, _tree :: Tree Spot
} deriving Show
data Game = Game
{ _deds :: [Deduction]
, _goal :: Expr
, _level :: Int
, _click :: Int -> Int -> IO ()
, _sym :: Int
, _live :: [String]
, _animcb :: IO ()
}
minVB = 100 vgap = 10 hgap = 8 cellHeight = 18 hf = (`div` 2) utf8length = \case [] -> 0 c:rest | n >= 128, n < 192 -> utf8length rest | otherwise -> succ $ utf8length rest where n = ord c hafwid s = hf (11 * utf8length (show s)) + 3
initSpots = go 0 0 where
go x idx = \case
[] -> []
expr:rest -> dedu : go (x + w + hgap) (succ idx) rest
where
hw = hafwid expr
w = 2*hw
sp = Spot { _id = "spot" ++ show idx, _xywh = [0, 0, w, cellHeight], _expr = expr }
dedu = Deduction ("dedu" ++ show idx) [x, 0, w, cellHeight] (Node sp [])
svgSpot (Spot idAttr [x, y, w, h] expr) = concat
[ "<g id='", idAttr, "' transform='translate"
, show (x, y), "'> <rect width='", show w, "' height='", show h
, "' fill='none' stroke='black' stroke-width='2' x='0' y='0' rx='4' ry='4'></rect>"
, "<text x='", show $ hf w, "' y='9' text-anchor='middle' alignment-baseline='central'>"
, show expr
, "</text></g>"
]
drawDedu (Deduction did [x, y, w, h] t) = do
jsEval_ $ concat
[ "soil.innerHTML += `<g id='", did, "' transform='translate"
, show (x,y), "'>"
, svgSpot $ rootLabel t
, "</g>`;"
]
redden (Deduction did _ _) = jsEval_ $ concat ["redden(", did, ");"]
blurb s = jsEval_ $ "blurb(`" ++ s ++ "`);"
select (Node sp _) = let
[_, _, w, h] = _xywh sp
in jsEval_ $ concat ["pick(", _id sp, ", ", show w, ", ", show h, ");"]
examine (Node sp ks, (_, dedu, _)) = do
lives <- _live <$> global
blurb $ intercalate ", " $ concat
[ [(if _id sp `elem` lives then "live" else "dead") ++ " hypothesis" | null ks]
, ["conclusion" | _id sp == _id (rootLabel $ _tree dedu)]
]
getAny \r@(node@(Node sp' _), _) -> do
untool
unless (_id sp == _id sp') do
select node
examine r
untool = do
getAny examine
jsEval_ "untool();"
seek f dedu = go $ _tree dedu where
go node@(Node v ks) = case f dedu v of
Just _ -> Just node
Nothing -> asum $ go <$> ks
zFind f xs = go [] xs where
go bef aft = case aft of
[] -> Nothing
a:at -> case f a of
Nothing -> go (a:bef) at
Just r -> Just (r, (bef, a, at))
click x y = do
f <- _click <$> global
f x y
someSpot sps xRaw yRaw = zFind (seek hit) sps where
hit dedu spot
| x >= x0 && y >= y0 && x <= x0 + w && y <= y0 + h = Just ()
| otherwise = Nothing
where
[x0, y0, w, h] = _xywh spot
[xd, yd, _, _] = _dim dedu
x = xRaw - xd
y = yRaw - yd
getAny f = do
g <- global
setGlobal g { _click = anySpot f }
anySpot f xRaw yRaw = do
g <- global
maybe untool go $ someSpot (_deds g) xRaw yRaw
where
go r@(node, _) = do
select node
f r
shove xdelta dedu@(Deduction did (xd:rest@(yd:_)) t) = do
jsEval $ concat [did, ".setAttribute('transform', 'translate", show (xd', yd), "');"]
pure $ Deduction did (xd':rest) t
where
xd' = xd + xdelta
animGrow x dx = jsEval_ $ concat [ "animGrow(", show x, ", ", show dx, ");" ]
animX xdelta dedu@(Deduction did (xd:rest@(yd:_)) t) = do
jsEval $ concat [ "animTr(", did, ", ", show xd, ", ", show xdelta, ", ", show yd, ");" ]
pure $ Deduction did (xd+xdelta:rest) t
genSym = do
g <- global
setGlobal g { _sym = succ $ _sym g }
pure $ _sym g
animThen f = do
jsEval_ "animStart();"
g <- global
setGlobal g { _animcb = f }
animDone = do
g <- global
_animcb g
checkGoal dedu = do
g <- global
let
t = _tree dedu
live (Node sp ks) = case ks of
[] -> _id sp `elem` _live g
_ -> or $ live <$> ks
when (_expr (rootLabel t) == _goal g && not (live t)) $ jsEval_ "qed();"
findIds f (Node sp ks) = case ks of
[] | f sp -> [_id sp]
| otherwise -> []
_ -> findIds f =<< ks
discharge hypo dedu = do
g <- global
let
liveMatches = findIds (\sp -> _expr sp == hypo && _id sp `elem` _live g) $ _tree dedu
mapM_ (\s -> jsEval_ $ "unredden(`" ++ s ++ "`);") liveMatches
setGlobal g { _live = _live g \\ liveMatches }
getConc f = getAny \x@(Node sp _, (_, dedu, _)) -> \cases
| _id sp == _id (rootLabel $ _tree dedu) -> f x
| otherwise -> oops $ "want conclusion"
getLive f = getAny \x@(Node sp _, (_, dedu, _)) -> do
lives <- _live <$> global
if _id sp `elem` lives then f x else oops $ "want live hypothesis"
implies = do
blurb "pick live hypothesis"
getLive \(node, ctx@(_, dedu, _)) -> do
let hypo = _expr $ rootLabel node
discharge hypo dedu
implies' hypo ctx
impliesZ = do
blurb "pick any antecedent"
getAny \(lhs, _) -> do
blurb "pick consequent conclusion"
getConc \(rhs, ctx) -> implies' (_expr $ rootLabel lhs) ctx
implies' ante ctx@(_, dedu, _) = deduce (ante :-> _expr (rootLabel $ _tree dedu)) ctx
translateTree dx dy = go where
go (Node sp ks) = do
jsEval_ $ concat
[_id sp, ".setAttribute('transform', 'translate", show (x', y'), "');"]
Node sp { _xywh = x':y':rest } <$> mapM go ks
where
x:y:rest = _xywh sp
x' = x + dx
y' = y + dy
untrans x0 y0 (Deduction _ (x:y:_) t) = translateTree (x - x0) (y - y0) t
deduce conc (bef, dedu, aft) = do
let
[xLast, _, wLast, _] = _dim $ last (dedu:aft)
origW = wLast + xLast
t = _tree dedu
[xd, yd, wd, hd] = _dim dedu
[_, y, _, _] = _xywh $ rootLabel t
hw = hafwid conc
xtra = max 0 $ hw - hf wd
sym <- genSym
t <- translateTree xtra 0 t
let
sp = Spot ("spot" ++ show sym) [max 0 $ hf wd - hw, y + cellHeight + vgap, 2*hw, cellHeight] conc
dedu' = dedu { _dim = [xd - xtra, yd, wd + 2*xtra, hd + cellHeight + vgap], _tree = t }
aft <- mapM (animX $ 2*xtra) aft
dedu' <- animX xtra dedu'
dedu' <- pure $ dedu' { _tree = Node sp [_tree dedu'] }
g <- global
setGlobal g { _deds = reverse bef ++ (dedu' : aft) }
let
srcW = max minVB origW
tgtW = max minVB $ origW + 2*xtra
when (tgtW > srcW) $ animGrow srcW $ tgtW - srcW
animThen do
jsEval_ $ concat
[ _did dedu, ".innerHTML+=`", svgSpot sp, "`;"
, _id sp, ".innerHTML+=`"
, "<rect fill='grey' width='1' height='", show vgap, "' x='", show hw, "' y='", show $ -vgap,"'></rect>"
, "`;"
, "fadeIn(", _id sp, ");"
, "borderOut(", _id $ rootLabel t, ");"
]
jsEval_ "unleashUnreddens();"
animThen $ checkGoal dedu'
untool
merge u ks = do
sym <- genSym
let
[xa, y, wa, _] = _dim $ head ks
[xd, _, wd, _] = _dim $ last ks
hmax = foldr1 max $ (!!3) . _dim <$> ks
hw = hafwid u
sp = Spot ("spot" ++ show sym) [hf w - hw, hmax + vgap, 2*hw, cellHeight] u
w = xd - xa + wd
x = xa
h = hmax + vgap + cellHeight
did = "dedu" ++ show sym
newKid k = do
jsEval_ $ concat [did, ".append(...", _did k, ".childNodes);"]
jsEval_ $ concat [_did k, ".remove();"]
let
[xk,yk,wk,hk] = _xywh $ rootLabel $ _tree k
idKid = _id $ rootLabel $ _tree k
jsEval_ $ concat
[ idKid, ".innerHTML+=`"
, "<rect fill='grey' width='1' height='"
, show $ (_xywh sp!!1) - yk - cellHeight - hf vgap
, "' x='", show $ hf wk, "' y='", show cellHeight,"'></rect>"
, "`;"
, "borderOut(", idKid, ");"
]
jsEval_ $ concat
[ "soil.innerHTML += `<g id='", did, "' transform='translate"
, show (x,y), "'>"
, svgSpot sp
, "</g>`;"
, "fadeIn(", _id sp, ");"
]
let
xL = hf wa - _xywh sp!!0
l2r = w - hf (wa + wd) + 1
jsEval_ $ concat [ _id sp, ".innerHTML+=`"
, "<rect fill='grey' width='1' height='", show $ hf vgap, "' x='", show $ hf (_xywh sp!!2), "' y='", show -(hf vgap), "'></rect>"
, "<rect fill='grey' width='", show l2r, "' height='1' x='", show xL, "' y='", show -(hf vgap), "'></rect>"
, "`;"
]
mapM_ newKid ks
Deduction did [x,y,w,h] . Node sp <$> mapM (untrans x y) ks
deduceMulti u ds (bef, dedu, aft) = do
let
[xLast, _, wLast, _] = _dim $ last (dedu:aft)
origW = wLast + xLast
offsets f w = \case
[] -> (w, f [])
d@(Deduction did dim _):rest
| elem did (_did <$> ds) -> offsets f w rest
| otherwise -> offsets (f . ((w - dim!!0, d):)) (w + dim!!2 + hgap) rest
offsets' f w = \case
[] -> (w, f [])
d@(Deduction did dim _):rest -> offsets' (f . ((w - dim!!0, d):)) (w + dim!!2 + hgap) rest
anim (w, as) = (w,) <$> mapM (uncurry animX) as
(w, bef) <- anim $ offsets id 0 $ reverse bef
(w, mids) <- anim $ offsets' id w $ ds ++ [dedu]
(w, aft) <- anim $ offsets id w aft
let
srcW = max minVB origW
tgtW = max minVB $ w - hgap
when (tgtW > srcW) $ animGrow srcW $ tgtW - srcW
animThen do
conc <- merge u mids
jsEval_ "unleashUnreddens();"
animThen do
g <- global
setGlobal g { _deds = bef ++ (conc : aft) }
untool
oops s = do
untool
blurb $ "oops: " ++ s
unor = do
lives <- _live <$> global
blurb "pick X∨Y conclusion"
getConc \(orNode, (_, d0, _)) -> case _expr $ rootLabel orNode of
x :+ y -> do
blurb "pick first live hypothesis"
getLive \case
(node1, (_, d1, _))
| x == _expr (rootLabel node1) -> do
blurb "pick second live hypothesis"
getLive \case
(node2, ctx@(_, d2, _))
| y == _expr (rootLabel node2) -> if c == c'
then do
discharge x d1
discharge y d2
deduceMulti c [d0, d1] ctx
else oops $ concat ["mismatch: ", show c, " vs. ", show c']
| otherwise -> oops $ concat ["want ", show y, ", got ", show $ _expr (rootLabel node2)]
where
c = _expr $ rootLabel $ _tree d1
c' = _expr $ rootLabel $ _tree d2
| otherwise -> oops $ concat ["want ", show x, ", got ", show $ _expr (rootLabel node1)]
_ -> oops "want X∨Y"
or1 = do
blurb "pick conclusion"
getConc \(lhs, ctx) -> do
blurb "pick any formula"
getAny \(rhs, _) -> do
deduce (_expr (rootLabel lhs) :+ _expr (rootLabel rhs)) ctx
or2 = do
blurb "pick any formula"
getAny \(lhs, _) -> do
blurb "pick conclusion"
getConc \(rhs, ctx) -> do
deduce (_expr (rootLabel lhs) :+ _expr (rootLabel rhs)) ctx
forAll = do
blurb "pick a variable"
getAny \r@(node@(Node sp _), _) -> case _expr sp of
Predicate "" [Term s []] | isVar s -> do
blurb "pick a conclusion"
getConc \(rhs, ctx) -> do
-- TODO: Free variable check.
deduce (Forall s $ _expr $ rootLabel rhs) ctx
_ -> oops "want variable"
unforAll = do
blurb "pick a term"
getAny \r@(node@(Node sp _), _) -> case _expr sp of
Predicate "" [term] -> do
blurb "pick a ∀ conclusion"
getConc \(rhs, ctx) -> case _expr $ rootLabel rhs of
Forall x body -> deduce (beta term x body) ctx
_ -> oops "want ∀"
_ -> oops "want term"
-- TODO: Avoid variable capture.
beta term x = go where
go = \case
a :-> b -> go a :-> go b
a :& b -> go a :& go b
a :+ b -> go a :+ go b
Forall v body
| v == x -> Forall v body
| otherwise -> Forall v $ go body
Exists v body
| v == x -> Exists v body
| otherwise -> Exists v $ go body
Predicate fun args -> Predicate fun $ termSub <$> args
t -> t
termSub (Term fun args)
| fun == x, null args = term
| otherwise = Term fun $ termSub <$> args
andIntro = do
blurb "pick first conclusion"
getConc \(lhs, (_, d1, _)) -> do
blurb "pick second conclusion"
getConc \(rhs, ctx) -> do
deduceMulti (_expr (rootLabel lhs) :& _expr (rootLabel rhs)) [d1] ctx
unand1 = do
blurb "pick X∧Y conclusion"
getConc \(node, ctx@(_, dedu, _)) -> do
case _expr (rootLabel node) of
x :& _ -> deduce x ctx
otherwise -> oops "want X∧Y"
unand2 = do
blurb "pick X∧Y conclusion"
getConc \(node, ctx@(_, dedu, _)) -> do
untool
case _expr (rootLabel node) of
_ :& x -> deduce x ctx
otherwise -> oops "want X∧Y"
unimplies = do
blurb "pick antecedent conclusion"
getConc \(lhs, (_, ante, _)) -> do
blurb "pick X⇒Y conclusion"
getConc \(rhs, ctx@(_, dedu, _)) -> do
case _expr $ rootLabel rhs of
t :-> u
| t == _expr (rootLabel lhs) -> do
deduceMulti u [ante] ctx
| otherwise -> oops $ concat ["want ", show t, ", got ", show $ _expr $ rootLabel lhs]
_ -> oops "want X⇒Y"
lem = do
blurb "pick live X⇒⊥ with ⊥ conclusion"
getLive \(node, ctx@(_, dedu, _)) -> do
let hypo = _expr $ rootLabel node
case hypo of
t :-> Bot -> case _expr $ rootLabel $ _tree dedu of
Bot -> do
discharge hypo dedu
deduce t ctx
_ -> oops "want ⊥ conclusion"
_ -> oops "want X⇒Y"
unbot = do
blurb "pick ⊥ conclusion"
getConc \(bot, ctx) -> \cases
| Bot == _expr (rootLabel bot) -> do
blurb "pick any formula"
getAny \(node, _) -> deduce (_expr $ rootLabel node) ctx
| otherwise -> oops "want ⊥"
readLevels = go . lines <$> jsEval "lvls.getElementsByTagName('pre')[0].innerText;" where
go = \case
flav:goal:src:rules:rest -> f $ go rest
where
f = either error (:) do
g <- parse formula "" goal
xs <- mapM (parse formula "") $ words src
pure (flav, g, xs, words rules)
_ -> []
levels = unsafePerformIO $ newIORef =<< readLevels
initLevel n = do
ls <- readIORef levels
if n < length ls then initSingle n (ls!!n) else do
jsEval_ "sandbox.style.display='';campaign.style.display='none';"
jsEval_ "initButtons();"
jsEval_ "const es = rules.getElementsByClassName('pushme'); for (const e of es) showLogic(e);"
jsEval_ "soil.innerHTML = ''; chosen = undefined;"
let vb = [-5, -5, minVB + 10, minVB + 10]
jsEval_ $ concat ["soil.setAttribute('viewBox', '", unwords $ show <$> vb, "');"]
setGlobal $ Game
{ _deds = []
, _goal = Bot
, _level = n
, _click = anySpot examine
, _sym = 0
, _live = []
, _animcb = undefined
}
initSingle n (flav, goal, starts, rules) = do
jsEval_ "sandbox.style.display='none';campaign.style.display='';"
jsEval_ $ concat ["initButtons();thmno.innerText = '", show n, "';"]
jsEval_ $ concat ["flavour.innerHTML = `<i>", flav, "</i>`;"]
mapM_ (\s -> jsEval_ $ "showLogic(" ++ s ++ ");") rules
let
deds = initSpots starts
[x, _, w, _] = _dim (last deds)
sz = max minVB $ x + w
setGlobal $ Game
{ _deds = deds
, _goal = goal
, _level = n
, _click = anySpot examine
, _sym = length starts
, _live = ("spot"++) . show <$> [0..length starts - 1]
, _animcb = undefined
}
let vb = [-5, -5, sz + 10, sz + 10]
g <- global
jsEval_ $ concat ["goal.innerHTML=`", show $ _goal g, "`;"]
jsEval_ $ concat ["soil.setAttribute('viewBox', '", unwords $ show <$> vb, "');"]
jsEval_ "soil.innerHTML = ''; chosen = undefined;"
mapM_ drawDedu $ _deds g
mapM_ redden $ _deds g
initLevel 0
jsEval "initGame(repl);"
reset = do untool initLevel . _level =<< global advance = do g <- global initLevel $ _level g + 1
parseHypo = do
s <- jsEval "hypoText.value;"
case parse formula "" s of
Left err -> oops err
Right expr -> do
sym <- genSym
g <- global
let
deds = _deds g
xD = case deds of
[] -> 0
_ -> x + w + hgap where [x, _, w, _] = _dim $ last deds
hw = hafwid expr
w = 2*hw
spid = "spot" ++ show sym
did = "dedu" ++ show sym
sp = Spot { _id = spid, _xywh = [0, 0, w, cellHeight], _expr = expr }
dedu = Deduction did [xD, 0, w, cellHeight] (Node sp [])
srcW = max minVB $ xD - hgap
tgtW = max minVB $ xD + w
when (tgtW > srcW) $ animGrow srcW $ tgtW - srcW
setGlobal g { _deds = deds ++ [dedu], _live = spid : _live g }
drawDedu dedu
redden dedu
animThen $ pure ()
Show yourself! a->a a implies Ghosts of departed hypotheses a->b->a a b implies impliesZ An introduction to elimination a->(a->b)->b a a->b implies impliesZ unimplies Take me to your Reader (a->b->c)->(a->b)->a->c a a a->b a->b->c implies impliesZ unimplies Two wrongs make a right ((a->0)->0)->a a->0 (a->0)->0 implies impliesZ unimplies LEM Logic bomb 0->a 0 a->0 implies impliesZ unimplies LEM Aftershock (a->0)->a->b a a->0 b->0 implies impliesZ unimplies LEM The lie becomes the truth ((a->0)->a)->a a->0 a->0 (a->0)->a implies impliesZ unimplies LEM Peirce is worse ((a->b)->a)->a a a->0 a->0 b->0 (a->b)->a implies impliesZ unimplies LEM One rule to rule them all ((a->b)->c)->((c->a)->(d->a)) a a->0 a->0 b->0 d c->a (a->b)->c implies impliesZ unimplies LEM Just a second a&b->b a&b implies impliesZ unimplies unand1 unand2 Caboodle and kit a&b->b&a a&b a&b implies impliesZ unimplies and unand1 unand2 Or else what? a->a+b a b implies impliesZ unimplies or1 or2 unor Shine or rain a+b->b+a a+b a b implies impliesZ unimplies or1 or2 unor You say either and I say disjunction (a->c)->(b->c)->a+b->c a b a->c b->c a+b implies impliesZ unimplies or1 or2 unor Intuitionistic logic bomb 0->a 0 a implies impliesZ unimplies unbot Two wrongs no longer make a right (a+(a->0)->0)->0 a a->0 a+(a->0)->0 a+(a->0)->0 implies impliesZ unimplies unbot or1 or2 unor and unand1 unand2 Disjunction to implication a+b->(a->b)->b a+b a b a->b implies impliesZ unimplies unbot or1 or2 unor and unand1 unand2 One-way trip ((((a->b)->b)->a+b)->0)->0 a a b b (a->b)->b (((a->b)->b)->a+b)->0 (((a->b)->b)->a+b)->0 implies impliesZ unimplies unbot or1 or2 unor and unand1 unand2 Not to be confused with Distributivism a&b+a&c->a&(b+c) b c a&b a&b a&c a&c a&b+a&c implies impliesZ unimplies unbot or1 or2 unor and unand1 unand2 The proof is always easier on the other side a&(b+c)->a&b+a&c b c a&(b+c) a&(b+c) a&(b+c) implies impliesZ unimplies unbot or1 or2 unor and unand1 unand2