typst-prooflists

This is a Typst package that provides for typesetting Gentzen-style proof trees in a succinct list-based notation. It builds atop curryst.

The canonical representation of a tree is a nested list. So, it only makes sense that when working with trees (proof trees or otherwise), you'd want to notate them down as a list (if not drawing them by hand). Yet existing typesetting packages don't do this!

This is mostly the fault of LaTeX. LaTeX is an intensely verbose (and hostile) piece of software... the normal syntax for lists goes something like \begin{itemize} \item ... \end{itemize} -- terrible! For this reason, LaTeX packages that aim to improve the ergonomics of typesetting trees (bussproofs for proof trees, forest for syntax trees) have not so much as considered lists as an option.

On the other hand, however, Typst provides a special list syntax, that can be introspected on: and assigned custom semantics! Which is what we do here. These lists as a domain-specific language allows for typesetting such (proof) trees in a compact, coherent, and more readily compositional fashion.

Usage

#import"@preview/prooflists:0.1.0":prooflist#prooflist[/$R$:$C_1orC_2orC_3$/$A$:$C_1orC_2orL$-$C_1orL$+$Pi_1$-$C_2oroverline(L)$+$Pi_2$]

Typst has three types of list items: - (bullet lists), + (numbered lists), and / (term lists). All three have their own semantics within the context of #prooflist.

• The + premise node is a terminal rule. It returns its content directly as a (single) premise. Any sublists are interpreted as lists directly, not proof lists or premises.

• The - conclusion node is a non-terminal rule. Any sublists are interpreted as premises, as are any nested calls to #prooflist. If no premises are provided, a top bar will still be drawn (as in the case of axioms).

• The / label: conclusion node is a labelled non-terminal rule. Any sublists are premises (as are any nested calls to #prooflist). If no premises are provided a top bar will still be drawn. The label field is technically optional -- if omitted, / : conclusion behaves identically to - conclusion.

Advanced Usage

#import"@preview/prooflists:0.1.0":prooflist#letax(conclusion)=prooflist[/ax:#conclusion]#letax-1=ax($Gammatackp->q$)#letax-2=ax($Gammatackpandnotq$)#prooflist[/$scripts(->)_i$:$tack(p->q)->not(pandnotq)$/$not_i$:$p->qtacknot(pandnotq)$/$not_e$:$underbrace(p->q,円pandnotq,Gamma)tackbot$/$scripts(->)_e$:$Gammatackq$#ax-1/$and_e^ell$:$Gammatackp$#ax-2/$and_e^r$:$Gammatacknotq$#ax-2]

Calls to #prooflist can be composed. #prooflist does not strip any content besides whitespace, and so calls to other functions may compose, too.

A limitation of the / label: conclusion syntax is that it only provides for providing one label, by default on the right. If labels appearing on the left is desired, label-dir: left can be passed as an optional argument to #prooflist, which will affect all / label: conclusion invocations. The label-lhs and label-rhs arguments can also be provided and will add custom labels to all inference rules on the left/right, respectively.

Finally, this package is built atop curryst and specifically #prooftree. #prooftree may take a number of optional arguments, which #prooflist plumbs through to additionally expose to the user. Documentation may be found in the function source (reproduced from curryst). The #rule-set function provided by curryst may be useful, also.

#import"@preview/prooflists:0.1.0":prooflist#import"@preview/curryst:0.6.0":rule-set#letvariable=prooflist[/Variable:$Gamma,x:Atackx:A$]#letabstraction=prooflist[/Abstraction:$Gammatacklambdax.P:A=>B$+$Gamma,x:AtackP:B$]#letapplication=prooflist[/Application:$Gamma,DeltatackPQ:B$+$GammatackP:A=>B$+$DeltatackQ:B$]#letweakening=prooflist[/Weakening:$Gamma,x:AtackP:B$+$GammatackP:B$]#letcontraction=prooflist(label-dir:left)[/Contraction:$Gamma,z:AtackP[x,y<-z]:B$+$Gamma,x:A,y:AtackP:B$]#letexchange=prooflist(label-dir:left)[/Exchange:$Gamma,y:B,x:A,DeltatackP:B$+$Gamma,x:A,y:B,DeltatackP:B$]#align(center,rule-set(variable,abstraction,application,weakening,contraction,exchange))

See examples/ for further use cases.