📝

Typstで論理式/証明図を書く

2024/12/13に公開

!この記事は、Typst Advent Calendar 2024 13日目の記事です。
論理式や証明図が入った文書やスライドを作成する場合、簡単な論理式程度であれば MS Word のような文書作成ソフトウェアの数式ツール、Markdown + MathJax、あるいは Unicode 文字でのベタ書きなどでも十分に書くことができるようになってきていると思いますが、特に証明図が入った文書やスライドを作成しようと思うと実質的に LaTeX 一択という印象でした[1]。

そんななか登場した Typst は、新しい実用レベルの選択肢と言えると思います。コンパイルが高速、文書のカスタマイズが比較的容易といった点だけでなく、(Myriad-Dreamin氏の貢献を中心に) typst.ts や shiroa などによるPDF以外のWeb向けのモダンな出力も可能になりつつある点でも期待が膨らむところです。
この記事では、Typst で論理式を入力したり証明図を作成したりするために必要な知識や便利なパッケージを簡単に紹介します。
一部の表示結果は MathJax で代用しているため、Typst の表示結果とは異なる場合があります。
なお、LaTeX での基本知識やパッケージについては以下のページが参考になります。
LaTeX for Logicians - Logic Matters

 論理式 etc. を書く
 数式モード (math mode)LaTeXと同様に、$...$ で囲うことで数式/論理式を入力することができます。

LaTeXではインライン表示は $...$ 、ブロック表示 (display style) は $$...$$ 等で囲って指定することができますが、typst ではドルマークと内容の間に1文字以上のスペースを入れることでブロック表示を指定することができます。
入力: $A and not A$

出力: A \land \neg A
入力: $ A and not A $

出力:

A \land \neg A

 記号の入力論理記号 etc. は Typst で定義されている記号の名前をそのまま入力します (例: and は ∧ になる)。LaTeX と異なり先頭にバックスラッシュはつけません。

一部の記号には略記も定義されています (例: arrow = ->)。
左矢印 (arrow.l) と右矢印 (arrow.r)、一重矢印 (arrow) と二重矢印 (arrow.double) のように、基本となる記号名の後にドット (.) で種別を指定するものもあります。

複数の種別の指定がある場合は、順序は任意です (例: arrow.l.double でも arrow.double.l でも可)。
Typst の便利なところとして、∧, → のように Unicode 文字を直接書いてもデフォルトで基本いい感じにしてくれる点があります[2]。LaTeX に比べると名前が長くなるものも多いので (例: \vDash vs tack.r.double) 、私は「たーん」→「⊨」のように辞書登録して入力しています。
Typst での記号の名前の一覧は以下のページで検索できます。
General Symbols – Typst Documentation
以下は典型的な記号等の入力例です。他にも載せるとよいものがあればぜひコメントをいただければと思います。


出力
LaTeX
Typst


P \land Q
P \land Q

P and Q, P ∧ Q


P \lor Q
P \lor Q

P or Q, P ∨ Q


P \to Q
P \to Q

P arrow Q, P -> Q, P → Q


P \supset Q
P \supset Q

P supset Q, P ⊃ Q


\neg P
\neg P

not P, ¬P


\forall x
\forall x

forall x, ∀x


\exists x
\exists x

exists x, ∃x


a = b
a = b

a eq b, a = b


k_{a_1}, ..., k_{a_n}
k_{a_1}, ..., k_{a_n}
k_a_1, ..., k_a_n

\varphi[a/x]
\varphi[a/x]
phi[a\/x]

\Box A
\Box A

square.stroked A, □A


\Diamond A
\Diamond A

diamond.stroked A, ◇A


\Gamma \Rightarrow \Delta
\Gamma \Rightarrow \Delta

Gamma => Delta, Γ ⇒ Δ


\Gamma \Longrightarrow \Delta
\Gamma \Longrightarrow \Delta

Gamma arrow.r.double.long Delta, Gamma ==> Delta


\Gamma \Longleftrightarrow \Delta
\Gamma \Longleftrightarrow \Delta

Gamma arrow.l.r.double Delta, Gamma <==> Delta


\Gamma \vdash \Delta
\Gamma \vdash \Delta

Gamma tack Delta, Γ ⊢ Δ


\Gamma \vDash \Delta
\Gamma \vDash \Delta

Gamma tack.r.double Delta, Γ ⊨ Δ


w \Vdash \varphi
w \vDash \varphi

w forces phi, w ⊩ φ



 打ち消し線打ち消し線 (取り消し線) は、Unicode で打ち消し線つきの記号が定義されているものについては、基本的に記号名に .not をつけることで入力できます。
例:


出力
LaTeX
Typst


\Gamma \not\vdash \Delta
\Gamma \not\vdash \Delta

Gamma tack.not Delta, Γ ⊬ Δ


それ以外に、cancel 関数を使うことで、任意の文字/文字列や記号に打ち消し線をつけられます。(Unicode上の打ち消し線つきの記号とは別です。)
例:
a eq.not b (a ≠ b)
a cancel(eq) b (a cancel(=) b)

 述語の注意点個人的にやや使いづらい点としては、Typstの数式モードでは基本的に2文字以上の文字列をそのまま表示することはできないという点があります。例えば、LaTeXでは
Rab \land Rba
を
$Rab \land Rba$
と書くことができますが、Typst では1文字ずつ空けて
$R a b and R b a$
と書く必要があります ($Rab and Rba$ と書くことはできない)。ただし、カッコをつけるスタイルであれば LaTeX 同様続けて書くことはできます (例: R(a,b) → R(a,b))。
このあたりの考え方については @ultimatile さんのアドベントカレンダー記事 (Typstで数式中の文字を斜めにしない方法) がとても参考になります。
また、分かりやすさのために述語として単語を使いたい場合 (例: Prime(x) など) も、$Prime(x)$ のように書くとエラーになってしまいます。$"Prime"(x)$ と書くことでエラーは解消できますが、これだけだと立体
\textnormal{Prime}(x)
になります。これはこれでアリなのですが、さらにイタリック体にするためには $italic("Prime")(x)$ のようにする必要があります。
もしこのあたりの手間を解消する方法をご存知の方がいましたらぜひご教示ください。

 証明図を書くいろいろな種類の証明図がありますが、ここでは2024年12月現在の typst Universe (LaTeXのCTANに相当するもの) に登録されているパッケージを使った4種類の証明図の例を紹介します。

 ゲンツェン式 (Gentzen-style) の証明図LaTeX では bussproofs などがよく使われると思います。
執筆時点では、typst Universe には prooftrees と curryst が掲載されていますが、prooftrees は deprecated となっており、curryst への移行が推奨されています。

 自然演繹の例#import "@preview/curryst:0.3.0": rule, proof-tree

#proof-tree(
  rule(
    name: [$→$ I, $1$],
    $(F a ∧ G a) → (G a ∧ F a)$,
    rule(
      name: [$and$ I],
      $G a ∧ F a$,
      rule(
        name: [$and$ E],
        $G a$,
        [$[F a ∧ G a]^1$],
      ),
      rule(
        name: [$and$ E],
        $F a$,
        $[F a ∧ G a]^1$,
      ),
    ),
  ),
)


自然演繹のゲンツェン式の証明図の例

 シーケント計算の例#proof-tree(
  rule(
    name: [$→$ R],
    $⇒ (F a ∧ G a) → (G a ∧ F a)$,
    rule(
      name: [$and$ R],
      $F a ∧ G a ⇒ G a ∧ F a$,
      rule(
        name: [$and$ L],
        $F a ∧ G a ⇒ G a$,
        [$G a ⇒ G a$],
      ),
      rule(
        name: [$and$ L],
        $F a ∧ G a ⇒ F a$,
        $F a ⇒ F a$,
      ),
    ),
  ),
)


シーケント計算のゲンツェン式の証明図の例

 フィッチ式 (Fitch-style) の証明図私はあまり使いませんが、英語圏のテキストなどではよく見る気がします。
これまで (少なくとも typst Universe には) フィッチスタイルの証明を作成するためのパッケージは存在していなかったのですが、つい先日 (2024.11.12) に derive-it というパッケージがリリースされました。
ただ、LaTeXのfitch.styで作れるようなフィッチ式の証明図と若干区切り線の流儀が異なっており、今のところオプションなどで変更する方法はなさそうなので、その点に注意が必要かもしれません。
例:
#import "@preview/derive-it:0.1.1": *

#ded-nat(
  stcolor: black,
  arr: (
    (0, $∀x F x$, [PR]),
    (0, $∃x (F x → G x)$, [PR]),
    (1, $F a → G a$, [AS]),
    (1, $F a$, [$∀$ E 1]),
    (1, $G a$, [$→$ E 3, 4]),
    (0, $G a$, [$∃$ E 2, 3-5]),
    (0, $∃x G x$, [$∃$ I 6]),
  ),
)


自然演繹のフィッチ式の証明図の例

 スーピーズ/レモン式 (Suppes/Lemmon-style) の証明図自分で表を使っても十分作ることはできると思いますが、上記の derive-it がレモン式の証明図にも対応しています。
例:
#import "@preview/derive-it:0.1.1": *

#ded-nat(
  stcolor: black,
  arr: (
    ([1], 0, $∀x F x$, [PR]),
    ([2], 0, $∃x (F x → G x)$, [PR]),
    ([2, 3], 0, $F a → G a$, [AS]),
    ([1, 2, 3], 0, $F a$, [$∀$ E 1]),
    ([1, 2, 3], 0, $G a$, [$→$ E 3, 4]),
    ([1, 2], 0, $G a$, [$∃$ E 2, 3-5]),
    ([1, 2], 0, $∃x G x$, [$∃$ I 6]),
  ),
)


自然演繹のレモン式の証明図の例

 タブロータブロー用のパッケージというものは今のところ (typst Universe には) 公開されていないと思いますが、私は構文木を作成するための syntree パッケージを以下のように流用しています。
ただ、ネストが一定の深さを超えるとエラーになることがあります。Typst の仕様だと思いますが、ユーザーやパッケージ側の工夫で回避できるのかどうか分かっていません。
例:
#import "@preview/syntree:0.2.0": tree

// 間隔を調整する場合
#let tree = (..args) => tree(
  layer-spacing: 2em,
  child-spacing: 3em,
  ..args,
)

#tree(
  [$P → Q\ Q → R\ ¬(P → R)$],
  tree(
    [$P\ ¬R$],
    [$¬P$\ ×],
    tree(
      [$Q$],
      [$¬Q$\ ×],
      [$R$\ ×]
    ),
  ),
)


タブローの例

 結びこうしたパッケージが使えるだけでなく、簡単な処理や図表の作成であれば、自分でマクロ (関数) を書いて再利用することもそれほど難しくありません。ぜひお試しください! (日本語も使う場合はフォント設定をお忘れなく)

脚注
MathJax v3 から bussproofs が使えるようになり、Web用であれば Markdown 等でもできる範囲は広がりました ↩︎
LaTeXでも XeLaTeX/LuaLaTeX であればunicode-mathが利用できます ↩︎

出力	LaTeX	Typst
$P \land Q$	`P \land Q`	`P and Q`, `P ∧ Q`
$P \lor Q$	`P \lor Q`	`P or Q`, `P ∨ Q`
$P \to Q$	`P \to Q`	`P arrow Q`, `P -> Q`, `P → Q`
$P \supset Q$	`P \supset Q`	`P supset Q`, `P ⊃ Q`
$\neg P$	`\neg P`	`not P`, `¬P`
$\forall x$	`\forall x`	`forall x`, `∀x`
$\exists x$	`\exists x`	`exists x`, `∃x`
$a = b$	`a = b`	`a eq b`, `a = b`
$k_{a_1}, ..., k_{a_n}$	`k_{a_1}, ..., k_{a_n}`	`k_a_1, ..., k_a_n`
$\varphi[a/x]$	`\varphi[a/x]`	`phi[a\/x]`
$\Box A$	`\Box A`	`square.stroked A`, `□A`
$\Diamond A$	`\Diamond A`	`diamond.stroked A`, `◇A`
$\Gamma \Rightarrow \Delta$	`\Gamma \Rightarrow \Delta`	`Gamma => Delta`, `Γ ⇒ Δ`
$\Gamma \Longrightarrow \Delta$	`\Gamma \Longrightarrow \Delta`	`Gamma arrow.r.double.long Delta`, `Gamma ==> Delta`
$\Gamma \Longleftrightarrow \Delta$	`\Gamma \Longleftrightarrow \Delta`	`Gamma arrow.l.r.double Delta`, `Gamma <==> Delta`
$\Gamma \vdash \Delta$	`\Gamma \vdash \Delta`	`Gamma tack Delta`, `Γ ⊢ Δ`
$\Gamma \vDash \Delta$	`\Gamma \vDash \Delta`	`Gamma tack.r.double Delta`, `Γ ⊨ Δ`
$w \Vdash \varphi$	`w \vDash \varphi`	`w forces phi`, `w ⊩ φ`

論理式 etc. を書く

数式モード (math mode)

記号の入力

打ち消し線

述語の注意点

証明図を書く

ゲンツェン式 (Gentzen-style) の証明図

自然演繹の例

シーケント計算の例

フィッチ式 (Fitch-style) の証明図

スーピーズ/レモン式 (Suppes/Lemmon-style) の証明図

タブロー

結び

Discussion